PRISM-games: A model checker for stochastic multi-player games
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F13%3A00068069" target="_blank" >RIV/00216224:14330/13:00068069 - isvavai.cz</a>
Result on the web
<a href="http://www.prismmodelchecker.org/papers/tacas13.pdf" target="_blank" >http://www.prismmodelchecker.org/papers/tacas13.pdf</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-642-36742-7_13" target="_blank" >10.1007/978-3-642-36742-7_13</a>
Alternative languages
Result language
angličtina
Original language name
PRISM-games: A model checker for stochastic multi-player games
Original language 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, exploreor export them, and verify other properties under the specified strategy.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/LG13010" target="_blank" >LG13010: Czech Republic representation in the European Research Consortium for Informatics and Mathematics (ERCIM)</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2013
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
TACAS 2013
ISBN
9783642367410
ISSN
0302-9743
e-ISSN
—
Number of pages
7
Pages from-to
185-191
Publisher name
Springer
Place of publication
Berlin, Heidelberg
Event location
Rome
Event date
Jan 1, 2013
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—