Conference item
Multi-player equilibria verification for concurrent stochastic games
- Abstract:
- Concurrent stochastic games (CSGs) are an ideal formalism for modelling probabilistic systems that feature multiple players or components with distinct objectives making concurrent, rational decisions. Examples include communication or security protocols and multi-robot navigation. Verification methods for CSGs exist but are limited to scenarios where agents or players are grouped into two coalitions, with those in the same coalition sharing an identical objective. In this paper, we propose multi-coalitional verification techniques for CSGs. We use subgame-perfect social welfare (or social cost) optimal Nash equilibria, which are strategies where there is no incentive for any coalition to unilaterally change its strategy in any game state, and where the total combined objectives are maximised (or minimised). We present an extension of the temporal logic rPATL (probabilistic alternating-time temporal logic with rewards) to specify equilibria-based properties for any number of distinct coalitions, and a corresponding model checking algorithm for a variant of stopping games. We implement our techniques in the PRISM-games tool and apply them to several case studies, including a secret sharing protocol and a public good game.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Accepted manuscript, 460.0KB, Terms of use)
-
- Publisher copy:
- 10.1007/978-3-030-59854-9_7
- Publication website:
- https://www.springer.com/gp/book/9783030598532
Authors
- Publisher:
- Springer
- Host title:
- Quantitative Evaluation of Systems: 17th International Conference, QEST 2020, Vienna, Austria, August 31–September 3, 2020, Proceedings
- Journal:
- Proceedings of the 17th International Conference on Quantitative Evaluation of Systems More from this journal
- Volume:
- 12289
- Pages:
- 74-95
- Series:
- Theoretical Computer Science and General Issues
- Publication date:
- 2020-11-03
- Acceptance date:
- 2020-08-03
- Event title:
- 17th International Conference on Quantitative Evaluation of SysTems (QEST 2020)
- Event location:
- Online
- Event website:
- http://www.qest.org/qest2020/
- Event start date:
- 2020-08-31
- Event end date:
- 2020-09-03
- DOI:
- ISSN:
-
0302-9743
- EISBN:
- 978-3-030-59854-9
- ISBN:
- 978-3-030-59853-2
- Language:
-
English
- Keywords:
- Pubs id:
-
1123636
- Local pid:
-
pubs:1123636
- Deposit date:
-
2020-08-05
Terms of use
- Copyright holder:
- Springer Nature
- Copyright date:
- 2020
- Rights statement:
- © Springer Nature Switzerland AG 2020
- Notes:
- This paper will be presented at the 17th International Conference on Quantative Evaluation of SysTems (QEST 2020), 31st August - 3rd September 2020. This is the accepted manuscript version of the article. The final version is available from Springer at: https://doi.org/10.1007/978-3-030-59854-9_7
If you are the owner of this record, you can report an update to it here: Report update to this record