Advertisement

Lightweight Statistical Model Checking in Nondeterministic Continuous Time

  • Pedro R. D’Argenio
  • Arnd HartmannsEmail author
  • Sean Sedwards
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11245)

Abstract

Lightweight scheduler sampling brings statistical model checking to nondeterministic formalisms with undiscounted properties, in constant memory. Its direct application to continuous-time models is rendered ineffective by their dense concrete state spaces and the need to consider continuous input for optimal decisions. In this paper we describe the challenges and state of the art in applying lightweight scheduler sampling to three continuous-time formalisms: After a review of recent work on exploiting discrete abstractions for probabilistic timed automata, we discuss scheduler sampling for Markov automata and apply it on two case studies. We provide further insights into the tradeoffs between scheduler classes for stochastic automata. Throughout, we present extended experiments and new visualisations of the distribution of schedulers.

Notes

Acknowledgments

The authors thank Yuliya Butkova (Saarland University) for clarifying discussions on uniformisation and the time-bounded analysis of MA.

References

  1. 1.
    Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994).  https://doi.org/10.1016/0304-3975(94)90010-8MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-27755-2_3CrossRefzbMATHGoogle Scholar
  3. 3.
    Bohlender, D., Bruintjes, H., Junges, S., Katelaan, J., Nguyen, V.Y., Noll, T.: A review of statistical model checking pitfalls on real-time stochastic models. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 177–192. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-45231-8_13CrossRefGoogle Scholar
  4. 4.
    Brázdil, T.: Verification of Markov decision processes using learning algorithms. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 98–114. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-11936-6_8CrossRefGoogle Scholar
  5. 5.
    Budde, C.E., D’Argenio, P.R., Hartmanns, A.: Better automated importance splitting for transient rare events. In: Larsen, K.G., Sokolsky, O., Wang, J. (eds.) SETTA 2017. LNCS, vol. 10606, pp. 42–58. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-69483-2_3CrossRefGoogle Scholar
  6. 6.
    Budde, C.E., DArgenio, P.R., Hartmanns, A., Sedwards, S.: A statistical model checker for nondeterminism and rare events. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 340–358. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89963-3_20CrossRefGoogle Scholar
  7. 7.
    Butkova, Y., Hatefi, H., Hermanns, H., Krčál, J.: Optimal continuous time Markov decisions. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 166–182. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-24953-7_12CrossRefGoogle Scholar
  8. 8.
    D’Argenio, P.R., Gerhold, M., Hartmanns, A., Sedwards, S.: A hierarchy of scheduler classes for stochastic automata. In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 384–402. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89366-2_21CrossRefzbMATHGoogle Scholar
  9. 9.
    D’Argenio, P.R., Hartmanns, A., Legay, A., Sedwards, S.: Statistical approximation of optimal schedulers for probabilistic timed automata. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 99–114. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-33693-0_7CrossRefGoogle Scholar
  10. 10.
    D’Argenio, P.R., Katoen, J.P.: A theory of stochastic systems part I: stochastic automata. Inf. Comput. 203(1), 1–38 (2005).  https://doi.org/10.1016/j.ic.2005.07.001CrossRefzbMATHGoogle Scholar
  11. 11.
    D’Argenio, P.R., Legay, A., Sedwards, S., Traonouez, L.M.: Smart sampling for lightweight verification of Markov decision processes. Softw. Tools Technol. Transf. 17(4), 469–484 (2015).  https://doi.org/10.1007/s10009-015-0383-0CrossRefGoogle Scholar
  12. 12.
    David, A., Jensen, P.G., Larsen, K.G., Mikučionis, M., Taankvist, J.H.: Uppaal Stratego. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 206–211. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46681-0_16CrossRefGoogle Scholar
  13. 13.
    David, A., Larsen, K.G., Legay, A., Mikučionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 349–355. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_27CrossRefGoogle Scholar
  14. 14.
    Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342–351. IEEE Computer Society (2010).  https://doi.org/10.1109/LICS.2010.41
  15. 15.
    Fehnker, A., Chaudhary, K.: Twenty percent and a few days – optimising a Bitcoin majority attack. In: Dutle, A., Muñoz, C., Narkawicz, A. (eds.) NFM 2018. LNCS, vol. 10811, pp. 157–163. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-77935-5_11CrossRefGoogle Scholar
  16. 16.
    Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53–113. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-21455-4_3CrossRefGoogle Scholar
  17. 17.
    Guck, D., Hatefi, H., Hermanns, H., Katoen, J.-P., Timmer, M.: Modelling, reduction and analysis of Markov automata. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 55–71. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-40196-1_5CrossRefGoogle Scholar
  18. 18.
    Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.P.: A compositional modelling and analysis framework for stochastic hybrid systems. Form. Methods Syst. Des. 43(2), 191–232 (2013).  https://doi.org/10.1007/s10703-012-0167-zCrossRefzbMATHGoogle Scholar
  19. 19.
    Hartmanns, A.: Lightweight statistical model checking in nondeterministic continuous time (artifact). 4TU.Centre for Research Data (2018).  https://doi.org/10.4121/uuid:1453a13b-10ae-418f-a1ae-4acf96028118
  20. 20.
    Hartmanns, A., Hermanns, H.: The Modest Toolset: an integrated environment for quantitative modelling and verification. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 593–598. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54862-8_51CrossRefGoogle Scholar
  21. 21.
    Hartmanns, A., Hermanns, H., Krčál, J.: Schedulers are no Prophets. In: Probst, C.W., Hankin, C., Hansen, R.R. (eds.) Semantics, Logics, and Calculi. LNCS, vol. 9560, pp. 214–235. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-27810-0_11CrossRefGoogle Scholar
  22. 22.
    Hartmanns, A., Sedwards, S., D’Argenio, P.R.: Efficient simulation-based verification of probabilistic timed automata. In: Winter Simulation Conference, pp. 1419–1430. IEEE (2017).  https://doi.org/10.1109/WSC.2017.8247885
  23. 23.
    Hatefi, H., Hermanns, H.: Model checking algorithms for Markov automata. Electron. Commun. EASST 53 (2012) .  https://doi.org/10.14279/tuj.eceasst.53.783
  24. 24.
    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).  https://doi.org/10.1007/978-3-540-24622-0_8CrossRefzbMATHGoogle Scholar
  25. 25.
    Kearns, M.J., Mansour, Y., Ng, A.Y.: A sparse sampling algorithm for near-optimal planning in large Markov decision processes. Mach. Learn. 49(2–3), 193–208 (2002).  https://doi.org/10.1023/A:1017932429737CrossRefzbMATHGoogle Scholar
  26. 26.
    Kroese, D.P., Nicola, V.F.: Efficient estimation of overflow probabilities in queues with breakdowns. Perform. Eval. 36, 471–484 (1999)CrossRefGoogle Scholar
  27. 27.
    Kurkowski, S., Camp, T., Colagrosso, M.: MANET simulation studies: the incredibles. Mob. Comput. Commun. Rev. 9(4), 50–61 (2005).  https://doi.org/10.1145/1096166.1096174CrossRefGoogle Scholar
  28. 28.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_47CrossRefGoogle Scholar
  29. 29.
    Kwiatkowska, M.Z., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282(1), 101–150 (2002).  https://doi.org/10.1016/S0304-3975(01)00046-9MathSciNetCrossRefzbMATHGoogle Scholar
  30. 30.
    Legay, A., Sedwards, S., Traonouez, L.-M.: Scalable verification of Markov decision processes. In: Canal, C., Idani, A. (eds.) SEFM 2014. LNCS, vol. 8938, pp. 350–362. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-15201-1_23CrossRefGoogle Scholar
  31. 31.
    Okamoto, M.: Some inequalities relating to the partial sum of binomial probabilities. Ann. Inst. Stat. Math. 10(1), 29–35 (1959)MathSciNetCrossRefGoogle Scholar
  32. 32.
    Reijsbergen, D., de Boer, P., Scheinhardt, W.R.W., Haverkort, B.R.: On hypothesis testing for statistical model checking. Softw. Tools Technol. Transf. 17(4), 377–395 (2015).  https://doi.org/10.1007/s10009-014-0350-1CrossRefGoogle Scholar
  33. 33.
    Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223–235. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45657-0_17CrossRefzbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Universidad Nacional de CórdobaCórdobaArgentina
  2. 2.CONICETCórdobaArgentina
  3. 3.Saarland UniversitySaarbrückenGermany
  4. 4.University of TwenteEnschedeThe Netherlands
  5. 5.University of WaterlooWaterlooCanada

Personalised recommendations