Faster Statistical Model Checking for Unbounded Temporal Properties
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Faster Statistical Model Checking for Unbounded Temporal Properties
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Center of excellence - Institute for theoretical computer science (CE-ITI)</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2016
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016
ISBN
9783662496732
ISSN
0302-9743
e-ISSN
—
Number of pages
18
Pages from-to
112-129
Publisher name
Springer
Place of publication
Berlin Heidelberg
Event location
Berlin Heidelberg
Event date
Jan 1, 2016
Type of event by nationality
CST - Celostátní akce
UT code for WoS article
—