Abstract
Probabilistic model checking is a powerful technique for formally verifying quantitative properties of systems that exhibit stochastic behaviour. Such systems are found in many application domains: for example, probabilistic behaviour may arise due to the presence of failures in unreliable hardware, message loss in wireless communication channels, or the use of randomisation in distributed protocols. This chapter starts with an introduction to the technique of probabilistic model checking. We then survey some recent advances in the area, including controller synthesis, compositional verification, probabilistic real-time systems and parametric model checking. We illustrate the application of the various techniques with a combination of toy examples and descriptions of larger case studies. The chapter concludes with a discussion of some of the key challenges in the field.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The bounded until operator \(\psi _1{\ {\mathtt U}^{\leqslant k}\ }\psi _2\) is not usually included in the syntax of LTL, but it can be derived from other operators so its inclusion is not problematic.
- 2.
Strictly speaking, the definition of reward operators differs in [28].
- 3.
In fact, state and action-labelled variants of temporal logics are equally expressive [90].
References
E. Ábrahám, B. Becker, C. Dehnert, N. Jansen, J.-P. Katoen, R. Wimmer, Counterexample generation for discrete-time Markov models: an introductory survey, in Formal Methods for the Design of Computer, Communication, and Software Systems (SFM’14), ed. By M. Bernardo, F. Damiani, R. Haehnle, E. Johnsen, I. Schaefer. LNCS, vol. 8483 (Springer, 2014), pp. 65–121
R. Alur, C. Courcoubetis, D. Dill, Model-checking for probabilistic real-time systems, in Proceedings of the 19th International Colloq Automata, Languages and Programming (ICALP’91). LNCS, vol. 510, (Springer, 1991), pp. 115–136
R. Alur, C. Courcoubetis, D. Dill, Model checking in dense real time. Inf. Comput. 104(1), 2–34 (1993)
R. Alur, T. Dang, F. Ivancic, Predicate abstraction for reachability analysis of hybrid systems. ACM Trans. Embed. Comput. Syst. 5(1), 152–199 (2006)
R. Alur, D. Dill, A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994)
R. Alur, T. Henzinger, O. Kupferman, Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)
R. Alur, T. Henzinger, S. Rajamani, Symbolic exploration of transition hierarchies, in Proceedings of the 4th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98). LNCS, vol. 1384, (Springer, 1998), pp. 330–344
R. Alur, S. La Torre, G. Pappas, Optimal paths in weighted timed automata. Theor. Comput. Sci. 318(3), 297–322 (2004)
R. Alur, A. Trivedi, Relating average and discounted costs for quantitative analysis of timed systems, in Proceedings of the 11th International Conference Embedded Software (EMSOFT’11) (ACM, 2011), pp. 165–174
E. André, T. Chatain, E. Encrenaz, L. Fribourg, An inverse method for parametric timed automata. Int. J. Found. Comput. Sci. 20(5), 819–836 (2009)
E. André, L. Fribourg, J. Sproston, An extension of the inverse method to probabilistic timed automata. Form. Methods Syst. Des. 42(2), 119–145 (2013)
C. Baier, E. Clarke, V. Hartonas-Garmhausen, M. Kwiatkowska, M. Ryan, Symbolic model checking for probabilistic processes, in Proceedings of the 24th International Colloquium Automata, Languages and Programming (ICALP’97), ed. By P. Degano, R. Gorrieri, A. Marchetti-Spaccamela. LNCS, vol. 1256 (Springer, 1997), pp. 430–440
C. Baier, M. Größer, M. Leucker, B. Bollig, F. Ciesinski, Controller synthesis for probabilistic systems, in Proceedings of the 3rd IFIP International Conference Theoretical Computer Science (TCS’06), ed. By J.-J. Lévy, E. Mayr, J. Mitchell (Kluwer, 2004), pp. 493–5062
C. Baier, B. Haverkort, H. Hermanns, J.-P. Katoen, Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524–541 (2003)
C. Baier, J.-P. Katoen, Principles of Model Checking (MIT Press, Cambridge, 2008)
E. Bartocci, R. Grosu, P. Katsaros, C. Ramakrishnan, S. Smolka, Model repair for probabilistic systems, in Proceedings of the 17th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS’11), ed. By P. Abdulla, K. Leino. LNCS, vol. 6605 (Springer, 2011), pp. 326–340
D. Beauquier, Probabilistic timed automata. Theor. Comput. Sci. 292(1), 65–84 (2003)
G. Behrmann, A. Cougnard, A. David, E. Fleury, K. Larsen, D. Lime, UPPAAL-Tiga: time for playing games!, in Proceedings of the 19th International Conference Computer Aided Verification (CAV’07). LNCS, vol. 4590 (Springer, 2007), pp. 121–125
G. Behrmann, A. Fehnker, T. Hune, K. Larsen, P. Pettersson, J. Romijn, Efficient guiding towards cost-optimality in UPPAAL, in Proceedings of the 7th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01), ed. By T. Margaria, W. Yi. LNCS, vol. 2031 (Springer, 2001), pp. 174–188
R. Bellman, Dynamic Programming (Princeton University Press, New Jersey, 1957)
P. Billingsley, Probability and Measure (Wiley, New Jersey, 1995)
P. Bouyer, U. Fahrenberg, K. Larsen, N. Markey, Quantitative analysis of real-time systems using priced timed automata. Commu. ACM 54(9), 78–87 (2011)
T. Brázdil, V. Brožek, V. Forejt, A. Kučera, Stochastic games with branching-time winning objectives, in Proceedings of the 21th IEEE Symposium Logic in Computer Science (LICS’06) (IEEE Computer Society, 2006), pp. 349–358
L. Brim, M. Češka, D.V.S. Dražan, Exploring parameter space of stochastic biochemical systems using quantitative model checking, in Proceedings of the 25th International Conference Computer Aided Verification (CAV’13). LNCS, vol. 8044 (Springer, 2013), pp. 107–123
P. Buchholz, E.M. Hahn, H. Hermanns, L. Zhang, Model checking algorithms for CTMDPs, in Proceedings of the 23rd International Conference Computer Aided Verification (CAV’11), ed. By G. Gopalakrishnan, S. Qadeer. LNCS, vol. 6806 (Springer, 2011), pp. 225–242
M. Češka, F. Dannenberg, M. Kwiatkowska, N. Paoletti, Precise parameter synthesis for stochastic biochemical systems, in Proceedings of the 12th International Conference Computational Methods in Systems Biology (CMSB’14), ed. By P. Mendes, J. Dada, K. Smallbone. LNCS/LNBI, vol. 8859 (Springer, 2014), pp. 86–98
K. Chatterjee, M. Chmelík, R. Gupta, A. Kanodia, Qualitative analysis of POMDPs with temporal logic specifications for robotics applications, in Proceedings of the IEEE International Conference Robotics and Automation, (ICRA’15) (IEEE Computer Society, 2015), pp. 325–330
T. Chen, V. Forejt, M. Kwiatkowska, D. Parker, A. Simaitis, Automatic verification of competitive stochastic systems. Form. Methods Syst. Des. 43(1), 61–92 (2013)
S. Cheshire, B. Adoba, E. Gutterman, Dynamic configuration of IPv4 link local addresses. http://www.ietf.org/rfc/rfc3927.txtwww.ietf.org/rfc/rfc3927.txt
E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith, Counterexample-guided abstraction refinement, in Proceedings of the 12th International Conference Computer Aided Verification (CAV’00), ed. By A. Emerson, A. Sistla. LNCS, vol. 1855 (Springer, 2000), pp. 154–169
A. Condon, The complexity of stochastic games. Inf. Comput. 96(2), 203–224 (1992)
A. Condon, On algorithms for simple stochastic games, Advances in computational complexity theory. DIMACS Series in Discrete Mathematics and Theoretical Computer Science 13, 51–73 (1993)
M. Daniele, F. Giunchiglia, M. Vardi, Improved automata generation for linear temporal logic, in Proceedings of the 11th International Conference Computer Aided Verification (CAV’99), ed. By N. Halbwachs, D. Peled. LNCS, vol. 1633 (Springer, 1999), pp. 249–260
P. D’Argenio, B. Jeannet, H. Jensen, K. Larsen, in Reachability analysis of probabilistic systems by successive refinements, Proceedings of the 1st Joint International Workshop Process Algebra and Probabilistic Methods, Performance Modelling and Verification (PAPM/PROBMIV’01), ed. By L. de Alfaro, S. Gilmore. LNCS, vol. 2165 (Springer, 2001), pp. 39–56
C. Daws, Symbolic and parametric model checking of discrete-time Markov chains, in Proceedings of the 1st International Colloquium Theoretical Aspects of Computing (ICTAC’04), ed. By Z. Liu, K. Araki. LNCS, vol. 3407 (Springer, 2004), pp. 280–294
L. de Alfaro, Formal Verification of Probabilistic Systems. Ph.D. thesis, Stanford University, 1997
C. Dehnert, S. Junges, N. Jansen, F. Corzilius, M. Volk, H. Bruintjes, J.-P. Katoen, E. Ábrahám, PROPhESY: a PRObabilistic ParamEter SYnthesis tool, in Proceedings of the 27th International Conference Computer Aided Verification (CAV’15). LNCS, vol. 9206 (Springer, 2015), pp. 214–231
J. Desharnais, J. Assouramou, Analysis of non-linear probabilistic hybrid systems, in Proceedings of the 9th Workshop Quantitative Aspects of Programming Languages (QAPL’11). EPTCS, vol. 57 (2011), pp. 104–119
A. Donaldson, A. Miller, Symmetry reduction for probabilistic model checking using generic representatives, in Proceedings of the 4th International Symposium Automated Technology for Verification and Analysis (ATVA’06), ed. By S. Graf, W. Zhang. LNCS, vol. 4218 (Springer, 2006), pp. 9–23
S. Donatelli, S. Haddad, J. Sproston, Model checking timed and stochastic properties with CSL\({}^{\text{ta}}\). IEEE Trans. Softw. Eng. 35(2), 224–240 (2008)
C. Eisentraut, H. Hermanns, L. Zhang, On probabilistic automata in continuous time, in Proceedings of the 25th Annual IEEE Symposium Logic in Computer Science (LICS’10) (IEEE Computer Society, 2010), pp. 342–351
K. Etessami, M. Kwiatkowska, M. Vardi, M. Yannakakis, Multi-objective model checking of Markov decision processes. Logical Methods Comput. Sci. 4(4), 1–21 (2008)
A. Filieri, G. Tamburrelli, C. Ghezzi, Supporting self-adaptation via quantitative verification and sensitivity analysis at run time. IEEE Trans. Softw. Eng. 42(1), 75–99 (2016)
V. Forejt, M. Kwiatkowska, G. Norman, D. Parker, Automated verification techniques for probabilistic systems, in Formal Methods for Eternal Networked Software Systems (SFM’11), ed. By M. Bernardo, V. Issarny. LNCS, vol. 6659 (Springer, 2011), pp. 53–113
V. Forejt, M. Kwiatkowska, G. Norman, D. Parker, H. Qu, Quantitative multi-objective verification for probabilistic systems, in Proceedings of the 17th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS’11), ed. By P. Abdulla, K. Leino. LNCS, vol. 6605 (Springer, 2011), pp. 112–127
V. Forejt, M. Kwiatkowska, D. Parker, Pareto curves for probabilistic model checking, in Proceedings of the 10th International Symposium Automated Technology for Verification and Analysis (ATVA’12), ed. By S. Chakraborty, M. Mukund. LNCS, vol. 7561 (Springer, 2012), pp. 317–332
M. Fränzle, T. Teige, A. Eggers, Engineering constraint solvers for automatic analysis of probabilistic hybrid automata. J. Logic Algebr. Progr. 79(7), 436–466 (2010)
S. Graf, H. Saidi, Construction of abstract state graphs with PVS, in Proceedings of the 9th International Conference Computer Aided Verification (CAV’97), ed. By O. Grumberg. LNCS, vol. 1254 (Springer, 1997), pp. 72–83
D. Gross, D. Miller, The randomization technique as a modeling tool and solution procedure for transient Markov processes. Oper. Res. 32(2), 343–361 (1984)
M. Größer, C. Baier, Partial order reduction for Markov decision processes: a survey, in Proceedings of the 4th International Symposium Formal Methods for Component and Objects (FMCO’05), ed. By F. de Boer, M. Bonsangue, S. Graf, W.-P. de Roever. LNCS, vol. 4111 (Springer, 2006), pp. 408–427
E.M. Hahn, T. Han, L. Zhang, Synthesis for PCTL in parametric Markov decision processes, in Proceedings of the 3rd NASA Formal Methods Symposium (NFM’11). LNCS, vol. 6617 (Springer, 2011)
E.M. Hahn, H. Hermanns, B. Wachter, L. Zhang, PARAM: a model checker for parametric Markov models, in Proceedings of the 22nd International Conference Computer Aided Verification (CAV’10). LNCS, vol. 6174 (Springer, 2010), pp. 660–664
E.M. Hahn, H. Hermanns, B. Wachter, L. Zhang, PASS: abstraction refinement for infinite probabilistic models, in Proceedings of the 16th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS’10), ed. By J. Esparza, R. Majumdar. LNCS, vol. 6105 (Springer, 2010), pp. 353–357
E.M. Hahn, H. Hermanns, L. Zhang, Probabilistic reachability for parametric Markov models. Int. J. Softw. Tools Technol. Trans. (STTT) 13(1), 3–19 (2011)
E.M. Hahn, Y. Li, S. Schewe, A. Turrini, L. Zhang, iscasMc: a web-based probabilistic model checker, in Proceedings of the 19th International Symposium on Formal Methods (FM’14) (2014), pp. 312–317
E.M. Hahn, G. Norman, D. Parker, B. Wachter, L. Zhang, Game-based abstraction and controller synthesis for probabilistic hybrid systems, in Proceedings of the 8th International Conference Quantitative Evaluation of SysTems (QEST’11) (IEEE Computer Society Press, 2011), pp. 69–78
J. Han, P. Jonker, A system architecture solution for unreliable nanoelectronic devices. IEEE Trans. Nanotechnol. 1, 201–208 (2002)
T. Han, J.-P. Katoen, B. Damman, Counterexample generation in probabilistic model checking. IEEE Trans. Softw. Eng. 35(2), 241–257 (2009)
T. Han, J.-P. Katoen, A. Mereacre, Approximate parameter synthesis for probabilistic time-bounded reachability, in Proceedings of the IEEE Real-Time Systems Symposium (RTSS 08) (IEEE Computer Society Press, 2008), pp. 173–182
H. Hansson, B. Jonsson, A logic for reasoning about time and reliability. Form. Asp. Comput. 6(5), 512–535 (1994)
A. Hartmanns, H. Hermanns, A modest approach to checking probabilistic timed automata, in Proceedings of the 6th International Conference Quantitative Evaluation of Systems (QEST’09) (2009). To appear
H. Hermanns, Interactive Markov Chains and the Quest for Quantified Quality. LNCS, vol. 2428 (Springer, New York, 2002)
H. Hermanns, B. Wachter, L. Zhang, Probabilistic CEGAR, in Proceedings of the 20th International Conference Computer Aided Verification (CAV’08), ed. By A. Gupta, S. Malik. LNCS, vol. 5123 (Springer, 2008), pp. 162–175
R. Howard, Dynamic Programming and Markov Processes (The MIT Press, Cambridge, 1960)
N. Jansen, F. Corzilius, M. Volk, R. Wimmer, E. Ábrahám, J.-P. Katoen, B. Becker, Accelerating parametric probabilistic verification, in Proceedings of the 11th International Conference Quantitative Evaluation of Systems (QEST’14) (2014), pp. 404–420
B. Jeannet, P. D’Argenio, K. Larsen, Rapture: a tool for verifying Markov decision processes, in Proceedings of the Tools Day, affiliated to 13th International Conference Concurrency Theory (CONCUR’02), ed. By I. Cerna. Technical Report FIMU-RS-2002-05, Faculty of Informatics Masaryk University (2002), pp. 84–98
A. Jensen, Markoff chains as an aid in the study of Markoff processes. Skandinavisk Aktuarietidskrift 36, 87–91 (1953)
H. Jensen, Model checking probabilistic real time systems, in Proceedings of the 7th Nordic Workshop Programming Theory (1996), pp. 247–261
A. Jovanovic, M. Kwiatkowska, Parameter synthesis for probabilistic timed automata using stochastic games, in Proceedings of the 8th International Workshop Reachability Problems (RP’14), ed. By J. Ouaknine, I. Potapov, J. Worrell. LNCS, vol. 8762, (Springer, 2014), pp. 176–189
M. Jurdziński, M. Kwiatkowska, G. Norman, A. Trivedi, Concavely-priced probabilistic timed automata, in Proceedings of the 20th International Conference Concurrency Theory (CONCUR’09), ed. By M. Bravetti, G. Zavattaro. LNCS, vol. 5710 (Springer, 2009), pp. 415–430
J.-P. Katoen, Probabilistic programming: a true challenge in verification, in Proceedings of the 13th International Symposium on Automated Technology for Verification and Analysis (ATVA’15). LNCS (Springer, 2015), pp. 1–3
J.-P. Katoen, T. Kemna, I. Zapreev, D. Jansen, Bisimulation minimisation mostly speeds up probabilistic model checking, in Proceedings of the 13th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS’07), ed. By O. Grumberg, M. Huth. LNCS, vol. 4424 (Springer, 2007), pp. 87–101
J.-P. Katoen, I. Zapreev, E.M. Hahn, H. Hermanns, D. Jansen, The ins and outs of the probabilistic model checker MRMC, in Proceedings of the 6th International Conference Quantitative Evaluation of Systems (QEST’09) (IEEE Computer Society Press, 2009), pp. 167–176
M. Kattenbelt, M. Kwiatkowska, G. Norman, D. Parker, Abstraction refinement for probabilistic software, in Proceedings of the 10th International Conference Verification, Model Checking, and Abstract Interpretation (VMCAI’09), ed. By N. Jones, M. Muller-Olm. LNCS, vol. 5403 (Springer, 2009), pp. 182–197
M. Kattenbelt, M. Kwiatkowska, G. Norman, D. Parker, A game-based abstraction-refinement framework for Markov decision processes. Form. Methods Syst. Des. 36(3), 246–280 (2010)
J. Kemeny, J. Snell, A. Knapp, Denumerable Markov Chains, 2nd edn. (Springer, Heidelberg, 1976)
M. Kwiatkowska, G. Norman, D. Parker, Symmetry reduction for probabilistic model checking, in Proceedings of the 18th International Conference Computer Aided Verification (CAV’06), ed. By T. Ball, R. Jones. LNCS, vol. 4114 (Springer, 2006), pp. 234–248
M. Kwiatkowska, G. Norman, D. Parker, Stochastic model checking, in Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM’07), ed. By M. Bernardo, J. Hillston. LNCS (Tutorial Volume), vol. 4486 (Springer, 2007), pp. 220–270
M. Kwiatkowska, G. Norman, D. Parker, Stochastic games for verification of probabilistic timed automata, in Proceedings of the 7th International Conference Formal Modelling and Analysis of Timed Systems (FORMATS’09), ed. By J. Ouaknine, F. Vaandrager. LNCS, vol. 5813 (Springer, 2009), pp. 212–227
M. Kwiatkowska, G. Norman, D. Parker, PRISM 4.0: verification of probabilistic real-time systems, in Proceedings of the 23rd International Conference Computer Aided Verification (CAV’11), ed. By G. Gopalakrishnan, S. Qadeer. LNCS, vol. 6806 (Springer, 2011), pp. 585–591
M. Kwiatkowska, G. Norman, D. Parker, H. Qu, Compositional probabilistic verification through multi-objective model checking. Inf. Comput. 232, 38–65 (2013)
M. Kwiatkowska, G. Norman, D. Parker, J. Sproston, Performance analysis of probabilistic timed automata using digital clocks. Form. Methods Syst. Des. 29, 33–78 (2006)
M. Kwiatkowska, G. Norman, R. Segala, J. Sproston, Verifying quantitative properties of continuous probabilistic timed automata, in In Proceedings of the 11th International Conference Concurrency Theory (CONCUR’00), ed. By C. Palamidessi. LNCS, vol. 1877 (Springer, 2000), pp. 123–137
M. Kwiatkowska, G. Norman, R. Segala, J. Sproston, Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282, 101–150 (2002)
M. Kwiatkowska, G. Norman, J. Sproston, F. Wang, Symbolic model checking for probabilistic timed automata. Inf. Comput. 205(7), 1027–1077 (2007)
M. Kwiatkowska, D. Parker, C. Wiltsche, PRISM-games 2.0: a tool for multi-objective strategy synthesis for stochastic games, in Proceedings of the 22nd International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS’16). LNCS (Springer, 2016)
O. Madani, S. Hanks, A. Condon, On the undecidability of probabilistic planning and related stochastic optimization problems. Artif. Intell. 147(1–2), 5–34 (2003)
O. Maler, K. Larsen, B. Krogh, On zone-based analysis of duration probabilistic automata, in Proceedings of the 12th International Workshop Verification of Infinite-State Systems (INFINITY’10). EPTCS, vol. 39 (2010), pp. 33–46
R. Milner, Calculi for synchrony and asynchrony. Theor. Comput. Sci. 25(3), 267–310 (1993)
R. Nicola, F. Vaandrager, Action versus state based logics for transition systems, in Proceedings of the LITP Spring School on Theoretical Computer Science: Semantics of Systems of Concurrent Processes, ed. By I. Guessarian (Springer, 1990), pp. 407–419
G. Norman, D. Parker, M. Kwiatkowska, S. Shukla, Evaluating the reliability of NAND multiplexing with PRISM. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 24(10), 1629–1637 (2005)
G. Norman, D. Parker, J. Sproston, Model checking for probabilistic timed automata. Form. Methods Syst. Des. 43(2), 164–190 (2013)
G. Norman, D. Parker, X. Zou, Verification and control of partially observable probabilistic real-time systems, in Proceedings of the 13th International Conference Formal Modelling and Analysis of Timed Systems (FORMATS’15), ed. By S. Sankaranarayanan, E. Vicario. LNCS, vol. 9268 (Springer, 2015), pp. 240–255
D. Parker, Implementation of Symbolic Model Checking for Probabilistic Systems. Ph.D. thesis, University of Birmingham, 2002
A. Pnueli, The temporal semantics of concurrent programs. Theor. Comput. Sci. 13, 45–60 (1981)
A. Puggelli, W. Li, A. Sangiovanni-Vincentelli, S. Seshia, Polynomial-time verification of PCTL properties of MDPs with convex uncertainties, in Proceedings of the 25th International Conference Computer Aided Verification (CAV’13). LNCS, vol. 8044 (Springer, 2013), pp. 527–542
M. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming (Wiley, New Jersey, 1994)
S. Ratschan, Z. She, Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans. Embed. Comput. Syst. 6(1) (2007)
A.W. Roscoe, The Theory and Practice of Concurrency (Prentice-Hall, New Jersey, 1997)
R. Segala, Modelling and verification of randomized distributed real time systems. Ph.D. thesis, Massachusetts Institute of Technology, 1995
R. Segala, N. Lynch, Probabilistic simulations for probabilistic processes. Nordic J. Comput. 2(2), 250–273 (1995)
J. Sproston, Decidable model checking of probabilistic hybrid automata, in Proceedings of the International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT’00), ed. By M. Joseph. LNCS, vol. 1926 (Springer, 2000), pp. 31–45
J. Sun, Y. Liu, J.S. Dong, J. Pang, Pat: towards flexible verification under fairness, in Proceedings of the 21st International Conference Computer Aided Verification (CAV’09). LNCS, vol. 5643 (Springer, 2009), pp. 709–714
M. Svorenova, M. Kwiatkowska, Quantitative verification and strategy synthesis for stochastic games. Eur. J. Control 30, 15–30 (2016)
M. Svoreňová, M. Chmelík, K. Leahy, H. Eniser, K. Chatterjee, I. Černá, C. Belta, Temporal logic motion planning using POMDPs with parity objectives: case study paper, in Proceedings of the 18th International Conference Hybrid Systems: Computation and Control (HSCC’15) (ACM, 2015), pp. 233–238
S. Tripakis, The analysis of timed systems in practice. Ph.D. thesis, Université Joseph Fourier, Grenoble, 1998
S. Tripakis, S. Yovine, A. Bouajjan, Checking timed Buchi automata emptiness efficiently. Form. Methods Syst. Des. 26(3), 267–292 (2005)
M. Vardi, P. Wolper, Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994)
J. von Neumann, Probabilistic logics and synthesis of reliable organisms from unreliable components, in Automata Studies, ed. By C. Shannon, J. McCarthy (Princeton University Press, 1956), pp. 43–98
B. Wachter, L. Zhang, H. Hermanns, Probabilistic model checking modulo theories, in Proceedings of the 4th International Conference Quantitative Evaluation of Systems (QEST’07) (IEEE Computer Society Press, 2007), pp. 129–140
C. Wiltsche, Assume-Guarantee Strategy Synthesis for Stochastic Games. Ph.D thesis, University of Oxford, 2015
E. Wolff, U. Topcu, R. Murray, Robust control of uncertain Markov decision processes with temporal logic specifications, in Proceedings of the IEEE 51st Annual Conference Decision and Control (CDC’12) (Computer Society Press, 2012), pp. 3372–3379
L. Zhang, Z. She, S. Ratschan, H. Hermanns, E.M. Hahn, Safety verification for probabilistic hybrid systems. Eur. J. Control 18(6), 572–587 (2012)
Acknowledgements
This work was supported by the ERC Advanced Investigators Grant VERIWARE, the EPSRC Mobile Autonomy Programme Grant EP/M019918/1, the EU FP7-funded project HIERATIC and the DARPA-funded BRASS project.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG
About this chapter
Cite this chapter
Kwiatkowska, M., Norman, G., Parker, D. (2018). Probabilistic Model Checking: Advances and Applications. In: Drechsler, R. (eds) Formal System Verification. Springer, Cham. https://doi.org/10.1007/978-3-319-57685-5_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-57685-5_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-57683-1
Online ISBN: 978-3-319-57685-5
eBook Packages: EngineeringEngineering (R0)