PRISM-games: A model checker for stochastic multi-player games

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

CHEN Taolue FOREJT Vojtěch KWIATKOWSKA Marta PARKER David SIMAITIS Aistis

Year of publication 2013
Type Article in Proceedings
Conference TACAS 2013
MU Faculty or unit

Faculty of Informatics

Citation
Web http://www.prismmodelchecker.org/papers/tacas13.pdf
Doi http://dx.doi.org/10.1007/978-3-642-36742-7_13
Field Informatics
Keywords model-checker; stochastic games
Description 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 co-operative 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.