Advertisement

Accelerated Model Checking of Parametric Markov Chains

  • Paul Gainer
  • Ernst Moritz HahnEmail author
  • Sven Schewe
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11138)

Abstract

Parametric Markov chains occur quite naturally in various applications: they can be used for a conservative analysis of probabilistic systems (no matter how the parameter is chosen, the system works to specification); they can be used to find optimal settings for a parameter; they can be used to visualise the influence of system parameters; and they can be used to make it easy to adjust the analysis for the case that parameters change. Unfortunately, these advancements come at a cost: parametric model checking is—or rather was—often slow. To make the analysis of parametric Markov models scale, we need three ingredients: clever algorithms, the right data structure, and good engineering. Clever algorithms are often the main (or sole) selling point; and we face the trouble that this paper focuses on – the latter ingredients to efficient model checking. Consequently, our easiest claim to fame is in the speed-up we have often realised when comparing to the state of the art.

References

  1. 1.
    Baier, C., Klein, J., Leuschner, L., Parker, D., Wunderlich, S.: Ensuring the reliability of your model checker: interval iteration for Markov decision processes. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 160–180. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63387-9_8CrossRefGoogle Scholar
  2. 2.
    Bloem, R., et al.: Synthesizing robust systems. Acta Inf. 51(3–4), 193–220 (2014)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Calinescu, R., Ghezzi, C., Kwiatkowska, M., Mirandola, R.: Self-adaptive software needs quantitative verification at runtime. CACM 55(9), 69–77 (2012)CrossRefGoogle Scholar
  4. 4.
    Cox, D.R.: Renewal Theory. Methuen & Co., Ltd, London (1967)Google Scholar
  5. 5.
    Cubuktepe, M., et al.: Sequential convex programming for the efficient verification of parametric MDPs. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 133–150. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54580-5_8CrossRefGoogle Scholar
  6. 6.
    Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 280–294. Springer, Heidelberg (2005).  https://doi.org/10.1007/978-3-540-31862-0_21CrossRefzbMATHGoogle Scholar
  7. 7.
    Jovanović, A., Kwiatkowska, M.: Parameter synthesis for probabilistic timed automata using stochastic game abstractions. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 176–189. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-11439-2_14CrossRefGoogle Scholar
  8. 8.
    Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592–600. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63390-9_31CrossRefGoogle Scholar
  9. 9.
    DeMillo, R.A., Lipton, R.J.: A probabilistic remark on algebraic program testing. Inf. Process. Lett. 7, 193–195 (1978)CrossRefGoogle Scholar
  10. 10.
    von Essen, C., Jobstmann, B.: Synthesizing systems with optimal average-case behavior for ratio objectives. In: iWIGP, pp. 17–32 (2011)Google Scholar
  11. 11.
    Filieri, A., Ghezzi, C., Tamburrelli, G.: Run-time efficient probabilistic model checking. In: ICSE, pp. 341–350. ACM (2011)Google Scholar
  12. 12.
    Gainer, P., Linker, S., Dixon, C., Hustadt, U., Fisher, M.: Investigating parametric influence on discrete synchronisation protocols using quantitative model checking. In: Bertrand, N., Bortolussi, L. (eds.) QEST 2017. LNCS, vol. 10503, pp. 224–239. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-66335-7_14CrossRefGoogle Scholar
  13. 13.
    Gainer, P., Linker, S., Dixon, C., Hustadt, U., Fisher, M.: The power of synchronisation: formal analysis of power consumption in networks of pulse-coupled oscillators. arXiv preprint arXiv:1709.04385 (2017)
  14. 14.
    Hahn, E.M., Han, T., Zhang, L.: Synthesis for PCTL in parametric Markov decision processes. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 146–161. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-20398-5_12CrossRefGoogle Scholar
  15. 15.
    Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PARAM: a model checker for parametric Markov models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 660–664. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14295-6_56CrossRefGoogle Scholar
  16. 16.
    Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. STTT 13(1), 3–19 (2011)CrossRefGoogle Scholar
  17. 17.
    Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: a web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312–317. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-06410-9_22CrossRefGoogle Scholar
  18. 18.
    Han, Y.S.: State elimination heuristics for short regular expressions. FI 128(4), 445–462 (2013)Google Scholar
  19. 19.
    Han, Y.S., Wood, D.: Obtaining shorter regular expressions from finite-state automata. TCS 370(1–3), 110–120 (2007)MathSciNetCrossRefGoogle Scholar
  20. 20.
    Harbron, C.: Heuristic algorithms for finding inexpensive elimination schemes. SC 5(4), 275–287 (1995)CrossRefGoogle Scholar
  21. 21.
    Helmink, L., Sellink, M.P.A., Vaandrager, F.W.: Proof-checking a data link protocol. In: TYPES, pp. 127–165. Springer, Berlin (1993)Google Scholar
  22. 22.
    Hopcroft, J.E.: Introduction to Automata Theory, Languages, and Computation. Pearson Education India (2008)Google Scholar
  23. 23.
    Ibe, O.C., Trivedi, K.S.: Stochastic Petri net models of polling systems. J-SAC 8(9), 1649–1657 (1990)Google Scholar
  24. 24.
    Knuth, D., Yao, A.: The complexity of nonuniform random number generation. Algorithms and Complexity: New Directions and Recent Results. Academic Press, Orlando (1976)Google Scholar
  25. 25.
    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).  https://doi.org/10.1007/978-3-540-72522-0_6CrossRefGoogle Scholar
  26. 26.
    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
  27. 27.
    Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.-P.: Parameter synthesis for Markov models: faster than ever. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 50–67. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-46520-3_4CrossRefGoogle Scholar
  28. 28.
    Reiter, M.K., Rubin, A.D.: Crowds: anonymity for web transactions. TISSEC 1(1), 66–92 (1998)CrossRefGoogle Scholar
  29. 29.
    Schwartz, J.T.: Fast probabilistic algorithms for verification of polynomial identities. J. ACM 27(4), 701–717 (1980)MathSciNetCrossRefGoogle Scholar
  30. 30.
    Zippel, R.: Probabilistic algorithms for sparse polynomials. In: Ng, E.W. (ed.) Symbolic and Algebraic Computation. LNCS, vol. 72, pp. 216–226. Springer, Heidelberg (1979).  https://doi.org/10.1007/3-540-09519-5_73CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.University of LiverpoolLiverpoolUK

Personalised recommendations