Faster Statistical Model Checking for Unbounded Temporal Properties

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F16%3A00088469" target="_blank" >RIV/00216224:14330/16:00088469 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-662-49674-9_7" target="_blank" >http://dx.doi.org/10.1007/978-3-662-49674-9_7</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-662-49674-9_7" target="_blank" >10.1007/978-3-662-49674-9_7</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Faster Statistical Model Checking for Unbounded Temporal Properties

Popis výsledku v původním jazyce

We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds.

Název v anglickém jazyce

Faster Statistical Model Checking for Unbounded Temporal Properties

Popis výsledku anglicky

We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Centrum excelence - Institut teoretické informatiky (CE-ITI)</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2016

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 - 22nd International Conference, TACAS 2016

ISBN

9783662496732

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

18

Strana od-do

112-129

Název nakladatele

Springer

Místo vydání

Berlin Heidelberg

Místo konání akce

Berlin Heidelberg

Datum konání akce

1. 1. 2016

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

CST - Celostátní akce

Kód UT WoS článku

—