Faster Statistical Model Checking for Unbounded Temporal Properties

TL;DR

This paper introduces a new, efficient algorithm for statistical model checking of Markov chains with unbounded properties, enabling faster verification with less system information and applicability to quantitative properties.

Contribution

The authors propose a novel on-the-fly monitoring algorithm that detects high-probability bottom strongly connected components, reducing simulation length and system knowledge requirements.

Findings

Simulation runs are significantly shorter than traditional methods.

The method requires only minimal transition probability information.

It can be extended to unbounded quantitative properties like mean-payoff bounds.

Abstract

We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, such as reachability and 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 and size of the state space. In comparison to previous algorithms for statistical model checking, for a given level of confidence, 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, thus enabling almost complete black-box verification. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds.