Statistical Model Checking : An Overview <s> Introduction and Context <s> We determine the complexity of testing whether a finite state, sequential or concurrent probabilistic program satisfies its specification expressed in linear-time temporal logic. For sequential programs, we present an algorithm that runs in time linear in the program and exponential in the specification, and also show that the problem is in PSPACE, matching the known lower bound. For concurrent programs, we show that the problem can be solved in time polynomial in the program and doubly exponential in the specification, and prove that it is complete for double exponential time. We also address these questions for specifications described by ω-automata or formulas in extended temporal logic. <s> BIB001 </s> Statistical Model Checking : An Overview <s> Introduction and Context <s> We propose a model independent procedure for verifying properties of discrete event systems. The dynamics of such systems can be very complex, making them hard to analyze, so we resort to methods based on Monte Carlo simulation and statistical hypothesis testing. The verification is probabilistic in two senses. First, the properties, expressed as CSL formulas, can be probabilistic. Second, the result of the verification is probabilistic, and the probability of error is bounded by two parameters passed to the verification procedure. The verification of properties can be carried out in an anytime manner by starting off with loose error bounds, and gradually tightening these bounds. <s> BIB002 </s> Statistical Model Checking : An Overview <s> Introduction and Context <s> Continuous-time Markov chains (CTMCs) have been widely used to determine system performance and dependability characteristics. Their analysis most often concerns the computation of steady-state and transient-state probabilities. This paper introduces a branching temporal logic for expressing real-time probabilistic properties on CTMCs and presents approximate model checking algorithms for this logic. The logic, an extension of the continuous stochastic logic CSL of Aziz et al. (1995, 2000), contains a time-bounded until operator to express probabilistic timing properties over paths as well as an operator to express steady-state probabilities. We show that the model checking problem for this logic reduces to a system of linear equations (for unbounded until and the steady-state operator) and a Volterra integral equation system (for time-bounded until). We then show that the problem of model-checking time-bounded until properties can be reduced to the problem of computing transient state probabilities for CTMCs. This allows the verification of probabilistic timing properties by efficient techniques for transient analysis for CTMCs such as uniformization. Finally, we show that a variant of lumping equivalence (bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of all formulas in the logic. <s> BIB003 </s> Statistical Model Checking : An Overview <s> Introduction and Context <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> BIB004 </s> Statistical Model Checking : An Overview <s> Introduction and Context <s> This paper gives a brief overview of version 2.0 of PRISM, a tool for the automatic formal verification of probabilistic systems, and some of the case studies to which it has already been applied. <s> BIB005 </s> Statistical Model Checking : An Overview <s> Introduction and Context <s> We propose a new statistical approach to analyzing stochastic systems against specifications given in a sublogic of continuous stochastic logic (CSL). Unlike past numerical and statistical analysis methods, we assume that the system under investigation is an unknown, deployed black-box that can be passively observed to obtain sample traces, but cannot be controlled. Given a set of executions (obtained by Monte Carlo simulation) and a property, our algorithm checks, based on statistical hypothesis testing, whether the sample provides evidence to conclude the satisfaction or violation of a property, and computes a quantitative measure (p-value of the tests) of confidence in its answer; if the sample does not provide statistical evidence to conclude the satisfaction or violation of the property, the algorithm may respond with a don't know answer. We implemented our algorithm in a Java-based prototype tool called VESTA, and experimented with the tool using case studies analyzed in [15]. Our empirical results show that our approach may, at least in some cases, be faster than previous analysis methods. <s> BIB006 </s> Statistical Model Checking : An Overview <s> Introduction and Context <s> Statistical methods to model check stochastic systems have been, thus far, developed only for a sublogic of continuous stochastic logic (CSL) that does not have steady state operator and unbounded until formulas. In this paper, we present a statistical model checking algorithm that also verifies CSL formulas with unbounded untils. The algorithm is based on Monte Carlo simulation of the model and hypothesis testing of the samples, as opposed to sequential hypothesis testing. We have implemented the algorithm in a tool called VESTA, and found it to be effective in verifying several examples. <s> BIB007 </s> Statistical Model Checking : An Overview <s> Introduction and Context <s> We explore the concept of a “black-box” stochastic system, and propose an algorithm for verifying probabilistic properties of such systems based on very weak assumptions regarding system dynamics. Properties are expressed as formulae in a probabilistic temporal logic. Our presentation is a generalization of and an improvement over recent work by Sen et al. on probabilistic verification for “black-box” systems. <s> BIB008 </s> Statistical Model Checking : An Overview <s> Introduction and Context <s> We give a brief overview of a statistical model-checking and analysis tool VESTA. VESTA is a tool for statistical analysis of probabilistic systems. It supports statistical model-checking and statistical evaluation of expected values of temporal expressions. <s> BIB009 </s> Statistical Model Checking : An Overview <s> Introduction and Context <s> We present Ymer, a tool for verifying probabilistic transient properties of stochastic discrete event systems. Ymer implements both statistical and numerical model checking techniques. We focus on two features of Ymer: distributed acceptance sampling and statistical model checking of nested probabilistic statements. <s> BIB010 </s> Statistical Model Checking : An Overview <s> Introduction and Context <s> Asynchronous stochastic systems are abundant in the real world. Examples include queuing systems, telephone exchanges, and computer networks. Yet, little attention has been given to such systems in the model checking and planning literature, at least not without making limiting and often unrealistic assumptions regarding the dynamics of the systems. The most common assumption is that of history-independence: the Markov assumption. In this thesis, we consider the problems of verification and planning for stochastic processes with asynchronous events, without relying on the Markov assumption. We establish the foundation for statistical probabilistic model checking, an approach to probabilistic model checking based on hypothesis testing and simulation. We demonstrate that this approach is competitive with state-of-the-art numerical solution methods for probabilistic model checking. While the verification result can be guaranteed only with some probability of error, we can set this error bound arbitrarily low (at the cost of efficiency). Our contribution in planning consists of a formalism, the generalized semi-Markov decision process (GSMDP), for planning with asynchronous stochastic events. We consider both goal directed and decision theoretic planning. In the former case, we rely on statistical model checking to verify plans, and use the simulation traces to guide plan repair. In the latter case, we present the use of phase-type distributions to approximate a GSMDP with a continuous-time MDP, which can then be solved using existing techniques. We demonstrate that the introduction of phases permits us to take history into account when making action choices, and this can result in policies of higher quality than we would get if we ignored history dependence. <s> BIB011 </s> Statistical Model Checking : An Overview <s> Introduction and Context <s> LiQuor is a tool for verifying probabilistic reactive systems modelled Probmela programs, which are terms of a probabilistic guarded command language with an operational semantics based on (finite) Markov decision processes. LiQuor provides the facility to perform a qualitative or quantitative analysis for omega-regular linear time properties by means of automata-based model checking algorithms <s> BIB012
Quantitative properties of stochastic systems are usually specified in logics that allow one to compare the measure of executions satisfying certain temporal properties with thresholds. The model checking problem for stochastic systems with respect to such logics is typically solved by a numerical approach that iteratively computes (or approximates) the exact measure of paths satisfying relevant subformulas. The algorithm for computing such measures depends on the class of stochastic systems being considered as well as the logics used for specifying the correctness properties. Model checking algorithms for a variety of contexts have been discovered BIB003 BIB001 BIB004 and there are mature tools (see e.g. BIB005 BIB012 ) that have been used to analyze a variety of systems in practice. Despite the great strides made by numerical model checking algorithms, there are many challenges. Numerical algorithms work only for special systems that have certain structural properties. Further the algorithms require a lot of time and space, and thus scaling to large systems is a challenge. Finally, the logics for which model checking algorithms exist are extensions of classical temporal logics, which are often not the most popular among engineers. Another approach to verify quantitative properties of stochastic systems is to simulate the system for finitely many runs, and use hypothesis testing to infer whether the samples provide a statistical evidence for the satisfaction or violation of the specification BIB002 . The crux of this approach is that since sample runs of a stochastic system are drawn according to the distribution defined by the system, they can be used to get estimates of the probability measure on executions. Starting from time-bounded PCTL properties BIB002 , the technique has been extended to handle properties with unbounded until operators BIB007 , as well as to black-box systems BIB006 BIB008 . Tools based on this idea have been built BIB009 BIB010 , and they have been used to analyze many systems. This approach enjoys many advantages. First, these algorithms only require that the system be executable (or rather, sample executions be drawn according to the measure space defined by the system). Thus, it can be applied to larger class of systems than numerical model checking algorithms including black-box systems and infinite state systems. Second the approach can be generalized to a larger class of properties, including Fourier transform based logics. Finally, the algorithm is easily parallelizable, which can help scale to large systems. However, the statistical approach also has some disadvantages when compared with the numerical approach. First, it only provides probabilistic guarantees about the correctness of the algorithms answer. Next, the sample size grows very large if the model checker's answer is required to be highly accurate. Finally, the statistical approach only works for purely probabilistic systems, i.e., those that do not have any nondeterminism. Furthermore, since statistical tests are used to determine the correctness of a system, the approach only works for systems that "robustly" satisfy a given property, i.e., the actual measure of paths satisfying a given subformula, is bounded away from the thresholds to which it is compared in the specification. In this short paper, we will overview some of existing statistical model checking algorithms and discuss their efficiency. We will present the hypothesis testing algorithms that are at the heart of most of statistical algorithms and show how to uniformly analyze a large class of systems and properties. We will also discuss case studies. Most of these results are taken from Haakan Younes PhD Thesis BIB011 .