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.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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"
WWW 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 0302-9743
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ěnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 29. 4. 2014 20:10.
Anotace
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 VaVNá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 MUNá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
VytisknoutZobrazeno: 17. 7. 2024 06:51