PRISM-games 3.0: Stochastic game verification with concurrency, equilibria and time
We present a major new release of the PRISM-games model checker, featuring multiple significant advances in its support for verification and strategy synthesis of stochastic games. Firstly, concurrent stochastic games bring more realistic modelling of agents interacting in a concurrent fashion. Seco...
| Main Authors: | , , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Springer
2020
|
| _version_ | 1797053439404933120 |
|---|---|
| author | Kwiatkowska, M Norman, G Parker, D Santos, G |
| author_facet | Kwiatkowska, M Norman, G Parker, D Santos, G |
| author_sort | Kwiatkowska, M |
| collection | OXFORD |
| description | We present a major new release of the PRISM-games model checker, featuring multiple significant advances in its support for verification and strategy synthesis of stochastic games. Firstly, concurrent stochastic games bring more realistic modelling of agents interacting in a concurrent fashion. Secondly, equilibria-based properties provide a means to analyse games in which competing or collaborating players are driven by distinct objectives. Thirdly, a real-time extension of (turn-based) stochastic games facilitates verification and strategy synthesis for systems where timing is a crucial aspect. This paper describes the advances made in the tool’s modelling language, property specification language and model checking engines in order to implement this new functionality. We also summarise the performance and scalability of the tool, and describe a selection of case studies, ranging from security protocols to robot coordination, which highlight the benefits of the new features. |
| first_indexed | 2024-03-06T18:43:45Z |
| format | Conference item |
| id | oxford-uuid:0dcba0ce-71f3-4a5f-a522-4b602a18a996 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T18:43:45Z |
| publishDate | 2020 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:0dcba0ce-71f3-4a5f-a522-4b602a18a9962022-03-26T09:42:25ZPRISM-games 3.0: Stochastic game verification with concurrency, equilibria and timeConference itemhttp://purl.org/coar/resource_type/c_5794uuid:0dcba0ce-71f3-4a5f-a522-4b602a18a996EnglishSymplectic ElementsSpringer2020Kwiatkowska, MNorman, GParker, DSantos, GWe present a major new release of the PRISM-games model checker, featuring multiple significant advances in its support for verification and strategy synthesis of stochastic games. Firstly, concurrent stochastic games bring more realistic modelling of agents interacting in a concurrent fashion. Secondly, equilibria-based properties provide a means to analyse games in which competing or collaborating players are driven by distinct objectives. Thirdly, a real-time extension of (turn-based) stochastic games facilitates verification and strategy synthesis for systems where timing is a crucial aspect. This paper describes the advances made in the tool’s modelling language, property specification language and model checking engines in order to implement this new functionality. We also summarise the performance and scalability of the tool, and describe a selection of case studies, ranging from security protocols to robot coordination, which highlight the benefits of the new features. |
| spellingShingle | Kwiatkowska, M Norman, G Parker, D Santos, G PRISM-games 3.0: Stochastic game verification with concurrency, equilibria and time |
| title | PRISM-games 3.0: Stochastic game verification with concurrency, equilibria and time |
| title_full | PRISM-games 3.0: Stochastic game verification with concurrency, equilibria and time |
| title_fullStr | PRISM-games 3.0: Stochastic game verification with concurrency, equilibria and time |
| title_full_unstemmed | PRISM-games 3.0: Stochastic game verification with concurrency, equilibria and time |
| title_short | PRISM-games 3.0: Stochastic game verification with concurrency, equilibria and time |
| title_sort | prism games 3 0 stochastic game verification with concurrency equilibria and time |
| work_keys_str_mv | AT kwiatkowskam prismgames30stochasticgameverificationwithconcurrencyequilibriaandtime AT normang prismgames30stochasticgameverificationwithconcurrencyequilibriaandtime AT parkerd prismgames30stochasticgameverificationwithconcurrencyequilibriaandtime AT santosg prismgames30stochasticgameverificationwithconcurrencyequilibriaandtime |