skip to main content
10.1145/2933575.2934574acmconferencesArticle/Chapter ViewAbstractPublication PageslicsConference Proceedingsconference-collections
tutorial

The Probabilistic Model Checking Landscape

Published:05 July 2016Publication History

ABSTRACT

Randomization is a key element in sequential and distributed computing. Reasoning about randomized algorithms is highly non-trivial. In the 1980s, this initiated first proof methods, logics, and model-checking algorithms. The field of probabilistic verification has developed considerably since then. This paper surveys the algorithmic verification of probabilistic models, in particular probabilistic model checking. We provide an informal account of the main models, the underlying algorithms, applications from reliability and dependability analysis---and beyond---and describe recent developments towards automated parameter synthesis.

References

  1. A. Abate, J.-P. Katoen, J. Lygeros, and M. Prandini. Approximate model checking of stochastic hybrid systems. Eur. J. Control, 16(6): 624--641, 2010.Google ScholarGoogle ScholarCross RefCross Ref
  2. P. A. Abdulla, N. B. Henda, and R. Mayr. Decisive Markov chains. Logical Methods in Computer Science, 3(4), 2007.Google ScholarGoogle Scholar
  3. E. Ábrahám, B. Becker, C. Dehnert, N. Jansen, J.-P. Katoen, and R. Wimmer. Counterexample generation for discrete-time Markov models: An introductory survey. In SFM, volume 8483 of LNCS, pages 65--121. Springer, 2014. Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. M. Agrawal, S. Akshay, B. Genest, and P. S. Thiagarajan. Approximate verification of the symbolic dynamics of Markov chains. J. ACM, 62(1):2:1--2:34, 2015. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. S. Akshay, T. Antonopoulos, J. Ouaknine, and J. Worrell. Reachability problems for Markov chains. Inf. Process. Lett., 115(2):155--158, 2015. Google ScholarGoogle ScholarDigital LibraryDigital Library
  6. R. Alur, T. A. Henzinger, and M. Vardi. Theory in practice for system design and verification. ACM SIGLOG News, 3, 2015. Google ScholarGoogle ScholarDigital LibraryDigital Library
  7. E. G. Amparore, G. Balbo, M. Beccuti, S. Donatelli, and G. Franceschinis. 30 years of GreatSPN. In Principles of Performance and Reliability Modeling and Evaluation, Springer Series in Reliability Engineering, pages 227--254. Springer, 2016.Google ScholarGoogle ScholarCross RefCross Ref
  8. S. Andova, H. Hermanns, and J.-P. Katoen. Discrete-time rewards model checked. In FORMATS, volume 2791 of LNCS, pages 88--104. Springer-Verlag, 2003.Google ScholarGoogle Scholar
  9. O. Andrei, M. Calder, M. Chalmers, A. Morrison, and M. Rost. Probabilistic formal analysis of app usage to inform redesign. CoRR, abs/1510.07898, 2015.Google ScholarGoogle Scholar
  10. A. Aziz, K. Sanwal, V. Singhal, and R. K. Brayton. Model-checking continous-time Markov chains. ACM Trans. Comput. Log., 1(1):162--170, 2000. Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. C. Baier and M. Z. Kwiatkowska. Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11(3): 125--155, 1998. Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. C. Baier, E. M. Clarke, V. Hartonas-Garmhausen, M. Z. Kwiatkowska, and M. Ryan. Symbolic model checking for probabilistic processes. In ICALP, volume 1256 of LNCS, pages 430--440. Springer, 1997. Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. C. Baier, B. R. Haverkort, H. Hermanns, and J.-P. Katoen. Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Software Eng., 29(6):524--541, 2003. Google ScholarGoogle ScholarDigital LibraryDigital Library
  15. C. Baier, M. Größer, M. Leucker, B. Bollig, and F. Ciesinski. Controller synthesis for probabilistic systems. In IFIP TCS, volume 155 of IFIP, pages 493--506. Kluwer/Springer, 2004.Google ScholarGoogle Scholar
  16. C. Baier, H. Hermanns, J.-P. Katoen, and B. R. Haverkort. Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theor. Comput. Sci., 345(1):2--26, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. C. Baier, J.-P. Katoen, H. Hermanns, and V. Wolf. Comparative branching-time semantics for Markov chains. Inf. Comput., 200(2): 149--214, 2005. Google ScholarGoogle ScholarCross RefCross Ref
  18. C. Baier, P. R. D'Argenio, and M. Größer. Partial order reduction for probabilistic branching time. Electr. Notes Theor. Comput. Sci., 153 (2):97--116, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. C. Baier, B. R. Haverkort, H. Hermanns, and J.-P. Katoen. Reachability in continuous-time Markov reward decision processes. In Logic and Automata History and Perspectives, volume 2 of Texts in Logic and Games, pages 53--72. Amsterdam University Press, 2008.Google ScholarGoogle Scholar
  20. C. Baier, L. Cloth, B. R. Haverkort, H. Hermanns, and J.-P. Katoen. Performability assessment by model checking of Markov reward models. Formal Methods in System Design, 36(1):1--36, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  21. C. Baier, M. Größer, and N. Bertrand. Probabilistic ω-automata. J. ACM, 59(1):1, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  22. C. Baier, E. M. Hahn, B. R. Haverkort, H. Hermanns, and J.-P. Katoen. Model checking for performability. Mathematical Structures in Computer Science, 23(4):751--795, 2013.Google ScholarGoogle ScholarCross RefCross Ref
  23. C. Baier, C. Dubslaff, and S. Klüppelholz. Trade-off analysis meets probabilistic model checking. In CSL-LICS, pages 1:1--1:10. ACM, 2014. Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. C. Baier, J. Klein, S. Klüppelholz, and S. Märcker. Computing conditional probabilities in Markovian models efficiently. In TACAS, volume 8413 of LNCS, pages 515--530. Springer, 2014.Google ScholarGoogle Scholar
  25. C. Baier, L. de Alfaro, V. Forejt, and M. Kwiatkowska. Probabilistic model checking. In Handbook of Model Checking. Springer, 2016 (to appear).Google ScholarGoogle Scholar
  26. B. Barbot, T. Chen, T. Han, J.-P. Katoen, and A. Mereacre. Efficient CTMC model checking of linear real-time objectives. In TACAS, volume 6605 of LNCS, pages 128--142. Springer, 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  27. F. Bartels, A. Sokolova, and E. P. de Vink. A hierarchy of probabilistic system types. Theor. Comput. Sci., 327(1-2):3--22, 2004. Google ScholarGoogle ScholarDigital LibraryDigital Library
  28. E. Bartocci, R. Grosu, P. Katsaros, C. R. Ramakrishnan, and S. A. Smolka. Model repair for probabilistic systems. In TACAS, volume 6605 of LNCS, pages 326--340. Springer, 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  29. M. D. Beaudry. Performance-related reliability measures for computing systems. IEEE Trans. on Computers, 27(6):540--547, 1978. Google ScholarGoogle ScholarDigital LibraryDigital Library
  30. N. Bertrand, P. Bouyer, T. Brihaye, Q. Menet, C. Baier, M. Größer, and M. Jurdzinski. Stochastic timed automata. Logical Methods in Computer Science, 10(4), 2014.Google ScholarGoogle Scholar
  31. A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In FSTTCS, volume 1026 of LNCS, pages 499--513. Springer-Verlag, 1995. Google ScholarGoogle ScholarDigital LibraryDigital Library
  32. E. Böde, M. Herbstritt, H. Hermanns, S. Johr, T. Peikenkamp, R. Pulungan, J.-H. Rakow, R. Wimmer, and B. Becker. Compositional dependability evaluation for STATEMATE. IEEE Trans. Software Eng., 35(2):274--292, 2009. Google ScholarGoogle ScholarDigital LibraryDigital Library
  33. G. Bolch, S. Greiner, H. de Meer, and K. S. Trivedi. Queueing Networks and Markov Chains: Modeling and Performance Evaluation with Computer Science Applications. Wiley, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  34. L. Bortolussi, J. Hillston, D. Latella, and M. Massink. Continuous approximation of collective system behaviour: A tutorial. Perform. Eval., 70(5):317--349, 2013. Google ScholarGoogle ScholarDigital LibraryDigital Library
  35. D. Bosnacki, S. Edelkamp, D. Sulewski, and A. Wijs. Parallel probabilistic model checking on general purpose graphics processors. STTT, 13(1):21--35, 2011.Google ScholarGoogle ScholarCross RefCross Ref
  36. H. Boudali, P. Crouzen, and M. Stoelinga. A rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE Trans. Dependable Sec. Comput., 7(2):128--143, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  37. M. Bozzano, A. Cimatti, J.-P. Katoen, V. Y. Nguyen, T. Noll, M. Roveri, and R. Wimmer. A model checker for AADL. In CAV, volume 6174 of LNCS, pages 562--565. Springer, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  38. M. Bozzano, A. Cimatti, J.-P. Katoen, V. Y. Nguyen, T. Noll, and M. Roveri. Safety, dependability and performance analysis of extended AADL models. Comput. J., 54(5):754--775, 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  39. M. Bozzano, A. Cimatti, J.-P. Katoen, P. Katsaros, K. Mokos, V. Y. Nguyen, T. Noll, B. Postma, and M. Roveri. Spacecraft early design validation using formal methods. Rel. Eng. & Sys. Safety, 132:20--35, 2014.Google ScholarGoogle ScholarCross RefCross Ref
  40. T. Brázdil, J. Esparza, S. Kiefer, and A. Kucera. Analyzing probabilistic pushdown automata. Formal Methods in System Design, 43 (2):124--163, 2013. Google ScholarGoogle ScholarDigital LibraryDigital Library
  41. T. Brázdil, S. Kiefer, A. Kucera, P. Novotný, and J.-P. Katoen. Zeroreachability in probabilistic multi-counter automata. In CSL-LICS, pages 22:1--22:10. ACM, 2014. Google ScholarGoogle ScholarDigital LibraryDigital Library
  42. V. Bruyère, E. Filiot, M. Randour, and J.-F. Raskin. Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games. In STACS, volume 25 of LIPIcs, pages 199--213. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014.Google ScholarGoogle Scholar
  43. P. Buchholz and I. Schulz. Numerical analysis of continuous time Markov decision processes over finite horizons. Computers & OR, 38(3):651--659, 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  44. Y. Butkova, H. Hatefi, H. Hermanns, and J. Krcál. Optimal continuous time Markov decisions. In ATVA, volume 9364 of LNCS, pages 166--182. Springer, 2015.Google ScholarGoogle Scholar
  45. R. Calinescu, C. Ghezzi, M. Z. Kwiatkowska, and R. Mirandola. Self-adaptive software needs quantitative verification at runtime. Commun. ACM, 55(9):69--77, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  46. M. Ceska, F. Dannenberg, M. Z. Kwiatkowska, and N. Paoletti. Precise parameter synthesis for stochastic biochemical systems. In CMSB, volume 8859 of LNCS, pages 86--98. Springer, 2014.Google ScholarGoogle Scholar
  47. S. Chakraborty and J.-P. Katoen. Parametric LTL on Markov chains. In IFIP TCS, volume 8705 of LNCS, pages 207--221. Springer, 2014.Google ScholarGoogle Scholar
  48. K. Chatterjee and T. A. Henzinger. A survey of stochastic ω-regular games. J. Comput. Syst. Sci., 78(2):394--413, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  49. K. Chatterjee, L. Doyen, and M. Y. Vardi. The complexity of synthesis from probabilistic components. In ICALP (2), volume 9135 of LNCS, pages 108--120. Springer, 2015. Google ScholarGoogle ScholarDigital LibraryDigital Library
  50. K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh. Measuring and synthesizing systems in probabilistic environments. J. ACM, 62(1):9:1--9:34, 2015. Google ScholarGoogle ScholarDigital LibraryDigital Library
  51. D. Chen, F. van Breugel, and J. Worrell. On the complexity of computing probabilistic bisimilarity. In FoSSaCS, volume 7213 of LNCS, pages 437--451. Springer, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  52. T. Chen, T. Han, J.-P. Katoen, and A. Mereacre. Model checking of continuous-time Markov chains against timed automata specifications. Logical Methods in Computer Science, 7(1), 2011.Google ScholarGoogle Scholar
  53. T. Chen, M. Diciolla, M. Z. Kwiatkowska, and A. Mereacre. Verification of linear duration properties over continuous-time Markov chains. ACM Trans. Comput. Log., 14(4):33, 2013. Google ScholarGoogle ScholarDigital LibraryDigital Library
  54. T. Chen, Y. Feng, D. S. Rosenblum, and G. Su. Perturbation analysis in verification of discrete-time Markov chains. In CONCUR, volume 8704 of LNCS, pages 218--233. Springer, 2014.Google ScholarGoogle Scholar
  55. L. Cheung, N. A. Lynch, R. Segala, and F. W. Vaandrager. Switched PIOA: parallel composition via distributed scheduling. Theor. Comput. Sci., 365(1-2):83--108, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  56. F. Ciesinski and C. Baier. Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems. In QEST, pages 131--132. IEEE Computer Society, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  57. E. M. Clarke. The birth of model checking. In 25 Years of Model Checking, volume 5000 of LNCS, pages 1--26. Springer, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  58. F. Corzilius, G. Kremer, S. Junges, S. Schupp, and E. Ábrahám. SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving. In SAT, volume 9340 of LNCS, pages 360--368. Springer, 2015.Google ScholarGoogle Scholar
  59. C. Courcoubetis and M. Yannakakis. Verifying temporal properties of finite-state probabilistic programs. In FOCS, pages 338--345. IEEE Computer Society, 1988. Google ScholarGoogle ScholarDigital LibraryDigital Library
  60. C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. J. ACM, 42(4):857--907, 1995. Google ScholarGoogle ScholarDigital LibraryDigital Library
  61. F. Dannenberg, M. Z. Kwiatkowska, C. Thachuk, and A. J. Turberfield. DNA walker circuits: computational potential, design, and verification. Natural Computing, 14(2):195--211, 2015. Google ScholarGoogle ScholarDigital LibraryDigital Library
  62. P. R. D'Argenio and J.-P. Katoen. A theory of stochastic systems part I: stochastic automata. Inf. Comput., 203(1):1--38, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  63. A. David, K. G. Larsen, A. Legay, M. Mikucionis, and D. B. Poulsen. Uppaal SMC tutorial. STTT, 17(4):397--415, 2015. Google ScholarGoogle ScholarDigital LibraryDigital Library
  64. C. Daws. Symbolic and parametric model checking of discrete-time Markov chains. In ICTAC, volume 3407 of LNCS, pages 280--294. Springer, 2004. Google ScholarGoogle ScholarDigital LibraryDigital Library
  65. L. de Alfaro. How to specify and verify the long-run average behavior of probabilistic systems. In LICS, pages 454--465. IEEE Computer Society, 1998. Google ScholarGoogle ScholarDigital LibraryDigital Library
  66. L. M. de Moura and N. Bjørner. Z3: an efficient SMT solver. In TACAS, volume 4963 of LNCS, pages 337--340. Springer, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  67. C. Dehnert, D. Gebler, M. Volpato, and D. N. Jansen. On abstraction of probabilistic systems. In ROCKS, volume 8453 of LNCS, pages 87--116, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  68. C. Dehnert, S. Junges, N. Jansen, F. Corzilius, M. Volk, H. Bruintjes, J.-P. Katoen, and E. Ábrahám. PROPhESY: A PRObabilistic ParamEter SYnthesis tool. In CAV (1), volume 9206 of LNCS, pages 214--231. Springer, 2015.Google ScholarGoogle Scholar
  69. B. Delahaye, J.-P. Katoen, K. G. Larsen, A. Legay, M. L. Pedersen, F. Sher, and A. Wasowski. Abstract probabilistic automata. Inf. Comput., 232:66--116, 2013. Google ScholarGoogle ScholarDigital LibraryDigital Library
  70. Y. Deng and M. Hennessy. On the semantics of Markov automata. Inf. Comput., 222:139--168, 2013. Google ScholarGoogle ScholarDigital LibraryDigital Library
  71. S. Donatelli, S. Haddad, and J. Sproston. Model checking timed and stochastic properties with CSL^{TA}. IEEE Trans. Software Eng., 35 (2):224--240, 2009. Google ScholarGoogle ScholarDigital LibraryDigital Library
  72. W. Douglas Obal II and W. H. Sanders. State-space support for path-based reward variables. Perform. Eval., 35(3-4):233--251, 1999. Google ScholarGoogle ScholarDigital LibraryDigital Library
  73. L. Doyen, T. A. Henzinger, and J.-F. Raskin. Equivalence of labeled Markov chains. Int. J. Found. Comput. Sci., 19(3):549--563, 2008.Google ScholarGoogle ScholarCross RefCross Ref
  74. C. Dubslaff, C. Baier, and M. Berg. Model checking probabilistic systems against pushdown specifications. Inf. Process. Lett., 112(8-9):320--328, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  75. J. B. Dugan, S. J. Bavuso, and M. A. Boyd. Dynamic fault-tree models for fault-tolerant computer systems. IEEE Trans. on Reliability, 41(3):363--377, 1992.Google ScholarGoogle ScholarCross RefCross Ref
  76. C. Eisentraut, H. Hermanns, and L. Zhang. On probabilistic automata in continuous time. In LICS, pages 342--351. IEEE CS, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  77. C. Eisentraut, H. Hermanns, J.-P. Katoen, and L. Zhang. A semantics for every GSPN. In Petri Nets, volume 7927 of LNCS, pages 90--109. Springer, 2013. Google ScholarGoogle ScholarDigital LibraryDigital Library
  78. M.-A. Esteve, J.-P. Katoen, V. Y. Nguyen, B. Postma, and Y. Yushtein. Formal correctness, safety, dependability, and performance analysis of a satellite. In ICSE, pages 1022--1031. IEEE, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  79. K. Etessami. Analysis of probabilistic processes and automata theory. In Automata: from Mathematics to Applications. 2016 (to appear).Google ScholarGoogle Scholar
  80. K. Etessami and M. Yannakakis. Recursive Markov decision processes and recursive stochastic games. J. ACM, 62(2):11, 2015. Google ScholarGoogle ScholarDigital LibraryDigital Library
  81. K. Etessami, M. Z. Kwiatkowska, M. Y. Vardi, and M. Yannakakis. Multi-objective model checking of Markov decision processes. Logical Methods in Computer Science, 4(4), 2008.Google ScholarGoogle Scholar
  82. J. Fearnley, M. N. Rabe, S. Schewe, and L. Zhang. Efficient approximation of optimal control for continuous-time Markov games. Inf. Comput., 247:106--129, 2016. Google ScholarGoogle ScholarDigital LibraryDigital Library
  83. P. H. Feiler and D. P. Gluch. Model-Based Engineering with AADL - An Introduction to the SAE Architecture Analysis and Design Language. SEI series in software engineering. Addison-Wesley, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  84. J. Filar and K. Vrieze. Competitive Markov Decision Processes. Springer-Verlag, 1996. Google ScholarGoogle ScholarDigital LibraryDigital Library
  85. V. Forejt, M. Z. Kwiatkowska, G. Norman, and D. Parker. Automated verification techniques for probabilistic systems. In SFM, volume 6659 of LNCS, pages 53--113. Springer, 2011.Google ScholarGoogle Scholar
  86. H. Fu. Maximal cost-bounded reachability probability on continuous-time Markov decision processes. In FoSSaCS, volume 8412 of LNCS, pages 73--87. Springer, 2014.Google ScholarGoogle Scholar
  87. D. Gross and D. R. Miller. The randomization technique as a modeling tool and solution procedure for transient Markov chains. Operations Research, 32(2):343--361, 1984. Google ScholarGoogle ScholarDigital LibraryDigital Library
  88. D. Guck, H. Hatefi, H. Hermanns, J.-P. Katoen, and M. Timmer. Analysis of timed and long-run objectives for Markov automata. Logical Methods in Computer Science, 10(3), 2014.Google ScholarGoogle Scholar
  89. D. Guck, J.-P. Katoen, M. I. A. Stoelinga, T. Luiten, and J. Romijn. Smart railroad maintenance engineering with stochastic model checking. In Railways, volume 104, pages 299--314. Civil-Comp Press, 2014.Google ScholarGoogle Scholar
  90. X. Guo and O. Hernandez-Lerma. Continuous-Time Markov Decision Processes: Theory and Applications, volume 62 of Stochastic Modelling and Applied Probability. Springer-Verlag, 2009.Google ScholarGoogle Scholar
  91. E. M. Hahn, H. Hermanns, and L. Zhang. Probabilistic reachability for parametric Markov models. STTT, 13(1):3--19, 2011.Google ScholarGoogle ScholarCross RefCross Ref
  92. E. M. Hahn, Y. Li, S. Schewe, A. Turrini, and L. Zhang. iscasMc: A web-based probabilistic model checker. In FM, volume 8442 of LNCS, pages 312--317. Springer, 2014. Google ScholarGoogle ScholarDigital LibraryDigital Library
  93. T. Han, J.-P. Katoen, and A. Mereacre. Approximate parameter synthesis for probabilistic time-bounded reachability. In RTSS, pages 173--182. IEEE Computer Society, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  94. H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Asp. of Comput., 6(5):512--535, 1994.Google ScholarGoogle ScholarCross RefCross Ref
  95. S. Hart, M. Sharir, and A. Pnueli. Termination of probabilistic concurrent program. ACM Trans. Program. Lang. Syst., 5(3):356--380, 1983. Google ScholarGoogle ScholarDigital LibraryDigital Library
  96. A. Hartmanns and H. Hermanns. In the quantitative automata zoo. Sci. Comput. Program., 112:3--23, 2015. Google ScholarGoogle ScholarDigital LibraryDigital Library
  97. M. Heiner, D. R. Gilbert, and R. Donaldson. Petri nets for systems and synthetic biology. In SFM, volume 5016 of LNCS, pages 215--264. Springer, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  98. H. Hermanns. Interactive Markov Chains: The Quest for Quantified Quality, volume 2428 of LNCS. Springer, 2002. Google ScholarGoogle ScholarDigital LibraryDigital Library
  99. H. Hermanns and J.-P. Katoen. Automated compositional Markov chain generation for a plain-old telephone system. Sci. Comput. Program., 36(1):97--127, 2000. Google ScholarGoogle ScholarDigital LibraryDigital Library
  100. J. Hillston. Process algebras for quantitative analysis. In LICS, pages 239--248. IEEE Computer Society, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  101. R. A. Howard. Dynamic Probabilistic Systems, volume 2: Semi-Markov and Decision Processes. John Wiley & Sons, 1972.Google ScholarGoogle Scholar
  102. N. Jansen, F. Corzilius, M. Volk, R. Wimmer, E. Ábrahám, J.-P. Katoen, and B. Becker. Accelerating parametric probabilistic verification. In QEST, volume 8657 of LNCS, pages 404--420. Springer, 2014.Google ScholarGoogle Scholar
  103. D. Jovanovic and L. M. de Moura. Solving non-linear arithmetic. In IJCAR, volume 7364 of LNCS, pages 339--354. Springer, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  104. J.-P. Katoen. Model checking meets probability: A gentle introduction. In Engineering Dependable Software Systems, volume 34 of NATO Science for Peace and Security Series, D: Information and Communication Security, pages 177--205. IOS Press, 2013.Google ScholarGoogle Scholar
  105. J.-P. Katoen and H. Wu. Probabilistic model checking for uncertain scenario-aware data flow. ACM Trans. Embedded Comp. Sys., pages 1--26, 2016 (to appear). Google ScholarGoogle ScholarDigital LibraryDigital Library
  106. J.-P. Katoen, M. Z. Kwiatkowska, G. Norman, and D. Parker. Faster and symbolic CTMC model checking. In PAPM-PROBMIV, volume 2165 of LNCS, pages 23--38. Springer, 2001. Google ScholarGoogle ScholarDigital LibraryDigital Library
  107. J.-P. Katoen, T. Kemna, I. S. Zapreev, and D. N. Jansen. Bisimulation minimisation mostly speeds up probabilistic model checking. In TACAS, volume 4424 of LNCS, pages 87--101. Springer, 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  108. J.-P. Katoen, D. Klink, and M. R. Neuhäußer. Compositional abstraction for stochastic systems. In FORMATS, volume 5813 of LNCS, pages 195--211. Springer, 2009. Google ScholarGoogle ScholarDigital LibraryDigital Library
  109. J.-P. Katoen, I. S. Zapreev, E. M. Hahn, H. Hermanns, and D. N. Jansen. The ins and outs of the probabilistic model checker MRMC. Perform. Eval., 68(2):90--104, 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  110. J.-P. Katoen, D. Klink, M. Leucker, and V. Wolf. Three-valued abstraction for probabilistic systems. J. Log. Algebr. Program., 81 (4):356--389, 2012.Google ScholarGoogle ScholarCross RefCross Ref
  111. J.-P. Katoen, L. Song, and L. Zhang. Probably safe or live. In CSL-LICS, pages 55:1--55:10. ACM, 2014. Google ScholarGoogle ScholarDigital LibraryDigital Library
  112. M. Kattenbelt, M. Z. Kwiatkowska, G. Norman, and D. Parker. A game-based abstraction-refinement framework for Markov decision processes. Formal Methods in System Design, 36(3):246--280, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  113. J. Kemeny and J. Snell. Finite Markov Chains. D. Van Nostrand, 1960.Google ScholarGoogle Scholar
  114. J. Kemeny and J. Snell. Denumerable Markov Chains. D. Van Nostrand, 1976.Google ScholarGoogle ScholarCross RefCross Ref
  115. S. Kiefer, A. S. Murawski, J. Ouaknine, B. Wachter, and J. Worrell. APEX: an analyzer for open probabilistic programs. In CAV, volume 7358 of LNCS, pages 693--698. Springer, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  116. D. Klink, A. Remke, B. R. Haverkort, and J.-P. Katoen. Time-bounded reachability in tree-structured QBDs by abstraction. Perform. Eval., 68(2):105--125, 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  117. G. Klutke, P. C. Kiessler, and M. A. Wortman. A critical look at the bathtub curve. IEEE Trans. Reliability, 52(1):125--129, 2003.Google ScholarGoogle ScholarCross RefCross Ref
  118. D. Knuth and A. Yao. Algorithms and Complexity: New Directions and Recent Results, chapter The complexity of nonuniform random number generation. Academic Press, 1976.Google ScholarGoogle ScholarDigital LibraryDigital Library
  119. A. Komuravelli, C. S. Pasareanu, and E. M. Clarke. Assume-guarantee abstraction refinement for probabilistic systems. In CAV, volume 7358 of LNCS, pages 310--326. Springer, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  120. D. Kozen. Semantics of probabilistic programs. J. Comput. Syst. Sci., 22(3):328--350, 1981.Google ScholarGoogle ScholarCross RefCross Ref
  121. D. Kozen. A probabilistic PDL. In STOC, pages 291--297. ACM, 1983. Google ScholarGoogle ScholarDigital LibraryDigital Library
  122. D. Krähmann, J. Schubert, C. Baier, and C. Dubslaff. Ratio and weight quantiles. In MFCS (1), volume 9234 of LNCS, pages 344--356. Springer, 2015.Google ScholarGoogle Scholar
  123. A. Kucera and O. Strazovský. On the controller synthesis for finite-state Markov decision processes. Fundam. Inform., 82(1-2):141--153, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  124. M. Kudlek. Probability in Petri nets. Fundam. Inform., 67(1-3):121--130, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  125. M. Kwiatkowska, D. Parker, and C. Wiltsche. PRISM-Games 2.0: A tool for multi-objective strategy synthesis for stochastic games. In TACAS, volume 9636 of LNCS, pages 560--566. Springer, 2016. Google ScholarGoogle ScholarDigital LibraryDigital Library
  126. M. Z. Kwiatkowska and C. Thachuk. Probabilistic model checking for biology. In Software Systems Safety, volume 36 of NATO Science for Peace and Security Series, D: Information and Communication Security, pages 165--189. IOS Press, 2014.Google ScholarGoogle Scholar
  127. M. Z. Kwiatkowska, G. Norman, and D. Parker. Symmetry reduction for probabilistic model checking. In CAV, volume 4144 of LNCS, pages 234--248. Springer, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  128. M. Z. Kwiatkowska, G. Norman, and D. Parker. Stochastic model checking. In SFM, volume 4486 of LNCS, pages 220--270. Springer, 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  129. M. Z. Kwiatkowska, G. Norman, and D. Parker. PRISM 4.0: Verification of probabilistic real-time systems. In CAV, volume 6806 of LNCS, pages 585--591. Springer, 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  130. M. Z. Kwiatkowska, G. Norman, D. Parker, and H. Qu. Compositional probabilistic verification through multi-objective model checking. Inf. Comput., 232:38--65, 2013. Google ScholarGoogle ScholarDigital LibraryDigital Library
  131. M. R. Lakin, D. Parker, L. Cardelli, M. Kwiatkowska, and A. Phillips. Design and analysis of dna strand displacement devices using probabilistic model checking. J R Soc Interface, 9:1470--1485, 2012.Google ScholarGoogle ScholarCross RefCross Ref
  132. R. Lanotte, A. Maggiolo-Schettini, and A. Troina. Parametric probabilistic transition systems for system design and analysis. Formal Asp. Comput., 19(1):93--109, 2007. Google ScholarGoogle ScholarCross RefCross Ref
  133. K. G. Larsen and A. Skou. Bisimulation through probabilistic testing. Inf. and Comp., 94(1):1--28, 1991. Google ScholarGoogle ScholarDigital LibraryDigital Library
  134. A. Legay, B. Delahaye, and S. Bensalem. Statistical model checking: An overview. In RV, volume 6418 of LNCS, pages 122--135. Springer, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  135. J. Lisman and M. van Zuylen. Note on the generation of most probable frequency distributions. Statistica Neerlandica, 26(1):19--23, 1972.Google ScholarGoogle ScholarCross RefCross Ref
  136. F. Long and M. Rinard. Automatic patch generation by learning correct code. In POPL, pages 298--312. ACM, 2016. Google ScholarGoogle ScholarDigital LibraryDigital Library
  137. C. Madsen, Z. Zhang, N. Roehner, C. Winstead, and C. J. Myers. Stochastic model checking of genetic circuits. JETC, 11(3):23:1--23:21, 2014. Google ScholarGoogle ScholarDigital LibraryDigital Library
  138. M. A. Marsan, G. Conte, and G. Balbo. A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems. ACM Trans. Comput. Syst., 2(2):93--122, 1984. Google ScholarGoogle ScholarDigital LibraryDigital Library
  139. L. Mikeev, M. R. Neuhäußer, D. Spieler, and V. Wolf. On-the-fly verification and optimization of DTA-properties for large Markov chains. Formal Methods in System Design, 43(2):313--337, 2013. Google ScholarGoogle ScholarDigital LibraryDigital Library
  140. B. L. Miller. Finite state continuous time Markov decision processes with a finite planning horizon. SIAM J. on Control, 6:266--280, 1968.Google ScholarGoogle ScholarCross RefCross Ref
  141. C. Moler and C. F. Van Loan. Nineteen dubious ways to compute the exponential of a matrix, twenty-five years later. SIAM Review, 45(1): 3--49, 2003.Google ScholarGoogle ScholarDigital LibraryDigital Library
  142. C. B. Moler and C. F. Van Loan. Nineteen dubious ways to compute the exponential of a matrix. SIAM Review, 20:801--836, 1978.Google ScholarGoogle ScholarDigital LibraryDigital Library
  143. S. Nain, Y. Lustig, and M. Y. Vardi. Synthesis from probabilistic components. Logical Methods in Computer Science, 10(2), 2014.Google ScholarGoogle Scholar
  144. N. Napp and E. Klavins. A compositional framework for programming stochastically interacting robots. I. J. Robotic Res., 30(6):713--729, 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  145. M. R. Neuhäußer, M. Stoelinga, and J.-P. Katoen. Delayed nondeterminism in continuous-time Markov decision processes. In FOSSACS, volume 5504 of LNCS, pages 364--379. Springer, 2009.Google ScholarGoogle Scholar
  146. M. F. Neuts. Matrix-geometric solutions in stochastic models - an algorithmic approach. Dover Publications, 1994.Google ScholarGoogle Scholar
  147. A. V. Nori, S. Ozair, S. K. Rajamani, and D. Vijaykeerthy. Efficient synthesis of probabilistic programs. In PLDI, pages 208--217. ACM, 2015. Google ScholarGoogle ScholarDigital LibraryDigital Library
  148. G. Norman. Analysing randomized distributed algorithms. In Validation of Stochastic Systems, volume 2925 of LNCS, pages 384--418. Springer, 2004.Google ScholarGoogle ScholarCross RefCross Ref
  149. G. Norman and V. Shmatikov. Analysis of probabilistic contract signing. In FASec, volume 2629 of LNCS, pages 81--96. Springer, 2002.Google ScholarGoogle Scholar
  150. G. Norman, D. Parker, M. Z. Kwiatkowska, S. K. Shukla, and R. Gupta. Using probabilistic model checking for dynamic power management. Formal Asp. Comput., 17(2):160--176, 2005. Google ScholarGoogle ScholarCross RefCross Ref
  151. G. Norman, D. Parker, and J. Sproston. Model checking for probabilistic timed automata. Formal Methods in System Design, 43(2): 164--190, 2013. Google ScholarGoogle ScholarDigital LibraryDigital Library
  152. J. R. Norris. Markov chains. Cambridge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, 1998.Google ScholarGoogle Scholar
  153. P. Panangaden. Labelled Markov Processes. Imperial College Press, 2009. Google ScholarGoogle ScholarDigital LibraryDigital Library
  154. S. Pathak, L. Pulina, and A. Tacchella. Evaluating probabilistic model checking tools for verification of robot control policies. AI Commun., 29(2):287--299, 2016.Google ScholarGoogle ScholarCross RefCross Ref
  155. A. Paz. Introduction to Probabilistic Automata. Academic Press, 1971. Google ScholarGoogle ScholarDigital LibraryDigital Library
  156. A. Pnueli and L. D. Zuck. Probabilistic verification by tableaux. In LICS, pages 322--331. IEEE Computer Society, 1986.Google ScholarGoogle Scholar
  157. M. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, 1994. Google ScholarGoogle ScholarDigital LibraryDigital Library
  158. T. Quatmann, C. Dehnert, N. Jansen, S. Junges, and J.-P. Katoen. Parameter synthesis for Markov models: Faster than ever. CoRR, abs/1602.05113, 2016.Google ScholarGoogle Scholar
  159. M. O. Rabin. Probabilistic automata. Inf. and Control, 6(3):230--245, 1963.Google ScholarGoogle ScholarCross RefCross Ref
  160. M. Randour, J.-F. Raskin, and O. Sankur. Percentile queries in multidimensional Markov decision processes. In CAV (1), volume 9206 of LNCS, pages 123--139. Springer, 2015.Google ScholarGoogle Scholar
  161. E. Ruijters and M. Stoelinga. Fault tree analysis: A survey of the state-of-the-art in modeling, analysis and tools. Computer Science Review, 15:29--62, 2015. Google ScholarGoogle ScholarDigital LibraryDigital Library
  162. P. Schnoebelen. The verification of probabilistic lossy channel systems. In Validation of Stochastic Systems, volume 2925 of LNCS, pages 445--466. Springer, 2004.Google ScholarGoogle ScholarCross RefCross Ref
  163. R. Segala and N. A. Lynch. Probabilistic simulations for probabilistic processes. Nord. J. Comput., 2(2):250--273, 1995. Google ScholarGoogle ScholarDigital LibraryDigital Library
  164. S. Song, J. Sun, Y. Liu, and J. S. Dong. A model checker for hierarchical probabilistic real-time systems. In CAV, volume 7358 of LNCS, pages 705--711. Springer, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  165. M. Stamatelatos, W. Vesely, J. B. Dugan, J. Fragola, J. Minarick, and J. Railsback. Fault Tree Handbook with Aerospace Applications. NASA Headquarters, 2002.Google ScholarGoogle Scholar
  166. E. W. Stark and S. A. Smolka. Compositional analysis of expected delays in networks of probabilistic I/O automata. In LICS, pages 466--477. IEEE Computer Society, 1998. Google ScholarGoogle ScholarDigital LibraryDigital Library
  167. G. Su, D. S. Rosenblum, and G. Tamburrelli. Reliability of run-time quality-of-service evaluation using parametric model checking. In ICSE. ACM, 2016 (to appear). Google ScholarGoogle ScholarDigital LibraryDigital Library
  168. M. Timmer, J.-P. K. J. van de Pol, and M. Stoelinga. Confluence reduction for Markov automata. Theor. Comput. Sci., 2016 (to appear).Google ScholarGoogle Scholar
  169. A. Valmari and G. Franceschinis. Simple O(m logn) time Markov chain lumping. In TACAS, volume 6015 of LNCS, pages 38--52. Springer, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  170. F. van Breugel and J. Worrell. A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci., 331(1):115--142, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  171. M. Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In FOCS, pages 327--338. IEEE, 1985. Google ScholarGoogle ScholarDigital LibraryDigital Library
  172. W. E. Vessely, F. F. Goldberg, N. H. Roberts, and D. F. Haasl. Fault Tree Handbook. Office of Nuclear Regulatory Research, U.S. Nuclear Regulatory Commission, 1981.Google ScholarGoogle Scholar
  173. M. Volk, S. Junges, and J.-P. Katoen. Advancing dynamic fault tree analysis. In SafeComp, LNCS. Springer, 2016 (to appear).Google ScholarGoogle Scholar
  174. B. Wachter and L. Zhang. Best probabilistic transformers. In VMCAI, volume 5944 of LNCS, pages 362--379. Springer, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  175. S.-H. Wu, S. A. Smolka, and E. W. Stark. Composition and behaviors of probabilistic I/O automata. Theor. Comput. Sci., 176(1-2):1--38, 1997. Google ScholarGoogle ScholarDigital LibraryDigital Library
  176. H. L. S. Younes and R. G. Simmons. Statistical probabilistic model checking with a focus on time-bounded properties. Inf. Comput., 204 (9):1368--1409, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  177. L. Zhang, D. N. Jansen, F. Nielson, and H. Hermanns. Automata-based CSL model checking. Logical Methods in Computer Science, 8(2), 2011.Google ScholarGoogle Scholar

Index Terms

  1. The Probabilistic Model Checking Landscape

          Recommendations

          Comments

          Login options

          Check if you have access through your login credentials or your institution to get full access on this article.

          Sign in
          • Published in

            cover image ACM Conferences
            LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science
            July 2016
            901 pages
            ISBN:9781450343916
            DOI:10.1145/2933575

            Copyright © 2016 Owner/Author

            Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

            Publisher

            Association for Computing Machinery

            New York, NY, United States

            Publication History

            • Published: 5 July 2016

            Check for updates

            Qualifiers

            • tutorial
            • Research
            • Refereed limited

            Acceptance Rates

            Overall Acceptance Rate143of386submissions,37%

          PDF Format

          View or Download as a PDF file.

          PDF

          eReader

          View online with eReader.

          eReader