Statistical Model Checking : An Overview <s> Nested Probability Operators <s> Abstract We propose a language for testing concurrent processes and examine its strength in terms of the processes that are distinguished by a test. By using probabilistic transition systems as the underlying semantic model, we show how a testing algorithm can distinguish, with a probability arbitrarily close to one, between processes that are not bisimulation equivalent. We also show a similar result (in a slightly stronger form) for a new process relation called 2 3 - bisimulation —which lies strictly between that of simulation and bisimulation. Finally, the ultimately strength of the testing language is shown to identify a new process relation called probabilistic bisimulation—which is strictly stronger than bisimulation. <s> BIB001 </s> Statistical Model Checking : An Overview <s> Nested Probability Operators <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> BIB002 </s> Statistical Model Checking : An Overview <s> Nested Probability Operators <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> Nested Probability Operators <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> BIB004 </s> Statistical Model Checking : An Overview <s> Nested Probability Operators <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> BIB005
We consider the problem of checking whether S satisfies φ with a probability greater or equal to θ. However, contrary to what we have been doing so far, we will now assume that φ cannot be decided on a single execution, i.e., we will assume that φ is of the form P ≥θ1 φ 1 . So, where is the difficulty? The difficulty is that φ cannot be model checked on a single execution, but rather depends on another test. Hence, we have to provide a way to nest tests. In his thesis, Younes proposed the following theorem. Theorem 1. Let ψ = P ≥θ (φ) be a property and assume that φ can be verified with Type-I error α ′ and Type-II error β ′ , then ψ can be verified with Type-I error α and Type-II error β, assuming that the indifference region is of size at least ((θ + δ) (  Hence one has to find a compromise between the size of the indifference region of the inner test and the outer one. There are two interesting facts to know about nested operators: 1. Even for bounded properties, the above result (and in fact, any result in the literature BIB002 BIB003 BIB004 BIB005 ) only works for systems that have the Markovian property. 2. In practice, the complexity (in term of number of sampling) becomes exponential in the number of tests. Remark 6. An interesting research direction would be to study the link with probabilistic testing BIB001 .