Advertisement

Probabilistic Model Checking: Advances and Applications

Chapter

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.

Notes

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.

References

  1. 1.
    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–121Google Scholar
  2. 2.
    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–136Google Scholar
  3. 3.
    R. Alur, C. Courcoubetis, D. Dill, Model checking in dense real time. Inf. Comput. 104(1), 2–34 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    R. Alur, T. Dang, F. Ivancic, Predicate abstraction for reachability analysis of hybrid systems. ACM Trans. Embed. Comput. Syst. 5(1), 152–199 (2006)CrossRefzbMATHGoogle Scholar
  5. 5.
    R. Alur, D. Dill, A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    R. Alur, T. Henzinger, O. Kupferman, Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    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–344Google Scholar
  8. 8.
    R. Alur, S. La Torre, G. Pappas, Optimal paths in weighted timed automata. Theor. Comput. Sci. 318(3), 297–322 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    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–174Google Scholar
  10. 10.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    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)CrossRefzbMATHGoogle Scholar
  12. 12.
    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–440Google Scholar
  13. 13.
    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–5062Google Scholar
  14. 14.
    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)CrossRefzbMATHGoogle Scholar
  15. 15.
    C. Baier, J.-P. Katoen, Principles of Model Checking (MIT Press, Cambridge, 2008)zbMATHGoogle Scholar
  16. 16.
    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–340Google Scholar
  17. 17.
    D. Beauquier, Probabilistic timed automata. Theor. Comput. Sci. 292(1), 65–84 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    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–125Google Scholar
  19. 19.
    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–188Google Scholar
  20. 20.
    R. Bellman, Dynamic Programming (Princeton University Press, New Jersey, 1957)zbMATHGoogle Scholar
  21. 21.
    P. Billingsley, Probability and Measure (Wiley, New Jersey, 1995)zbMATHGoogle Scholar
  22. 22.
    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)CrossRefGoogle Scholar
  23. 23.
    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–358Google Scholar
  24. 24.
    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–123Google Scholar
  25. 25.
    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–242Google Scholar
  26. 26.
    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–98Google Scholar
  27. 27.
    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–330Google Scholar
  28. 28.
    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)CrossRefzbMATHGoogle Scholar
  29. 29.
    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
  30. 30.
    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–169Google Scholar
  31. 31.
    A. Condon, The complexity of stochastic games. Inf. Comput. 96(2), 203–224 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  32. 32.
    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)Google Scholar
  33. 33.
    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–260Google Scholar
  34. 34.
    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–56Google Scholar
  35. 35.
    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–294Google Scholar
  36. 36.
    L. de Alfaro, Formal Verification of Probabilistic Systems. Ph.D. thesis, Stanford University, 1997Google Scholar
  37. 37.
    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–231Google Scholar
  38. 38.
    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–119Google Scholar
  39. 39.
    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–23Google Scholar
  40. 40.
    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)Google Scholar
  41. 41.
    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–351Google Scholar
  42. 42.
    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)MathSciNetzbMATHGoogle Scholar
  43. 43.
    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)CrossRefGoogle Scholar
  44. 44.
    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–113Google Scholar
  45. 45.
    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–127Google Scholar
  46. 46.
    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–332Google Scholar
  47. 47.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  48. 48.
    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–83Google Scholar
  49. 49.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  50. 50.
    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–427Google Scholar
  51. 51.
    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)Google Scholar
  52. 52.
    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–664Google Scholar
  53. 53.
    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–357Google Scholar
  54. 54.
    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)CrossRefGoogle Scholar
  55. 55.
    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–317Google Scholar
  56. 56.
    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–78Google Scholar
  57. 57.
    J. Han, P. Jonker, A system architecture solution for unreliable nanoelectronic devices. IEEE Trans. Nanotechnol. 1, 201–208 (2002)CrossRefGoogle Scholar
  58. 58.
    T. Han, J.-P. Katoen, B. Damman, Counterexample generation in probabilistic model checking. IEEE Trans. Softw. Eng. 35(2), 241–257 (2009)Google Scholar
  59. 59.
    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–182Google Scholar
  60. 60.
    H. Hansson, B. Jonsson, A logic for reasoning about time and reliability. Form. Asp. Comput. 6(5), 512–535 (1994)CrossRefzbMATHGoogle Scholar
  61. 61.
    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 appearGoogle Scholar
  62. 62.
    H. Hermanns, Interactive Markov Chains and the Quest for Quantified Quality. LNCS, vol. 2428 (Springer, New York, 2002)Google Scholar
  63. 63.
    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–175Google Scholar
  64. 64.
    R. Howard, Dynamic Programming and Markov Processes (The MIT Press, Cambridge, 1960)Google Scholar
  65. 65.
    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–420Google Scholar
  66. 66.
    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–98Google Scholar
  67. 67.
    A. Jensen, Markoff chains as an aid in the study of Markoff processes. Skandinavisk Aktuarietidskrift 36, 87–91 (1953)MathSciNetzbMATHGoogle Scholar
  68. 68.
    H. Jensen, Model checking probabilistic real time systems, in Proceedings of the 7th Nordic Workshop Programming Theory (1996), pp. 247–261Google Scholar
  69. 69.
    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–189Google Scholar
  70. 70.
    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–430Google Scholar
  71. 71.
    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–3Google Scholar
  72. 72.
    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–101Google Scholar
  73. 73.
    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–176Google Scholar
  74. 74.
    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–197Google Scholar
  75. 75.
    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)CrossRefzbMATHGoogle Scholar
  76. 76.
    J. Kemeny, J. Snell, A. Knapp, Denumerable Markov Chains, 2nd edn. (Springer, Heidelberg, 1976)Google Scholar
  77. 77.
    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–248Google Scholar
  78. 78.
    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–270Google Scholar
  79. 79.
    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–227Google Scholar
  80. 80.
    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–591Google Scholar
  81. 81.
    M. Kwiatkowska, G. Norman, D. Parker, H. Qu, Compositional probabilistic verification through multi-objective model checking. Inf. Comput. 232, 38–65 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  82. 82.
    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)CrossRefzbMATHGoogle Scholar
  83. 83.
    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–137Google Scholar
  84. 84.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  85. 85.
    M. Kwiatkowska, G. Norman, J. Sproston, F. Wang, Symbolic model checking for probabilistic timed automata. Inf. Comput. 205(7), 1027–1077 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  86. 86.
    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)Google Scholar
  87. 87.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  88. 88.
    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–46Google Scholar
  89. 89.
    R. Milner, Calculi for synchrony and asynchrony. Theor. Comput. Sci. 25(3), 267–310 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  90. 90.
    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–419Google Scholar
  91. 91.
    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)CrossRefGoogle Scholar
  92. 92.
    G. Norman, D. Parker, J. Sproston, Model checking for probabilistic timed automata. Form. Methods Syst. Des. 43(2), 164–190 (2013)CrossRefzbMATHGoogle Scholar
  93. 93.
    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–255Google Scholar
  94. 94.
    D. Parker, Implementation of Symbolic Model Checking for Probabilistic Systems. Ph.D. thesis, University of Birmingham, 2002Google Scholar
  95. 95.
    A. Pnueli, The temporal semantics of concurrent programs. Theor. Comput. Sci. 13, 45–60 (1981)MathSciNetCrossRefzbMATHGoogle Scholar
  96. 96.
    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–542Google Scholar
  97. 97.
    M. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming (Wiley, New Jersey, 1994)Google Scholar
  98. 98.
    S. Ratschan, Z. She, Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans. Embed. Comput. Syst. 6(1) (2007)Google Scholar
  99. 99.
    A.W. Roscoe, The Theory and Practice of Concurrency (Prentice-Hall, New Jersey, 1997)Google Scholar
  100. 100.
    R. Segala, Modelling and verification of randomized distributed real time systems. Ph.D. thesis, Massachusetts Institute of Technology, 1995Google Scholar
  101. 101.
    R. Segala, N. Lynch, Probabilistic simulations for probabilistic processes. Nordic J. Comput. 2(2), 250–273 (1995)MathSciNetzbMATHGoogle Scholar
  102. 102.
    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–45Google Scholar
  103. 103.
    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–714Google Scholar
  104. 104.
    M. Svorenova, M. Kwiatkowska, Quantitative verification and strategy synthesis for stochastic games. Eur. J. Control 30, 15–30 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  105. 105.
    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–238Google Scholar
  106. 106.
    S. Tripakis, The analysis of timed systems in practice. Ph.D. thesis, Université Joseph Fourier, Grenoble, 1998Google Scholar
  107. 107.
    S. Tripakis, S. Yovine, A. Bouajjan, Checking timed Buchi automata emptiness efficiently. Form. Methods Syst. Des. 26(3), 267–292 (2005)CrossRefzbMATHGoogle Scholar
  108. 108.
    M. Vardi, P. Wolper, Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  109. 109.
    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–98Google Scholar
  110. 110.
    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–140Google Scholar
  111. 111.
    C. Wiltsche, Assume-Guarantee Strategy Synthesis for Stochastic Games. Ph.D thesis, University of Oxford, 2015Google Scholar
  112. 112.
    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–3379Google Scholar
  113. 113.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  114. 114.
  115. 115.
  116. 116.
  117. 117.

Copyright information

© Springer International Publishing AG 2018

Authors and Affiliations

  1. 1.Department of Computer ScienceUniversity of OxfordOxfordUK
  2. 2.School of Computing ScienceUniversity of GlasgowGlasgowUK
  3. 3.School of Computer ScienceUniversity of BirminghamBirminghamUK

Personalised recommendations