TY - GEN
T1 - Automated Verification of Concurrent Stochastic Games
AU - Kwiatkowska, Marta
AU - Norman, Gethin
AU - Parker, David
AU - Santos, Gabriel
PY - 2018/8/15
Y1 - 2018/8/15
N2 - 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.
AB - 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.
U2 - 10.1007/978-3-319-99154-2_14
DO - 10.1007/978-3-319-99154-2_14
M3 - Conference contribution
SN - 978-3-319-99153-5
T3 - Lecture Notes in Computer Science
BT - Proceedings of the 15th International Conference on Quantitative Evaluation of SysTems (QEST'18).
PB - Springer
T2 - 15th International Conference on Quantitative Evaluation of SysTems (QEST'18)
Y2 - 4 September 2018 through 7 September 2018
ER -