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%2F13%3A00072856" target="_blank" >RIV/00216224:14330/13:00072856 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/s10703-013-0183-7" target="_blank" >http://dx.doi.org/10.1007/s10703-013-0183-7</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/s10703-013-0183-7" target="_blank" >10.1007/s10703-013-0183-7</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 an algorithm for verifying properties expressed in this logic and implement the techniques in a probabilistic model checker, as an extension of 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 an algorithm for verifying properties expressed in this logic and implement the techniques in a probabilistic model checker, as an extension of the PRISM tool.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

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 periodika

Formal Methods in System Design

ISSN

0925-9856

e-ISSN

—

Svazek periodika

43

Číslo periodika v rámci svazku

1

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

32

Strana od-do

61-92

Kód UT WoS článku

000321223500003

EID výsledku v databázi Scopus

—