# 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 , SMC can answer two types of questions:

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

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 ) such that Pr(|p’-p|<)>=, where and 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 , hypothesis tesing decides which of the hypothesis against  is correct, given a confidence level (). 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.