Rare Events for Statistical Model Checking an Overview

  • Axel Legay
  • Sean Sedwards
  • Louis-Marie TraonouezEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9899)


This invited paper surveys several simulation-based approa-ches to compute the probability of rare bugs in complex systems. The paper also describes how those techniques can be implemented in the professional toolset Plasma.


Model Check Score Function Importance Sampling Leader Election Markov Jump Process 
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.


  1. 1.
    Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Baier, C., Katoen, J.-P.: Principles of Model Checking. Representation and Mind Series. The MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  3. 3.
    Boyer, B., Corre, K., Legay, A., Sedwards, S.: PLASMA-lab: a flexible, distributable statistical model checking library. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 160–164. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  4. 4.
    Cérou, F., Del Moral, P., Furon, T., Guyader, A.: Sequential Monte Carlo for rare event estimation. Stat. Comput. 22, 795–808 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Cérou, F., Guyader, A.: Adaptive multilevel splitting for rare event analysis. Stoch. Anal. Appl. 25, 417–443 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Clarke, E., Emerson, E.A., Sifakis, J.: Model checking: algorithmic verification and debugging. Commun. ACM 52(11), 74–84 (2009)CrossRefGoogle Scholar
  7. 7.
    Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  8. 8.
    David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., van Vliet, J., Wang, Z.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 80–96. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  9. 9.
    Del Moral, P.: Feynman-Kac Formulae: Genealogical and Interacting Particle Systems with Applications. Probability and Its Applications. Springer, New York (2004)CrossRefzbMATHGoogle Scholar
  10. 10.
    Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Inf. Comput. 88(1), 60–87 (1990)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    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)CrossRefGoogle Scholar
  13. 13.
    Jegourel, C., Legay, A., Sedwards, S.: Importance splitting for statistical model checking rare properties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 576–591. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  14. 14.
    Jegourel, C., Legay, A., Sedwards, S.: An Effective Heuristic for Adaptive Importance Splitting in Statistical Model Checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part II. LNCS, vol. 8803, pp. 143–159. Springer, Heidelberg (2014)Google Scholar
  15. 15.
    Jegourel, C., Legay, A., Sedwards, S., Traonouez, L.-M.: Distributed verification of rare properties using importance splitting observers. In: ECEASST, vol. 72 (2015)Google Scholar
  16. 16.
    Kahn, H.: Stochastic (Monte Carlo) attenuation analysis. Technical report P-88, Rand Corporation, July 1949Google Scholar
  17. 17.
    Kahn, H.: Random sampling (Monte Carlo) techniques in neutron attenuation problems. Nucleonics 6(5), 27 (1950)Google Scholar
  18. 18.
    Kahn, H., Harris, T.E.: Estimation of particle transmission by random sampling. In: Applied Mathematics. Series 12, vol. 5. National Bureau of Standards (1951)Google Scholar
  19. 19.
    Kahn, H., Marshall, A.W.: Methods of reducing sample size in Monte Carlo computations. Oper. Res. 1(5), 263–278 (1953)Google Scholar
  20. 20.
    Lehmann, D., Rabin, M.O.: On the advantage of free choice: a symmetric and fully distributed solution to the dining philosophers problem. In: Proceedings of the 8th Annual Symposium on Principles of Programming Languages, pp. 133–138 (1981)Google Scholar
  21. 21.
    Maler, O., Larsen, K.G., Krogh, B.H.: On zone-based analysis of duration probabilistic automata. In: 12th International Workshop on Verification of Infinite-State Systems (INFINITY), pp. 33–46 (2010)Google Scholar
  22. 22.
    Okamoto, M.: Some inequalities relating to the partial sum of binomial probabilities. Ann. Inst. Stat. Math. 10, 29–35 (1959)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Ridder, A.: Importance sampling simulations of markovian reliability systems using cross-entropy. Ann. Oper. Res. 134, 119–136 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Rosenbluth, M.N., Rosenbluth, A.W.: Monte Carlo calculation of the average extension of molecular chains. J. Chem. Phys. 23(2) (1955)Google Scholar
  25. 25.
    Rubinstein, R.: The cross-entropy method for combinatorial and continuous optimization. In: Methodology and Computing in Applied Probability, vol. 1, pp. 127–190. Kluwer Academic (1999)Google Scholar
  26. 26.
    Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117–186 (1945)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • Axel Legay
    • 1
  • Sean Sedwards
    • 1
  • Louis-Marie Traonouez
    • 1
    Email author
  1. 1.Inria Rennes – Bretagne AtlantiqueRennesFrance

Personalised recommendations