Statistical Model Checking : An Overview <s> Qualitative Answer using Statistical Model Checking <s> By a sequential test of a statistical hypothesis is meant any statistical test procedure which gives a specific rule, at any stage of the experiment (at the n-th trial for each integral value of n), for making one of the following three decisions: (1) to accept the hypothesis being tested (null hypothesis), (2) to reject the null hypothesis, (3) to continue the experiment by making an additional observation. Thus, such a test procedure is carried out sequentially. On the basis of the first trial, one of the three decisions mentioned above is made. If the first or the second decision is made, the process is terminated. If the third decision is made, a second trial is performed. Again on the basis of the first two trials one of the three decisions is made and if the third decision is reached a third trial is performed, etc. This process is continued until either the first or the second decision is made. <s> BIB001 </s> Statistical Model Checking : An Overview <s> Qualitative Answer using Statistical Model Checking <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> BIB002 </s> Statistical Model Checking : An Overview <s> Qualitative Answer using Statistical Model Checking <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> BIB003 </s> Statistical Model Checking : An Overview <s> Qualitative Answer using Statistical Model Checking <s> Probabilistic verification of continuous-time stochastic processes has received increasing attention in the model-checking community in the past 5 years, with a clear focus on developing numerical solution methods for model checking of continuous-time Markov chains. Numerical techniques tend to scale poorly with an increase in the size of the model (the "state space explosion problem"), however, and are feasible only for restricted classes of stochastic discrete-event systems. We present a statistical approach to probabilistic model checking, employing hypothesis testing and discrete-event simulation. Since we rely on statistical hypothesis testing, we cannot guarantee that the verification result is correct, but we can at least bound the probability of generating an incorrect answer to a verification problem. <s> BIB004
The main approaches BIB003 BIB002 proposed to answer the qualitative question are based on hypothesis testing. Let p = P r(φ), to determine whether p ≥ θ, we can test H : p ≥ θ against K : p < θ. A test-based solution does not guarantee a correct result but it is possible to bound the probability of making an error. The strength (α, β) of a test is determined by two parameters, α and β, such that the probability of accepting K (respectively, H) when H (respectively, K) holds, called a Type-I error (respectively, a Type-II error ) is less or equal to α (respectively, β). A test has ideal performance if the probability of the Type-I error (respectively, Type-II error) is exactly α (respectively, β). However, these requirements make it impossible to ensure a low probability for both types of errors simultaneously (see BIB003 for details). A solution to this problem is to relax the test by working with an indifference region (p 1 , p 0 ) with p 0 ≥p 1 (p 0 − p 1 is the size of the region). In this context, we test the hypothesis If the value of p is between p 1 and p 0 (the indifference region), then we say that the probability is sufficiently close to θ so that we are indifferent with respect to which of the two hypotheses K or H is accepted. The thresholds p 0 and p 1 are generally defined in term of the single threshold θ, e.g., p 1 = θ − δ and p 0 = θ + δ. We now need to provide a test procedure that satisfies the requirements above. In the next two subsections, we recall two solutions proposed by Younes in BIB003 BIB004 . Single Sampling Plan. To test H 0 against H 1 , we specify a constant c. If n i=1 b i is larger than c, then H 0 is accepted, else H 1 is accepted. The difficult part in this approach is to find values for the pair (n, c), called a single sampling plan (SSP in short), such that the two error bounds α and β are respected. In practice, one tries to work with the smallest value of n possible so as to minimize the number of simulations performed. Clearly, this number has to be greater if α and β are smaller but also if the size of the indifference region is smaller. This results in an optimization problem, which generally does not have a closed-form solution except for a few special cases BIB003 . In his thesis BIB003 , Younes proposes a binary search based algorithm that, given p 0 , p 1 , α, β, computes an approximation of the minimal value for c and n. ≥p. Here, the difficulty is to find a value for n such that the error bounds are valid. Sequential probability ratio test. The sample size for a single sampling plan is fixed in advance and independent of the observations that are made. However, taking those observations into account can increase the performance of the test. As an example, if we use a single plan (n, c) and the m > c first simulations satisfy the property, then we could (depending on the error bounds) accept H 0 without observing the n − m other simulations. To overcome this problem, one can use the sequential probability ratio test (SPRT in short) proposed by Wald BIB001 . The approach is briefly described below. In SPRT, one has to choose two values A and B (A > B) (see bellow) that ensure that the strength of the test is respected. Let m be the number of observations that have been made so far. The test is based on the following quotient: where for successive values of m until either H 0 or H 1 is satisfied; the algorithm terminates with probability 1 BIB001 . This has the advantage of minimizing the number of simulations. In his thesis BIB003 , Younes proposed a logarithmic based algorithm SPRT that given p 0 , p 1 , α and β implements the sequential ratio testing procedure.