Abstract
Statistical model checking avoids the intractable growth of states associated with probabilistic model checking by estimating the probability of a property from simulations. Rare properties are often important, but pose a challenge for simulation-based approaches: the relative error of the estimate is unbounded. A key objective for statistical model checking rare events is thus to reduce the variance of the estimator. Importance splitting achieves this by estimating a sequence of conditional probabilities, whose product is the required result. To apply this idea to model checking it is necessary to define a score function based on logical properties, and a set of levels that delimit the conditional probabilities.
In this paper we motivate the use of importance splitting for statistical model checking and describe the necessary and desirable properties of score functions and levels. We illustrate how a score function may be derived from a property and give two importance splitting algorithms: one that uses fixed levels and one that discovers optimal levels adaptively.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Baier, C., Katoen, J.-P.: Principles of Model Checking. Representation and Mind Series. MIT Press (2008)
Barbot, B., Haddad, S., Picaronny, C.: Coupling and importance sampling for statistical model checking. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 331–346. Springer, Heidelberg (2012)
Cérou, F., Del Moral, P., Furon, T., Guyader, A.: Sequential Monte Carlo for rare event estimation. Statistics and Computing 22, 795–808 (2012)
Cérou, F., Guyader, A.: Adaptive multilevel splitting for rare event analysis. Stochastic Analysis and Applications 25, 417–443 (2007)
Chernoff, H.: A Measure of Asymptotic Efficiency for Tests of a Hypothesis Based on the sum of Observations. Ann. Math. Statist. 23(4), 493–507 (1952)
Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)
Del Moral, P.: Feynman-Kac Formulae: Genealogical and Interacting Particle Systems with Applications. Probability and Its Applications. Springer (2004)
Dijkstra, E.W.: Hierarchical ordering of sequential processes. Acta Informatica 1, 115–138 (1971)
Gillespie, D.T.: Exact stochastic simulation of coupled chemical reactions. Journal of Physical Chemistry 81, 2340–2361 (1977)
Glasserman, P., Heidelberger, P., Shahabuddin, P., Zajic, T.: Multilevel splitting for estimating rare event probabilities. Oper. Res. 47(4), 585–600 (1999)
Jegourel, C., Legay, A., Sedwards, S.: A Platform for High Performance Statistical Model Checking – PLASMA. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 498–503. Springer, Heidelberg (2012)
Jegourel, C., Legay, A., Sedwards, S.: Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 327–342. Springer, Heidelberg (2012)
Kahn, H.: Random sampling (Monte Carlo) techniques in neutron attenuation problems. Nucleonics 6(5), 27 (1950)
Kahn, H., Harris, T.E.: Estimation of Particle Transmission by Random Sampling. In: Applied Mathematics. series 12, vol. 5, National Bureau of Standards (1951)
Kahn, H., Marshall, A.W.: Methods of Reducing Sample Size in Monte Carlo Computations. Operations Research 1(5), 263–278 (1953)
Lehmann, D., Rabin, M.O.: On the Advantage of Free Choice: A Symmetric and Fully Distributed Solution to the Dining Philosophers Problem (Extended Abstract). In: Proc. 8th Ann. Symposium on Principles of Programming Languages, pp. 133–138 (1981)
Metropolis, N., Ulam, S.: The Monte Carlo Method. Journal of the American Statistical Association 44(247), 335–341 (1949)
Reijsbergen, D., de Boer, P.-T., Scheinhardt, W., Haverkort, B.: Rare event simulation for highly dependable systems with fast repairs. Performance Evaluation 69(7-8), 336–355 (2012)
Ridder, A.: Importance sampling simulations of markovian reliability systems using cross-entropy. Annals of Operations Research 134, 119–136 (2005)
Rosenbluth, M.N., Rosenbluth, A.W.: Monte Carlo Calculation of the Average Extension of Molecular Chains. Journal of Chemical Physics 23(2) (February 1955)
Shahabuddin, P.: Importance Sampling for the Simulation of Highly Reliable Markovian Systems. Management Science 40(3), 333–352 (1994)
Villén-Altamirano, M., Villén-Altamirano, J.: RESTART: A Method for Accelerating Rare Event Simulations. In: Cohen, J.W., Pack, C.D. (eds.) Queueing, Performance and Control in ATM, pp. 71–76. Elsevier (1991)
Wald, A.: Sequential Tests of Statistical Hypotheses. The Annals of Mathematical Statistics 16(2), 117–186 (1945)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jegourel, C., Legay, A., Sedwards, S. (2013). Importance Splitting for Statistical Model Checking Rare Properties. In: Sharygina, N., Veith, H. (eds) Computer Aided Verification. CAV 2013. Lecture Notes in Computer Science, vol 8044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39799-8_38
Download citation
DOI: https://doi.org/10.1007/978-3-642-39799-8_38
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39798-1
Online ISBN: 978-3-642-39799-8
eBook Packages: Computer ScienceComputer Science (R0)