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.

Základní údaje

Originální název

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

Autoři

CHEN, Taolue (156 Čína), Vojtěch FOREJT (203 Česká republika, garant, domácí), Marta KWIATKOWSKA (616 Polsko), David PARKER (826 Velká Británie a Severní Irsko) a Aistis SIMAITIS (440 Litva)

Vydání

Berlin, Heidelberg, TACAS 2013, od s. 185-191, 7 s. 2013

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

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

Forma vydání

tištěná verze "print"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/13:00068069

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-36741-0

ISSN

DOI

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

Klíčová slova anglicky

model-checker; stochastic games

Štítky

core_A, firank_A

Změněno: 29. 4. 2014 20:10, RNDr. Pavel Šmerk, Ph.D.

Anotace

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.

Návaznosti

LG13010, projekt VaV

Název: Zastoupení ČR v European Research Consortium for Informatics and Mathematics (Akronym: ERCIM-CZ)

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Zastoupení ČR v European Research Consortium for Informatics and Mathematics

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

Název: 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 (Akronym: PVT-VVPZ)

Investor: Masarykova univerzita, 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

Citovat

CHEN, Taolue, Vojtěch FOREJT, Marta KWIATKOWSKA, David PARKER a 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, s. 185-191. ISBN 978-3-642-36741-0. Dostupné z: 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 a 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, s.~185-191. ISBN~978-3-642-36741-0. Dostupné z: https://dx.doi.org/10.1007/978-3-642-36742-7\_{}13.

Podrobný výpis o publikaci