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

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/LG13010" target="_blank" >LG13010: Zastoupení ČR v European Research Consortium for Informatics and Mathematics</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2013

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

TACAS 2013

ISBN

9783642367410

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

7

Strana od-do

185-191

Název nakladatele

Springer

Místo vydání

Berlin, Heidelberg

Místo konání akce

Rome

Datum konání akce

1. 1. 2013

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—