Statistical Model Checking : An Overview <s> What do we want to do? <s> In this survey we motivate, define and explain model checking of probabilistic deterministic and nondeterministic systems using the probabilistic computation tree logics PCTL and PCTL *. Juxtapositions to non-deterministic computation tree logic are made and algorithms are presented. <s> BIB001 </s> Statistical Model Checking : An Overview <s> What do we want to do? <s> Symbolic model checking methods have been extended recently to the verification of probabilistic systems. However, the representation of the transition matrix may be expensive for very large systems and may induce a prohibitive cost for the model checking algorithm. In this paper, we propose an approximation method to verify quantitative properties on discrete Markov chains. We give a randomized algorithm to approximate the probability that a property expressed by some positive LTL formula is satisfied with high confidence by a probabilistic system. Our randomized algorithm requires only a succinct representation of the system and is based on an execution sampling method. We also present an implementation and a few classical examples to demonstrate the effectiveness of our approach. <s> BIB002 </s> Statistical Model Checking : An Overview <s> What do we want to do? <s> We present MC 2 , what we believe to be the first randomized, Monte Carlo algorithm for temporal-logic model checking. Given a specification S of a finite-state system, an LTL formula φ, and parameters ∈ and 6, MC 2 takes M = ln(δ)/ln(1 - e) random samples (random walks ending in a cycle, i.e lassos) from the Biichi automaton B = B S x B ¬φ to decide if L(B) = θ Let p Z be the expectation of an accepting lasso in B. Should a sample reveal an accepting lasso l, MC 2 returns false with I as a witness. Otherwise, it returns true and reports that the probability of finding an accepting lasso through further sampling, under the assumption that p Z ≥ e, is less than 6. It does so in time O(MD) and space O(D), where D is B's recurrence diameter, using an optimal number of samples M. Our experimental results demonstrate that MC 2 is fast, memory-efficient, and scales extremely well. <s> BIB003 </s> Statistical Model Checking : An Overview <s> What do we want to do? <s> The goal of model checking is to verify the correctness of a given program, on all its inputs. The main obstacle, in many cases, is the intractably large size of the program's transition system. Property testing is a randomized method to verify whether some fixed property holds on individual inputs, by looking at a small random part of that input. We join the strengths of both approaches by introducing a new notion of probabilistic abstraction, and by extending the framework of model checking to include the use of these abstractions. Our abstractions map transition systems associated with large graphs to small transition systems associated with small random subgraphs. This reduces the original transition system to a family of small, even constant-size, transition systems. We prove that with high probability, “sufficiently” incorrect programs will be rejected (e-robustness). We also prove that under a certain condition (exactness), correct programs will never be rejected (soundness). Our work applies to programs for graph properties such as bipartiteness, k-colorability, or any ∃∀ first order graph properties. Our main contribution is to show how to apply the ideas of property testing to syntactic programs for such properties. We give a concrete example of an abstraction for a program for bipartiteness. Finally, we show that the relaxation of the test alone does not yield transition systems small enough to use the standard model checking method. More specifically, we prove, using methods from communication complexity, that the OBDD size remains exponential for approximate bipartiteness. <s> BIB004
We consider a stochastic system S and a property φ. An execution of S is a possibly infinite sequence of states of S. Our objective is to solve the probabilistic model checking problem, i.e., to decide whether S satisfies φ with a probability greater or equal to a certain threshold θ. The latter is denoted S |= P ≥θ (φ), where P is called a probabilistic operator. This paper will overview solutions to this problem. These solutions depend on the nature of S and φ. We consider three cases. 1. We first assume that S is a white-box system, i.e., that one can generate as much executions of the system as we want. We also assume that φ does not contain probabilistic operators. In Section 3, we recall basic statistical algorithms that can be used to verify bounded properties (i.e., properties that can be verified on fixed-length execution) of white-box systems. 2. In Section 4, we discuss extensions to the full probabilistic computation tree logic BIB001 . There, we consider the case where φ can also contain probabilistic operators and the case where it has to be verified on infinite executions. 3. In Section 5, we briefly discuss the verification of black-box systems, i.e. systems for which a part of the probability distribution is unknown. In addition, in Section 6, we will present various experiments that show that (1) statistical model checking algorithms are more efficient than numerical ones, and (2) statistical model checking algorithms can be applied to solve problems that are beyond the scope of numerical methods. Finally, Section 7 discusses the future of statistical model checking. Remark 1. The objective of the present tutorial is not to feed the reader with technical details, but rather to present the concepts of statistical model checking, and outline its main advantages in terms of efficiency, uniformity, and simplicity. Remark 2. There are other techniques that allow to estimate the probability for S to satisfies φ. Those techniques, which are based on Monte-Carlo techniques, will not be presented in this paper. The interested reader is redirected to BIB003 BIB002 BIB004 for more details.