Automatic Verification of Competitive Stochastic Systems

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F12%3A00064717" target="_blank" >RIV/00216224:14330/12:00064717 - isvavai.cz</a>

Výsledek na webu

<a href="http://www.prismmodelchecker.org/papers/tacas12.pdf" target="_blank" >http://www.prismmodelchecker.org/papers/tacas12.pdf</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-642-28756-5_22" target="_blank" >10.1007/978-3-642-28756-5_22</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Automatic Verification of Competitive Stochastic Systems

Popis výsledku v původním jazyce

We present automatic verification techniques for the modelling and analysis of probabilistic systems that incorporate competitive behaviour. These systems are modelled as turn-based stochastic multi-player games, in which the players can either collaborate or compete in order to achieve a particular goal. We define a temporal logic called rPATL for expressing quantitative properties of stochastic multi-player games. This logic allows us to reason about the collective ability of a set of players to achieve a goal relating to the probability of an event's occurrence or the expected amount of cost/reward accumulated. We give a model checking algorithm for verifying properties expressed in this logic and implement the techniques in a probabilistic model checker, based on the PRISM tool.

Název v anglickém jazyce

Automatic Verification of Competitive Stochastic Systems

Popis výsledku anglicky

We present automatic verification techniques for the modelling and analysis of probabilistic systems that incorporate competitive behaviour. These systems are modelled as turn-based stochastic multi-player games, in which the players can either collaborate or compete in order to achieve a particular goal. We define a temporal logic called rPATL for expressing quantitative properties of stochastic multi-player games. This logic allows us to reason about the collective ability of a set of players to achieve a goal relating to the probability of an event's occurrence or the expected amount of cost/reward accumulated. We give a model checking algorithm for verifying properties expressed in this logic and implement the techniques in a probabilistic model checker, based on the PRISM tool.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/LA09016" target="_blank" >LA09016: Účast ČR v European Research Consortium for Informatics and Mathematics (ERCIM)</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í

2012

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

Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference

ISBN

9783642287558

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

15

Strana od-do

315-330

Název nakladatele

Springer

Místo vydání

Berlin, Heidelberg

Místo konání akce

Tallinn

Datum konání akce

1. 1. 2012

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

WRD - Celosvětová akce

Kód UT WoS článku

—