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

D 2013

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

CHEN, Taolue, Vojtěch FOREJT, Marta KWIATKOWSKA, David PARKER, Aistis SIMAITIS et. al.

Basic information

Original name

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

Authors

CHEN, Taolue (156 China), Vojtěch FOREJT (203 Czech Republic, guarantor, belonging to the institution), Marta KWIATKOWSKA (616 Poland), David PARKER (826 United Kingdom of Great Britain and Northern Ireland) and Aistis SIMAITIS (440 Lithuania)

Edition

Berlin, Heidelberg, TACAS 2013, p. 185-191, 7 pp. 2013

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/13:00068069

Organization unit

Faculty of Informatics

ISBN

978-3-642-36741-0

ISSN

DOI

http://dx.doi.org/10.1007/978-3-642-36742-7_13

Keywords in English

model-checker; stochastic games

Abstract

V originále

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.

Links

LG13010, research and development project

Name: Zastoupení ČR v European Research Consortium for Informatics and Mathematics (Acronym: ERCIM-CZ)

Investor: Ministry of Education, Youth and Sports of the CR

MUNI/33/IP1/2013, interní kód MU

Name: 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 (Acronym: PVT-VVPZ)

Investor: Masaryk University

Citovat

CHEN, Taolue, Vojtěch FOREJT, Marta KWIATKOWSKA, David PARKER and Aistis SIMAITIS. PRISM-games: A model checker for stochastic multi-player games. In Nir Piterman and Scott A. Smolka. TACAS 2013. Berlin, Heidelberg: Springer, 2013, p. 185-191. ISBN 978-3-642-36741-0. Available from: https://dx.doi.org/10.1007/978-3-642-36742-7_13.

@inproceedings{1095782,
   author = {Chen, Taolue and Forejt, Vojtěch and Kwiatkowska, Marta and Parker, David and Simaitis, Aistis},
   address = {Berlin, Heidelberg},
   booktitle = {TACAS 2013},
   doi = {http://dx.doi.org/10.1007/978-3-642-36742-7_13},
   editor = {Nir Piterman and Scott A. Smolka},
   keywords = {model-checker; stochastic games},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Berlin, Heidelberg},
   isbn = {978-3-642-36741-0},
   pages = {185-191},
   publisher = {Springer},
   title = {PRISM-games: A model checker for stochastic multi-player games},
   url = {http://www.prismmodelchecker.org/papers/tacas13.pdf},
   year = {2013}
}

TY  - JOUR
ID  - 1095782
AU  - Chen, Taolue - Forejt, Vojtěch - Kwiatkowska, Marta - Parker, David - Simaitis, Aistis
PY  - 2013
TI  - PRISM-games: A model checker for stochastic multi-player games
PB  - Springer
CY  - Berlin, Heidelberg
SN  - 9783642367410
KW  - model-checker
KW  - stochastic games
UR  - http://www.prismmodelchecker.org/papers/tacas13.pdf
L2  - http://www.prismmodelchecker.org/papers/tacas13.pdf
N2  - 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.
ER  -

CHEN, Taolue, Vojtěch FOREJT, Marta KWIATKOWSKA, David PARKER and Aistis SIMAITIS. PRISM-games: A model checker for stochastic multi-player games. In Nir Piterman and Scott A. Smolka. \textit{TACAS 2013}. Berlin, Heidelberg: Springer, 2013, p.~185-191. ISBN~978-3-642-36741-0. Available from: https://dx.doi.org/10.1007/978-3-642-36742-7\_{}13.

Detailed Information on Publication Record