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.
CITATION STYLE
Legay, A., Lukina, A., Traonouez, L. M., Yang, J., Smolka, S. A., & Grosu, R. (2019). Statistical model checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10000). Springer. https://doi.org/10.1007/978-3-319-91908-9_23
Mendeley helps you to discover research relevant for your work.