On the Sequential Massart Algorithm for Statistical Model Checking

  • Cyrille JegourelEmail author
  • Jun Sun
  • Jin Song Dong
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11245)


Several schemes have been provided in Statistical Model Checking (SMC) for the estimation of property occurrence based on predefined confidence and absolute or relative error. Simulations might be however costly if many samples are required and the usual algorithms implemented in statistical model checkers tend to be conservative. Bayesian and rare event techniques can be used to reduce the sample size but they can not be applied without prerequisite or knowledge about the system under scrutiny. Recently, sequential algorithms based on Monte Carlo estimations and Massart bounds have been proposed to reduce the sample size while providing guarantees on error bounds which has been shown to outperform alternative frequentist approaches [15]. In this work, we discuss some features regarding the distribution and the optimisation of these algorithms.



This work was supported in part by the National Research Foundation (NRF), Prime Minister’s Office, Singapore, under its National Cybersecurity R&D Programme (Award No. NRF2014NCR-NCR001-040) and administered by the National Cybersecurity R&D Directorate.


  1. 1.
    Agresti, A., Caffo, B.: Simple and effective confidence intervals for proportions and differences of proportions result from adding two successes and two failures. Am. Stat. 54(4), 280–288 (2000)MathSciNetzbMATHGoogle Scholar
  2. 2.
    Ballarini, P., Barbot, B., Duflot, M., Haddad, S., Pekergin, N.: HASL: a new approach for performance evaluation and model checking from concepts to experimentation. Perform. Eval. 90, 53–77 (2015)CrossRefGoogle Scholar
  3. 3.
    Brown, L., Cai, T., DasGupta, A.: Interval estimation for a binomial proportion. Stat. Sci. 16(2), 101–133 (2001)MathSciNetzbMATHGoogle Scholar
  4. 4.
    Chen, Y., Poskitt, C.M., Sun, J.: Learning from mutants: using code mutation to learn and monitor invariants of a cyber-physical system. In: SP, pp. 648–660 (2018)Google Scholar
  5. 5.
    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)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Clopper, C.J., Pearson, E.S.: The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika 26, 404–413 (1934)CrossRefGoogle Scholar
  7. 7.
    Dagum, P., Karp, R.M., Luby, M., Ross, S.M.: An optimal algorithm for Monte Carlo estimation. SIAM J. Comput. 29(5), 1484–1496 (2000)MathSciNetCrossRefGoogle Scholar
  8. 8.
    David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Uppaal SMC tutorial. STTT 17(4), 397–415 (2015)CrossRefGoogle Scholar
  9. 9.
    Grosu, R., Peled, D., Ramakrishnan, C.R., Smolka, S.A., Stoller, S.D., Yang, J.: Using statistical model checking for measuring systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 223–238. Springer, Heidelberg (2014). Scholar
  10. 10.
    Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73–84. Springer, Heidelberg (2004). Scholar
  11. 11.
    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). Scholar
  12. 12.
    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). Scholar
  13. 13.
    Jegourel, C., Legay, A., Sedwards, S.: Command-based importance sampling for statistical model checking. Theor. Comput. Sci. 649, 1–24 (2016)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Jegourel, C., Sun, J., Dong, J.S.: Sequential schemes for frequentist estimation of properties in statistical model checking (Journal version). Currently submittedGoogle Scholar
  15. 15.
    Jegourel, C., Sun, J., Dong, J.S.: Sequential schemes for frequentist estimation of properties in statistical model checking. In: Bertrand, N., Bortolussi, L. (eds.) QEST 2017. LNCS, vol. 10503, pp. 333–350. Springer, Cham (2017). Scholar
  16. 16.
    Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 2.0: a tool for probabilistic model checking. In: QEST, pp. 322–323. IEEE (2004)Google Scholar
  17. 17.
    Massart, P.: The tight constant in the Dvoretzky-Kiefer-Wolfowitz inequality. Ann. Probab. 18, 1269–1283 (1990)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Metropolis, N., Ulam, S.: The Monte Carlo method. J. Am. Stat. Assoc. 44(247), 335–341 (1949)CrossRefGoogle Scholar
  19. 19.
    Okamoto, M.: Some inequalities relating to the partial sum of binomial probabilities. Ann. Inst. Stat. Math. 10, 29–35 (1958)MathSciNetCrossRefGoogle Scholar
  20. 20.
    Samuels, M.L., Witmer, J.W.: Statistics for the Life Sciences, 2nd edn. Prentice Hall, Englewood Cliffs (1999)Google Scholar
  21. 21.
    Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117–186 (1945)MathSciNetCrossRefGoogle Scholar
  22. 22.
    Younes, H.: Verification and planning for stochastic processes with asynchronous events. Ph.D. thesis, Carnegie Mellon University (2004)Google Scholar
  23. 23.
    Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to stateflow/simulink verification. FMSD 43(2), 338–367 (2013)zbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Singapore University of Technology and DesignSingaporeSingapore
  2. 2.Griffith UniversityMount GravattAustralia

Personalised recommendations