Journal
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS (TACAS 2016)
Volume 9636, Issue -, Pages 112-129Publisher
SPRINGER-VERLAG BERLIN
DOI: 10.1007/978-3-662-49674-9_7
Keywords
-
Funding
- European Research Council (ERC) [267989]
- Austrian Science Fund (FWF) [S11402-N23, Z211-N23]
- People Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7) REA Grant [291734]
- SNSF Advanced Postdoc.Mobility Fellowship [P300P2_161067]
- Czech Science Foundation [P202/12/G061]
- Swiss National Science Foundation (SNF) [P300P2_161067] Funding Source: Swiss National Science Foundation (SNF)
Ask authors/readers for more resources
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.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available