PRISM-games: a model checker for stochastic multi-player games. 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.
Keywords for this software
References in zbMATH (referenced in 5 articles , 1 standard article )
Showing results 1 to 5 of 5.
- Chen, Taolue; Primiero, Giuseppe; Raimondi, Franco; Rungta, Neha: A computationally grounded, weighted doxastic logic (2016)
- Drager, Klaus; Forejt, Vojtech; Kwiatkowska, Marta; Parker, David; Ujma, Mateusz: Permissive controller synthesis for probabilistic systems (2015)
- Chen, Taolue; Forejt, Vojtěch; Kwiatkowska, Marta; Parker, David; Simaitis, Aistis: PRISM-games: a model checker for stochastic multi-player games (2013)
- Kwiatkowska, Marta: Advances in quantitative verification for ubiquitous computing (2013)
- Kwiatkowska, Marta; Parker, David: Automated verification and strategy synthesis for probabilistic systems (2013)