Faster statistical model checking for unbounded temporal properties Conference Paper

Author(s): Daca, Przemysław; Henzinger, Thomas A; Křetínský, Jan; Petrov, Tatjana P
Title: Faster statistical model checking for unbounded temporal properties
Title Series: LNCS
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: Linear temporal logic; Transition probabilities; Temporal property; mean payoff; High probability; On the flies; Statistical model checking; Strongly connected component
Conference Title: TACAS: Tools and Algorithms for the Construction and Analysis of Systems
Volume: 9636
Conference Dates: April 2 - 8, 2016
Conference Location: Eindhoven, Netherlands
Publisher: Springer  
Date Published: 2016-01-01
Start Page: 112
End Page: 129
DOI: 10.1007/978-3-662-49674-9_7
Notes: This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), the Austrian Science Fund (FWF) under grants project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), the Peo- ple 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 number P300P2 161067, and the Czech Science Foun- dation under grant agreement P202/12/G061.
Open access: yes (repository)
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
  2. Przemysław, Daca
    12 Daca
  3. Tatjana Petrov
    12 Petrov
Related IST Austria Work