Abstract
Statistical model-checking is an alternative verification technique applied on stochastic systems whose size is beyond numerical analysis ability. Given a model (most often a Markov chain) and a formula, it provides a confidence interval for the probability that the model satisfies the formula. One of the main limitations of the statistical approach is the computation time explosion triggered by the evaluation of very small probabilities. In order to solve this problem we develop a new approach based on importance sampling and coupling. The corresponding algorithms have been implemented in our tool cosmos. We present experimentation on several relevant systems, with estimated time reductions reaching a factor of 10− 120.
Chapter PDF
Similar content being viewed by others
References
Amparore, E.G., Donatelli, S.: Model checking CSL\(^{\mbox{TA}}\) with deterministic and stochastic Petri nets. In: DSN, pp. 605–614 (2010)
Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Software Eng. 29(6), 524–541 (2003)
Bain, L.J., Engelhardt, M.: Introduction to Probability and Mathematical Statistics, 2nd edn. Duxbury Classic Series (1991)
Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: HASL: An expressive language for statistical verification of stochastic models. In: VALUETOOLS 2011, Cachan, France (May 2011) (to appear)
Barbot, B., Haddad, S., Picaronny, C.: Échantillonnage préférentiel pour le model checking statistique. In: MSR 2011. Journal Européen des Systèmes Automatisés, vol. 45, pp. 237–252 (2011)
Barbot, B., Haddad, S., Picaronny, C.: Coupling and importance sampling for statistical model checking. Research Report LSV-12-01, Laboratoire Spécification et Vérification. ENS Cachan, France (January 2012)
Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL - a tool suite for automatic verification of real-time systems. In: Hybrid Systems, pp. 232–243 (1995)
Chiola, G., Franceschinis, G., Gaeta, R., Ribaudo, M.: GreatSPN 1.7: Graphical editor and analyzer for timed and stochastic Petri nets. Perform. Eval. 24(1-2), 47–68 (1995)
Ciesinski, F., Baier, C.: LiQuor: A tool for qualitative and quantitative linear time analysis of reactive systems. In: QEST 2006, pp. 131–132 (2006)
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)
de Boer, P.-T.: Analysis of state-independent importance-sampling measures for the two-node tandem queue. ACM Trans. Model. Comput. Simul. 16(3), 225–250 (2006)
Dupuis, P., Sezer, A.D., Wang, H.: Dynamic importance sampling for queueing networks. Annals of Applied Probability 17, 1306–1346 (2007)
Emerson, E.A., Clarke, E.M.: Characterizing Correctness Properties of Parallel Programs Using Fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 169–181. Springer, Heidelberg (1980)
Glynn, P.W., Iglehart, D.L.: Importance sampling for stochastic simulations. Management Science (1989)
Heegaard, P.E., Sandmann, W.: Ant-based approach for determining the change of measure in importance sampling. In: Winter Simulation Conference, pp. 412–420 (2007)
Katoen, J.-P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. In: International Conference on Quantitative Evaluation of Systems, pp. 167–176 (2009)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic Symbolic Model Checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 113–140. Springer, Heidelberg (2002)
Kwiatkowska, M., Norman, G., Parker, D.: Stochastic Model Checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007)
L’Ecuyer, P., Demers, V., Tuffin, B.: Splitting for rare-event simulation. In: Winter Simulation Conference, pp. 137–148 (2006)
Legay, A., Delahaye, B., Bensalem, S.: Statistical Model Checking: An Overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010)
Lindvall, T.: Lectures on the coupling method. Dover (2002)
Rubino, G., Tuffin, B.: Rare Event Simulation using Monte Carlo Methods. Wiley (2009)
Sen, K., Viswanathan, M., Agha, G.: VESTA: A statistical model-checker and analyzer for probabilistic systems. In: QEST, pp. 251–252 (2005)
Srinivasan, R.: Importance sampling – Applications in communications and detection. Springer, Berlin (2002)
Younes, H.L.S.: Ymer: A Statistical Model Checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 429–433. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barbot, B., Haddad, S., Picaronny, C. (2012). Coupling and Importance Sampling for Statistical Model Checking. In: Flanagan, C., König, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2012. Lecture Notes in Computer Science, vol 7214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28756-5_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-28756-5_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28755-8
Online ISBN: 978-3-642-28756-5
eBook Packages: Computer ScienceComputer Science (R0)