Automated Verification of Concurrent Stochastic Games

Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos

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

7 Citations (Scopus)
185 Downloads (Pure)

Abstract

We present automatic verification 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 verification and strategy synthesis of CSGs, as an extension of PRISM-games. We evaluate the performance, scalability and applicability of our techniques on case studies from domains such as security, networks and finance, 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.
Original languageEnglish
Title of host publicationProceedings of the 15th International Conference on Quantitative Evaluation of SysTems (QEST'18).
PublisherSpringer
Number of pages16
ISBN (Electronic)978-3-319-99154-2
ISBN (Print)978-3-319-99153-5
DOIs
Publication statusPublished - 15 Aug 2018
Event15th International Conference on Quantitative Evaluation of SysTems (QEST'18) - Beijing, China
Duration: 4 Sept 20187 Sept 2018

Publication series

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

Conference

Conference15th International Conference on Quantitative Evaluation of SysTems (QEST'18)
Country/TerritoryChina
CityBeijing
Period4/09/187/09/18

Fingerprint

Dive into the research topics of 'Automated Verification of Concurrent Stochastic Games'. Together they form a unique fingerprint.

Cite this