Oxford logo
[KNP+18] M. Kwiatkowska, G. Norman, D. Parker, and G. Santos. Automated Verification of Concurrent Stochastic Games. In Proc. 15th International Conference on Quantitative Evaluation of SysTems (QEST 2018), Springer. 2018. [pdf] [bib]
Downloads:  pdf pdf (408 KB)  bib bib
Notes: The original publication is available at link.springer.com.
Abstract. We present automatic verifi cation techniques for concurrent stochastic multi-player games (CSGs) with rewards. To express properties of such models, we adapt the temporal logic rPATL (probabilistic alternating-time temporal logic with rewards), originally introduced for the simpler model of turn-based games, which enables quantitative reasoning about the ability of coalitions of players to achieve goals related to the probability of an event or reward measures. We propose and implement a modelling approach and model checking algorithms for property verifi cation and strategy synthesis of CSGs, as an extension of PRISMgames. We evaluate the performance, scalability and applicability of our techniques on case studies from domains such as security, networks and fi nance, showing that we can analyse systems with probabilistic, cooperative and competitive behaviour between concurrent components, including many scenarios that cannot be analysed with turn-based models.