An Evaluation of Estimation Techniques for Probabilistic Verification

Formal techniques for verifying stochastic systems (e.g.., probabilistic model checking) do not generally scale well with respect to the system size. Therefore, simulation-based techniques such as statistical model checking are often used in practice. In this paper, we focus on stochastic hybrid systems and evaluate Monte Carlo and Quasi-Monte Carlo (QMC) methods for computing probabilistic reachability. We compare a number of interval estimation techniques based on the Central Limit Theorem (CLT), and we also introduce a new approach based on the CLT for computing confidence intervals for probabilities near the borders of the [0,1] interval. We empirically show that QMC techniques and our CLT approach are accurate and efficient in practice. Our results readily apply to any stochastic system and property that can be checked by simulation, and are hence relevant for statistical model checking.