Abstract
Statistical Model Checking (SMC) is an approximate verification method that overcomes the state space explosion problem for probabilistic systems by Monte Carlo simulations. Simulations might be however costly if many samples are required. It is thus necessary to implement efficient algorithms to reduce the sample size while preserving precision and accuracy. In the literature, some sequential schemes have been provided for the estimation of property occurrence based on predefined confidence and absolute or relative error. Nevertheless, these algorithms remain conservative and may result in huge sample sizes if the required precision standards are demanding. In this article, we compare some useful bounds and some sequential methods based on frequentist estimations. We propose outperforming and rigorous alternative schemes, based on Massart bounds and robust confidence intervals. Our theoretical and empirical analysis show that our proposal reduces the sample size while providing guarantees on error bounds.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The Okamoto bound is sometimes called the Chernoff bound in the literature.
- 2.
At least here: http://sav.sutd.edu.sg/publications/.
- 3.
References
Angluin, D., Valiant, L.: Fast probabilistic algorithms for Hamiltonian circuits and matchings. J. Comput. Syst. Sci. 18(2), 155–193 (1979)
Brown, L., Cai, T., DasGupta, A.: Interval estimation for a binomial proportion. Stat. Sci. 16(2), 101–133 (2001)
Chen, J.: Properties of a new adaptive sampling method with applications to scalable learning. In: WI, pp. 9–15, Atlanta (2013)
Chernoff, H.: A measure of asymptotic efficiency for tests of a hypothesis based on the sum of observations. Ann. Math. Stat. 23(4), 493–507 (1952)
Clarke, E.M., Zuliani, P.: Statistical model checking for cyber-physical systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 1–12. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24372-1_1
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)
Dagum, P., Karp, R., Luby, M., Ross, S.: An optimal algorithm for Monte Carlo estimation. SIAM J. Comput. 29(5), 1484–1496 (2000)
David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Uppaal SMC tutorial. STTT 17(4), 397–415 (2015)
Frey, J.: Fixed-width sequential confidence intervals for a proportion. Am. Stat. 64(3), 242–249 (2010)
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). doi:10.1007/978-3-662-45231-8_16
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). doi:10.1007/978-3-540-24622-0_8
Hérault, T., Lassaigne, R., Peyronnet, S.: APMC 3.0: approximate verification of discrete and continuous time Markov chains. In: QEST, pp. 129–130 (2006)
Hoeffding, W.: Probability inequalities for sums of bounded random variables. J. Am. Stat. Assoc. 58(301), 13–30 (1963)
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). doi:10.1007/978-3-642-28756-5_37
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). doi:10.1007/978-3-642-39799-8_38
Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 2.0: a tool for probabilistic model checking. In: QEST, pp. 322–323. IEEE (2004)
Massart, P.: The tight constant in the Dvoretzky-Kiefer-Wolfowitz inequality. Ann. Prob. 18, 1269–1283 (1990)
Metropolis, N., Ulam, S.: The Monte Carlo method. J. Am. Stat. Assoc. 44(247), 335–341 (1949)
Okamoto, M.: Some inequalities relating to the partial sum of binomial probabilities. Ann. Inst. Statis. Math. 10, 29–35 (1958)
Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117–186 (1945)
Watanabe, O.: Sequential sampling techniques for algorithmic learning theory. Theoret. Comput. Sci. 348, 3–14 (2005)
Younes, H.: Verification and planning for stochastic processes with asynchronous events. Ph.D. thesis, Carnegie Mellon University (2004)
Younes, H.L.S., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking: an empirical study. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 46–60. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24730-2_4
Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to stateflow/simulink verification. FMSD 43(2), 338–367 (2013)
Acknowledgements
Cyrille Jegourel and Jun Sun are partially supported by NRF grant GNRF1501 and Jin Song Dong by the project: Reliable Prototyping Framework for Daily Living Assistance of Frail Ageing People (RELIANCE).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Jegourel, C., Sun, J., Dong, J.S. (2017). Sequential Schemes for Frequentist Estimation of Properties in Statistical Model Checking. In: Bertrand, N., Bortolussi, L. (eds) Quantitative Evaluation of Systems. QEST 2017. Lecture Notes in Computer Science(), vol 10503. Springer, Cham. https://doi.org/10.1007/978-3-319-66335-7_23
Download citation
DOI: https://doi.org/10.1007/978-3-319-66335-7_23
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66334-0
Online ISBN: 978-3-319-66335-7
eBook Packages: Computer ScienceComputer Science (R0)