Sagar Chaki

Jeffery Hansen, Lutz Wrage, Sagar Chaki, Dionisio De Niz, Mark Klein, Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), April 11-18, 2015.

Software: Tools and benchmarks for experiments reported in the paper are here. Read LICENSE.txt for the license, and README.txt for usage.

Abstract: Statistical Model Checking (SMC) is a technique, based on Monte-Carlo simulations, for computing the bounded probability that a specific event occurs during a stochastic system's execution. Estimating the probability of a "rare" event accurately with SMC requires many simulations. To this end, Importance Sampling (IS) is used to reduce the simulation effort. Commonly, IS involves "tilting" the parameters of the original input distribution, which is ineffective if the set of inputs causing the event (i.e., input-event region) is disjoint. In this paper, we propose a technique called Semantic Importance Sampling (SIS) to address this challenge. Using an SMT solver, SIS recursively constructs an abstract indicator function that over-approximates the input-event region, and then uses this abstract indicator function to perform SMC with IS. By using abstraction and SMT solving, SIS thus exposes a new connection between the verification of non-deterministic and stochastic systems. We also propose two optimizations that reduce the SMT solving cost of SIS significantly. Finally, we implement SIS and validate it on several problems. Our results indicate that SIS reduces simulation effort by multiple orders of magnitude even in systems with disjoint input-event regions.