PRISM-games: a model checker for stochastic multi-player games. (English) Zbl 1381.68151

Piterman, Nir (ed.) et al., Tools and algorithms for the construction and analysis of systems. 19th international conference, TACAS 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16–24, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-36741-0/pbk). Lecture Notes in Computer Science 7795, 185-191 (2013).
Summary: We present PRISM-games, a model checker for stochastic multi-player games, which supports modelling, automated verification and strategy synthesis for probabilistic systems with competitive or cooperative behaviour. Models are described in a probabilistic extension of the Reactive Modules language and properties are expressed using rPATL, which extends the well-known logic ATL with operators to reason about probabilities, various reward-based measures, quantitative properties and precise bounds. The tool is based on the probabilistic model checker PRISM, benefiting from its existing user interface and simulator, whilst adding novel model checking algorithms for stochastic games, as well as functionality to synthesise optimal player strategies, explore or export them, and verify other properties under the specified strategy.
For the entire collection see [Zbl 1268.68030].


68Q60 Specification and verification (program logics, model checking, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
91A06 \(n\)-person games, \(n>2\)
91A15 Stochastic games, stochastic differential games
Full Text: DOI Link