Faster statistical model checking for unbounded temporal properties Journal Article


Author(s): Daca, Przemysław; Henzinger, Thomas A; Křetínský, Jan; Petrov, Tatjana
Article Title: Faster statistical model checking for unbounded temporal properties
Affiliation IST Austria
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.
Keywords: simulation; Markov Chains; Temporal logic; mean payoff; Statistical model checking
Journal Title: ACM Transactions on Computational Logic (TOCL)
Volume: 18
Issue 2
ISSN: 1557-945X
Publisher: ACM  
Date Published: 2017-05-01
Start Page: Article number: 12
URL:
DOI: 10.1145/3060139
Notes: This is an extended version of Daca et al. [2016a] with full proofs and an extended discussion of the experimental results. This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), the People Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7/2007-2013) REA Grant No. 291734, the SNSF Advanced Postdoc Mobility Fellowship, grant No. P300P2-161067, and the Czech Science Foundation under grant agreement P202/12/G061.
Open access: yes (repository)
IST Austria Authors
  1. Thomas A. Henzinger
    410 Henzinger
  2. Przemysław, Daca
    12 Daca
  3. Tatjana Petrov
    12 Petrov
Related IST Austria Work