Statistical Model Checking

Statistical Model Checking (SMC) is a formal verification technique that combines simulation and statistical methods for the analysis of stochastic systems. It represents a powerful scalable alternative to numerical probabilistic model checking techniques that suffer from state space explosion issues.

Given a formal model of the stochastic system S and a formal specification of the requirement to verify \phi, SMC can answer two types of questions:

  • Quantitative: What is the probability that S satisfies \phi ?
  • Qualitative: Is the probability for S to satisfy \phi greater or lower than some given threshold \theta ?

The quantitative question can be answered by using probability estimation techniques based on Chernoff-Hoeffding bound. It mainly consists of computing an estimation p’ of p (the actual probability for S to satisfy \phi) such that Pr(|p’-p|<\delta)>=1-\alpha, where \delta and \alpha are respectively the required precision and the confidence level [1] [2].

Regarding the qualitative question, it is mainly answered using a hypothesis testing approach. Assuming p is the probability for S to satisfy \phi, hypothesis tesing decides which of the hypothesis H_0:p>=\theta against H_1:p<\theta is correct, given a confidence level (\alpha,\beta). One important work proposed in this context can be found in [3]. It relies on the Wald Probability ratio Test [4]

We implemented statistical model checking algorithm in the SBIP tool that supports different stochastic models, i.e. discrte-time Markov chains (DTMCs), continous-time Markov chains (CTMCs), and generalized semi-Markov processes (GSMPs). All these models can described in a high-level component-based modeling formalism BIP. For properties specification, the tool supports bounded LTL and MTL logics.

[1W. Hoeffding. Probability inequalities. Journal of the American Statistical Association, 1963

[2T. Herault, R. Lassaigne, F. Magniette, and S. Peyronnet. Approximate Probabilistic Model Checking. VMCAI’04

[3H. L. S. Younes. Verification and Planning for Stochastic Processes with Asynchronous Events. PhD thesis, Carnegie Mellon, 2005

[4A. Wald. Sequential tests of statistical hypotheses. Annals of Mathematical Statistics, 16(2):117–186, 1945.