Advertisement

Modelling, Reduction and Analysis of Markov Automata

  • Dennis Guck
  • Hassan Hatefi
  • Holger Hermanns
  • Joost-Pieter Katoen
  • Mark Timmer
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8054)

Abstract

Markov automata (MA) constitute an expressive continuous-time compositional modelling formalism. They appear as semantic backbones for engineering frameworks including dynamic fault trees, Generalised Stochastic Petri Nets, and AADL. Their expressive power has thus far precluded them from effective analysis by probabilistic (and statistical) model checkers, stochastic game solvers, or analysis tools for Petri net-like formalisms. This paper presents the foundations and underlying algorithms for efficient MA modelling, reduction using static analysis, and most importantly, quantitative analysis. We also discuss implementation pragmatics of supporting tools and present several case studies demonstrating feasibility and usability of MA in practice.

Keywords

Goal State Polling System Markov State Markovian Transition Fault Tree Analysis 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE TSE 29(6), 524–541 (2003)Google Scholar
  2. 2.
    Bertsekas, D.P., Tsitsiklis, J.N.: An analysis of stochastic shortest path problems. Mathematics of Operations Research 16(3), 580–595 (1991)MathSciNetzbMATHCrossRefGoogle Scholar
  3. 3.
    Boudali, H., Crouzen, P., Stoelinga, M.I.A.: A rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE Trans. Dependable Sec. Comput. 7(2), 128–143 (2010)CrossRefGoogle Scholar
  4. 4.
    Bozzano, M., Cimatti, A., Katoen, J.-P., Nguyen, V.Y., Noll, T., Roveri, M.: Safety, dependability and performance analysis of extended AADL models. The Computer Journal 54(5), 754–775 (2011)CrossRefGoogle Scholar
  5. 5.
    Chatterjee, K., Henzinger, M.: Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In: SODA, pp. 1318–1336. SIAM (2011)Google Scholar
  6. 6.
    Coste, N., Hermanns, H., Lantreibecq, E., Serwe, W.: Towards performance prediction of compositional models in industrial GALS designs. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 204–218. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  7. 7.
    de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford University (1997)Google Scholar
  8. 8.
    de Alfaro, L.: How to specify and verify the long-run average behavior of probabilistic systems. In: LICS, pp. 454–465. IEEE (1998)Google Scholar
  9. 9.
    de Alfaro, L.: Computing minimum and maximum reachability times in probabilistic systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 66–81. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  10. 10.
    Deng, Y., Hennessy, M.: On the semantics of Markov automata. Inf. Comput. 222, 139–168 (2013)MathSciNetzbMATHCrossRefGoogle Scholar
  11. 11.
    Eisentraut, C., Hermanns, H., Katoen, J.-P., Zhang, L.: A semantics for every GSPN. In: Colom, J.-M., Desel, J. (eds.) ICATPN 2013. LNCS, vol. 7927, pp. 90–109. Springer, Heidelberg (2013)Google Scholar
  12. 12.
    Eisentraut, C., Hermanns, H., Zhang, L.: Concurrency and composition in a stochastic world. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 21–39. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  13. 13.
    Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342–351. IEEE (2010)Google Scholar
  14. 14.
    Guck, D., Han, T., Katoen, J.-P., Neuhäußer, M.R.: Quantitative timed analysis of interactive Markov chains. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 8–23. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  15. 15.
    Guck, D., Hatefi, H., Hermanns, H., Katoen, J.-P., Timmer, M.: Modelling, reduction and analysis of Markov automata (extended version). Technical Report 1305.7050, ArXiv e-prints (2013)Google Scholar
  16. 16.
    Hatefi, H., Hermanns, H.: Model checking algorithms for Markov automata. In: ECEASST (AVoCS proceedings), vol. 53 (2012) (to appear)Google Scholar
  17. 17.
    Haverkort, B.R., Kuntz, M., Remke, A., Roolvink, S., Stoelinga, M.I.A.: Evaluating repair strategies for a water-treatment facility using Arcade. In: DSN, pp. 419–424. IEEE (2010)Google Scholar
  18. 18.
    Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality. LNCS, vol. 2428. Springer, Heidelberg (2002)Google Scholar
  19. 19.
    Katoen, J.-P.: GSPNs revisited: Simple semantics and new analysis algorithms. In: ACSD, pp. 6–11. IEEE (2012)Google Scholar
  20. 20.
    Katoen, J.-P., van de Pol, J.C., Stoelinga, M.I.A., Timmer, M.: A linear process-algebraic format with data for probabilistic automata. TCS 413(1), 36–57 (2012)zbMATHCrossRefGoogle Scholar
  21. 21.
    López, G.G.I., Hermanns, H., Katoen, J.-P.: Beyond memoryless distributions: Model checking semi-markov chains. In: de Luca, L., Gilmore, S. (eds.) PAPM-PROBMIV 2001. LNCS, vol. 2165, pp. 57–70. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  22. 22.
    Ajmone Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. John Wiley & Sons (1995)Google Scholar
  23. 23.
    Ajmone Marsan, M., Conte, G., Balbo, G.: A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems. ACM Transactions on Computer Systems 2(2), 93–122 (1984)CrossRefGoogle Scholar
  24. 24.
    Meyer, J.F., Movaghar, A., Sanders, W.H.: Stochastic activity networks: Structure, behavior, and application. In: PNPM, pp. 106–115. IEEE (1985)Google Scholar
  25. 25.
    Neuhäußer, M.R., Stoelinga, M.I.A., Katoen, J.-P.: Delayed nondeterminism in continuous-time Markov decision processes. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 364–379. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  26. 26.
    Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT (1995)Google Scholar
  27. 27.
    Srinivasan, M.M.: Nondeterministic polling systems. Management Science 37(6), 667–681 (1991)zbMATHCrossRefGoogle Scholar
  28. 28.
    Timmer, M.: SCOOP: A tool for symbolic optimisations of probabilistic processes. In: QEST, pp. 149–150. IEEE (2011)Google Scholar
  29. 29.
    Timmer, M., Katoen, J.-P., van de Pol, J.C., Stoelinga, M.I.A.: Efficient modelling and generation of Markov automata. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 364–379. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  30. 30.
    Timmer, M., Katoen, J.-P., van de Pol, J.C., Stoelinga, M.I.A.: Efficient modelling and generation of Markov automata (extended version). Technical Report TR-CTIT-12-16, CTIT, University of Twente (2012)Google Scholar
  31. 31.
    Timmer, M., van de Pol, J.C., Stoelinga, M.I.A.: Confluence reduction for markov automata. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 240–254. Springer, Heidelberg (2013)Google Scholar
  32. 32.
    van de Pol, J.C., Timmer, M.: State space reduction of linear processes using control flow reconstruction. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 54–68. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  33. 33.
    Zhang, L., Neuhäußer, M.R.: Model checking interactive markov chains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 53–68. Springer, Heidelberg (2010)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Dennis Guck
    • 1
    • 3
  • Hassan Hatefi
    • 2
  • Holger Hermanns
    • 2
  • Joost-Pieter Katoen
    • 1
    • 3
  • Mark Timmer
    • 3
  1. 1.Software Modelling and VerificationRWTH Aachen UniversityGermany
  2. 2.Dependable Systems and SoftwareSaarland UniversityGermany
  3. 3.Formal Methods and ToolsUniversity of TwenteThe Netherlands

Personalised recommendations