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

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
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

Citace
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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.