---
res:
bibo_abstract:
- 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.@eng
bibo_authorlist:
- foaf_Person:
foaf_givenName: Przemyslaw
foaf_name: Daca, Przemyslaw
foaf_surname: Daca
foaf_workInfoHomepage: http://www.librecat.org/personId=49351290-F248-11E8-B48F-1D18A9856A87
- foaf_Person:
foaf_givenName: Thomas A
foaf_name: Henzinger, Thomas A
foaf_surname: Henzinger
foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
orcid: 0000−0002−2985−7724
- foaf_Person:
foaf_givenName: Jan
foaf_name: Kretinsky, Jan
foaf_surname: Kretinsky
foaf_workInfoHomepage: http://www.librecat.org/personId=44CEF464-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0002-8122-2881
- foaf_Person:
foaf_givenName: Tatjana
foaf_name: Petrov, Tatjana
foaf_surname: Petrov
foaf_workInfoHomepage: http://www.librecat.org/personId=3D5811FC-F248-11E8-B48F-1D18A9856A87
bibo_doi: 10.1007/978-3-662-49674-9_7
bibo_volume: 9636
dct_date: 2016^xs_gYear
dct_language: eng
dct_publisher: Springer@
dct_title: Faster statistical model checking for unbounded temporal properties@
...