Faster Statistical Model Checking for Unbounded Temporal Properties

Investor logo

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

DACA Przemyslaw HENZINGER Thomas A. KŘETÍNSKÝ Jan PETROV Tatjana

Year of publication 2016
Type Article in Proceedings
Conference Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-662-49674-9_7
Field Informatics
Keywords statistical model checking; verification; temporal logic
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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.