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.
- 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 ScholarCross Ref
- P. A. Abdulla, N. B. Henda, and R. Mayr. Decisive Markov chains. Logical Methods in Computer Science, 3(4), 2007.Google Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- S. Akshay, T. Antonopoulos, J. Ouaknine, and J. Worrell. Reachability problems for Markov chains. Inf. Process. Lett., 115(2):155--158, 2015. Google ScholarDigital Library
- R. Alur, T. A. Henzinger, and M. Vardi. Theory in practice for system design and verification. ACM SIGLOG News, 3, 2015. Google ScholarDigital Library
- 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 ScholarCross Ref
- 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 Scholar
- 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 Scholar
- 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 ScholarDigital Library
- C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008. Google ScholarDigital Library
- C. Baier and M. Z. Kwiatkowska. Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11(3): 125--155, 1998. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- 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 ScholarCross Ref
- 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 ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- C. Baier, M. Größer, and N. Bertrand. Probabilistic ω-automata. J. ACM, 59(1):1, 2012. Google ScholarDigital Library
- 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 ScholarCross Ref
- 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 ScholarDigital Library
- 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 Scholar
- C. Baier, L. de Alfaro, V. Forejt, and M. Kwiatkowska. Probabilistic model checking. In Handbook of Model Checking. Springer, 2016 (to appear).Google Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- M. D. Beaudry. Performance-related reliability measures for computing systems. IEEE Trans. on Computers, 27(6):540--547, 1978. Google ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarCross Ref
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarCross Ref
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
- P. Buchholz and I. Schulz. Numerical analysis of continuous time Markov decision processes over finite horizons. Computers & OR, 38(3):651--659, 2011. Google ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- 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 Scholar
- S. Chakraborty and J.-P. Katoen. Parametric LTL on Markov chains. In IFIP TCS, volume 8705 of LNCS, pages 207--221. Springer, 2014.Google Scholar
- K. Chatterjee and T. A. Henzinger. A survey of stochastic ω-regular games. J. Comput. Syst. Sci., 78(2):394--413, 2012. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- E. M. Clarke. The birth of model checking. In 25 Years of Model Checking, volume 5000 of LNCS, pages 1--26. Springer, 2008. Google ScholarDigital Library
- 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 Scholar
- C. Courcoubetis and M. Yannakakis. Verifying temporal properties of finite-state probabilistic programs. In FOCS, pages 338--345. IEEE Computer Society, 1988. Google ScholarDigital Library
- C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. J. ACM, 42(4):857--907, 1995. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- A. David, K. G. Larsen, A. Legay, M. Mikucionis, and D. B. Poulsen. Uppaal SMC tutorial. STTT, 17(4):397--415, 2015. Google ScholarDigital Library
- C. Daws. Symbolic and parametric model checking of discrete-time Markov chains. In ICTAC, volume 3407 of LNCS, pages 280--294. Springer, 2004. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- Y. Deng and M. Hennessy. On the semantics of Markov automata. Inf. Comput., 222:139--168, 2013. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarCross Ref
- C. Dubslaff, C. Baier, and M. Berg. Model checking probabilistic systems against pushdown specifications. Inf. Process. Lett., 112(8-9):320--328, 2012. Google ScholarDigital Library
- 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 ScholarCross Ref
- C. Eisentraut, H. Hermanns, and L. Zhang. On probabilistic automata in continuous time. In LICS, pages 342--351. IEEE CS, 2010. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- K. Etessami. Analysis of probabilistic processes and automata theory. In Automata: from Mathematics to Applications. 2016 (to appear).Google Scholar
- K. Etessami and M. Yannakakis. Recursive Markov decision processes and recursive stochastic games. J. ACM, 62(2):11, 2015. Google ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- J. Filar and K. Vrieze. Competitive Markov Decision Processes. Springer-Verlag, 1996. Google ScholarDigital Library
- 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 Scholar
- 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 Scholar
- 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 ScholarDigital Library
- 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 Scholar
- 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 Scholar
- 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 Scholar
- E. M. Hahn, H. Hermanns, and L. Zhang. Probabilistic reachability for parametric Markov models. STTT, 13(1):3--19, 2011.Google ScholarCross Ref
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Asp. of Comput., 6(5):512--535, 1994.Google ScholarCross Ref
- S. Hart, M. Sharir, and A. Pnueli. Termination of probabilistic concurrent program. ACM Trans. Program. Lang. Syst., 5(3):356--380, 1983. Google ScholarDigital Library
- A. Hartmanns and H. Hermanns. In the quantitative automata zoo. Sci. Comput. Program., 112:3--23, 2015. Google ScholarDigital Library
- 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 ScholarDigital Library
- H. Hermanns. Interactive Markov Chains: The Quest for Quantified Quality, volume 2428 of LNCS. Springer, 2002. Google ScholarDigital Library
- 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 ScholarDigital Library
- J. Hillston. Process algebras for quantitative analysis. In LICS, pages 239--248. IEEE Computer Society, 2005. Google ScholarDigital Library
- R. A. Howard. Dynamic Probabilistic Systems, volume 2: Semi-Markov and Decision Processes. John Wiley & Sons, 1972.Google Scholar
- 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 Scholar
- D. Jovanovic and L. M. de Moura. Solving non-linear arithmetic. In IJCAR, volume 7364 of LNCS, pages 339--354. Springer, 2012. Google ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarCross Ref
- J.-P. Katoen, L. Song, and L. Zhang. Probably safe or live. In CSL-LICS, pages 55:1--55:10. ACM, 2014. Google ScholarDigital Library
- 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 ScholarDigital Library
- J. Kemeny and J. Snell. Finite Markov Chains. D. Van Nostrand, 1960.Google Scholar
- J. Kemeny and J. Snell. Denumerable Markov Chains. D. Van Nostrand, 1976.Google ScholarCross Ref
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarCross Ref
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- D. Kozen. Semantics of probabilistic programs. J. Comput. Syst. Sci., 22(3):328--350, 1981.Google ScholarCross Ref
- D. Kozen. A probabilistic PDL. In STOC, pages 291--297. ACM, 1983. Google ScholarDigital Library
- 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 Scholar
- A. Kucera and O. Strazovský. On the controller synthesis for finite-state Markov decision processes. Fundam. Inform., 82(1-2):141--153, 2008. Google ScholarDigital Library
- M. Kudlek. Probability in Petri nets. Fundam. Inform., 67(1-3):121--130, 2005. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- M. Z. Kwiatkowska, G. Norman, and D. Parker. Stochastic model checking. In SFM, volume 4486 of LNCS, pages 220--270. Springer, 2007. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarCross Ref
- 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 ScholarCross Ref
- K. G. Larsen and A. Skou. Bisimulation through probabilistic testing. Inf. and Comp., 94(1):1--28, 1991. Google ScholarDigital Library
- A. Legay, B. Delahaye, and S. Bensalem. Statistical model checking: An overview. In RV, volume 6418 of LNCS, pages 122--135. Springer, 2010. Google ScholarDigital Library
- J. Lisman and M. van Zuylen. Note on the generation of most probable frequency distributions. Statistica Neerlandica, 26(1):19--23, 1972.Google ScholarCross Ref
- F. Long and M. Rinard. Automatic patch generation by learning correct code. In POPL, pages 298--312. ACM, 2016. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- B. L. Miller. Finite state continuous time Markov decision processes with a finite planning horizon. SIAM J. on Control, 6:266--280, 1968.Google ScholarCross Ref
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- S. Nain, Y. Lustig, and M. Y. Vardi. Synthesis from probabilistic components. Logical Methods in Computer Science, 10(2), 2014.Google Scholar
- N. Napp and E. Klavins. A compositional framework for programming stochastically interacting robots. I. J. Robotic Res., 30(6):713--729, 2011. Google ScholarDigital Library
- 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 Scholar
- M. F. Neuts. Matrix-geometric solutions in stochastic models - an algorithmic approach. Dover Publications, 1994.Google Scholar
- A. V. Nori, S. Ozair, S. K. Rajamani, and D. Vijaykeerthy. Efficient synthesis of probabilistic programs. In PLDI, pages 208--217. ACM, 2015. Google ScholarDigital Library
- G. Norman. Analysing randomized distributed algorithms. In Validation of Stochastic Systems, volume 2925 of LNCS, pages 384--418. Springer, 2004.Google ScholarCross Ref
- G. Norman and V. Shmatikov. Analysis of probabilistic contract signing. In FASec, volume 2629 of LNCS, pages 81--96. Springer, 2002.Google Scholar
- 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 ScholarCross Ref
- G. Norman, D. Parker, and J. Sproston. Model checking for probabilistic timed automata. Formal Methods in System Design, 43(2): 164--190, 2013. Google ScholarDigital Library
- J. R. Norris. Markov chains. Cambridge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, 1998.Google Scholar
- P. Panangaden. Labelled Markov Processes. Imperial College Press, 2009. Google ScholarDigital Library
- 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 ScholarCross Ref
- A. Paz. Introduction to Probabilistic Automata. Academic Press, 1971. Google ScholarDigital Library
- A. Pnueli and L. D. Zuck. Probabilistic verification by tableaux. In LICS, pages 322--331. IEEE Computer Society, 1986.Google Scholar
- M. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, 1994. Google ScholarDigital Library
- 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 Scholar
- M. O. Rabin. Probabilistic automata. Inf. and Control, 6(3):230--245, 1963.Google ScholarCross Ref
- 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 Scholar
- 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 ScholarDigital Library
- P. Schnoebelen. The verification of probabilistic lossy channel systems. In Validation of Stochastic Systems, volume 2925 of LNCS, pages 445--466. Springer, 2004.Google ScholarCross Ref
- R. Segala and N. A. Lynch. Probabilistic simulations for probabilistic processes. Nord. J. Comput., 2(2):250--273, 1995. Google ScholarDigital Library
- 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 ScholarDigital Library
- M. Stamatelatos, W. Vesely, J. B. Dugan, J. Fragola, J. Minarick, and J. Railsback. Fault Tree Handbook with Aerospace Applications. NASA Headquarters, 2002.Google Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- M. Timmer, J.-P. K. J. van de Pol, and M. Stoelinga. Confluence reduction for Markov automata. Theor. Comput. Sci., 2016 (to appear).Google Scholar
- 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 ScholarDigital Library
- F. van Breugel and J. Worrell. A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci., 331(1):115--142, 2005. Google ScholarDigital Library
- M. Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In FOCS, pages 327--338. IEEE, 1985. Google ScholarDigital Library
- 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 Scholar
- M. Volk, S. Junges, and J.-P. Katoen. Advancing dynamic fault tree analysis. In SafeComp, LNCS. Springer, 2016 (to appear).Google Scholar
- B. Wachter and L. Zhang. Best probabilistic transformers. In VMCAI, volume 5944 of LNCS, pages 362--379. Springer, 2010. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- L. Zhang, D. N. Jansen, F. Nielson, and H. Hermanns. Automata-based CSL model checking. Logical Methods in Computer Science, 8(2), 2011.Google Scholar
Index Terms
The Probabilistic Model Checking Landscape
Recommendations
Model checking epistemic-probabilistic logic using probabilistic interpreted systems
Model checking is a formal technique widely used to verify security and communication protocols in epistemic multi-agent systems against given properties. Qualitative properties such as safety and liveliness have been widely analyzed in the literature. ...
Abstraction for model checking multi-agent systems
Model checking multi-agent systems (MAS) always suffers from the state explosion problem. In this paper we focus on an abstraction technique which is one of the major methods for overcoming this problem. For a multi-agent system, we present a novel ...
A counterexample-guided abstraction-refinement framework for markov decision processes
The main challenge in using abstractions effectively is to construct a suitable abstraction for the system being verified. One approach that tries to address this problem is that of counterexample guided abstraction refinement (CEGAR), wherein one ...
Comments