Statistical Model Checking : An Overview <s> Black-box Systems: a note <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> BIB001 </s> Statistical Model Checking : An Overview <s> Black-box Systems: a note <s> We introduce a framework for expressing correctness guarantees of model-checking algorithms. The framework allows us to qualitatively compare different solution techniques for probabilistic model checking, both techniques based on statistical sampling and numerical computation of probability estimates. We provide several new insights into the relative merits of the different approaches. In addition, we present a new statistical solution method that can bound the probability of error under any circumstances by sometimes reporting undecided results. Previous statistical solution methods could only bound the probability of error outside of an “indifference region.” <s> BIB002
Black-box Systems is an interesting class of stochastic systems whose treatment is beyond the scope of numerical techniques. Roughly speaking, a black-box systems is simply a system whose probability distribution (i.e., set of behaviors) is not totally known and cannot be observed. Hence, one can view a black-box system as a finite set of executions pre-computed and for which no information is available. In the context of such systems, Type errors and indifference region cannot play a role. Indeed, those parameters influence the number of simulations that can be computed, but here the simulations are given and you cannot compute more! A solution to this problem is to conduct a SSP test, without indifference region (i.e., δ set to 0) and assuming that the parameter n is fixed to the number of simulations that are given in advance. The difficulty is to chose the constant c in such a way that it becomes roughly equal to accept H 0 or H 1 if θ = p. In his thesis BIB001 and in BIB002 , Younes proposed a solution to the problem. He also shown that a previous solution proposed by Sen [25] is not correct. There are techniques to verify nested formulas over black-box systems. There exists no technique for the verification of unbounded properties. Hence there is still a lot of research to conduct in this area.