Statistical model checking

We highlight the contributions made in the field of Statistical Model Checking (SMC) since its inception in 2002. As the formal setting, we use a very general model of Stochastic Systems (an SS is simply a family of time-indexed random variables), and Bounded LTL (BLTL) as the temporal logic. Let S be an SS and ϕ a BLTL formula. Our survey of the area is centered around the following five main contributions. Qualitative approach to SMC: Is the probability that S satisfies ϕ greater or equal to a certain threshold? Quantitative approach to SMC: What is the probability that S satisfies ϕ? Typically this results in a confidence interval being computed for this probability. Rare Events: What happens when the probability that S satisfies ϕ is extremely small, i.e. it is a rare event? To make the SMC approach viable in this setting, rare-event estimation techniques Importance Sampling and Importance Splitting are deployed to great advantage. Optimal Planning: Motivated by the success of Importance Sampling and Importance Splitting in rare-event SMC, we explore the use of these techniques in the context of optimal planning. In particular, we consider ARES, an optimal-planning approach based on a notion of adaptive receding-horizon planning. We illustrate the utility of ARES on the planning problem of bringing a flock of birds (autonomous agents) from a random initial configuration to a V-formation, an energy-conservation formation deployed by migrating geese. Somewhat ironically, the performance of ARES can be evaluated using (quantitative) SMC, as the problem to be solved is of the form F (J ≤ θ); i.e. does an ARES-generated plan eventually bring the flock to a configuration where the flock-wide cost function J is below a given threshold θ? Optimal Control: We show that the techniques we presented for optimal planning in the form of ARES carry over to the control setting in the form of Adaptive-Horizon Model-Predictive Control (AMPC). We again use the V-formation problem for evaluation purposes. We also introduce the concept of V-formation games, and show how the power of AMPC can be used to ward off cyber-physical attacks.