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

• Autoři: CHEN Taolue; FOREJT Vojtěch; KWIATKOWSKA Marta; PARKER David; SIMAITIS Aistis
• Rok publikování: 2013
• Druh: Článek ve sborníku
• Konference: TACAS 2013
• Fakulta / Pracoviště MU: Fakulta informatiky
• www: http://www.prismmodelchecker.org/papers/tacas13.pdf
• Doi: http://dx.doi.org/10.1007/978-3-642-36742-7_13
• Obor: Informatika
• Klíčová slova: model-checker; stochastic games
• Popis: 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.

Související projekty

• Podpora perspektivních výzkumných týmů Fakulty informatiky a vynikajících vědeckých pracovníků z jiných institucí působících na Fakultě informatiky
• Zastoupení ČR v European Research Consortium for Informatics and Mathematics