Multi-player Equilibria Verification for Concurrent Stochastic Games

Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 subgameperfect 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.
Original languageEnglish
Title of host publicationProceedings of the 17th International Conference on Quantitative Evaluation of SysTems (QEST'20)
Number of pages21
Publication statusAccepted/In press - 19 Jun 2020
Event17th International Conference on Quantitative Evaluation of SysTems (QEST'20) - Virtual Event
Duration: 31 Aug 20203 Sept 2020

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference17th International Conference on Quantitative Evaluation of SysTems (QEST'20)
CityVirtual Event


Dive into the research topics of 'Multi-player Equilibria Verification for Concurrent Stochastic Games'. Together they form a unique fingerprint.

Cite this