1932
0
  1. Home
  2. A-Z Publications
  3. Annual Review of Control, Robotics, and Autonomous Systems
  4. Volume 5, 2022
  5. Article

Annual Review of Control, Robotics, and Autonomous Systems

Volume 5, 2022

Probabilistic Model Checking and Autonomy

Abstract

The design and control of autonomous systems that operate in uncertain or adversarial environments can be facilitated by formal modeling and analysis. Probabilistic model checking is a technique to automatically verify, for a given temporal logic specification, that a system model satisfies the specification, as well as to synthesize an optimal strategy for its control. This method has recently been extended to multiagent systems that exhibit competitive or cooperative behavior modeled via stochastic games and synthesis of equilibria strategies. In this article, we provide an overview of probabilistic model checking, focusing on models supported by the PRISM and PRISM-games model checkers. This overview includes fully observable and partially observable Markov decision processes, as well as turn-based and concurrent stochastic games, together with associated probabilistic temporal logics. We demonstrate the applicability of the framework through illustrative examples from autonomous systems. Finally, we highlight research challenges and suggest directions for future work in this area.

Keyword(s): equilibria, model checking, probabilistic modeling, stochastic games, strategy synthesis, temporal logic
Loading

Article metrics loading...

/content/journals/10.1146/annurev-control-042820-010947
2022-05-03
2024-05-14
Loading full text...

Full text loading...

/deliver/fulltext/control/5/1/annurev-control-042820-010947.html?itemId=/content/journals/10.1146/annurev-control-042820-010947&mimeType=html&fmt=ahah

Literature Cited

  1. 1. 
    Kwiatkowska M, Norman G, Parker D 2011. PRISM 4.0: verification of probabilistic real-time systems. Computer Aided Verification: 23rd International Conference, CAV 2011 G Gopalakrishnan, S Qadeer 585–91 Berlin: Springer
     [Google Scholar]
  2. 2. 
    Kwiatkowska M, Norman G, Parker D, Santos G 2020. PRISM-games 3.0: stochastic game verification with concurrency, equilibria and time. Computer Aided Verification 32nd International Conference, CAV 2020 S Lahiri, C Wang 475–87 Cham, Switz: Springer
     [Google Scholar]
  3. 3. 
    Puterman M. 1994. Markov Decision Processes: Discrete Stochastic Dynamic Programming New York: Wiley & Sons
  4. 4. 
    Lacerda B, Parker D, Hawes N 2014. Optimal and dynamic planning for Markov decision processes with co-safe LTL specifications. 2014 IEEE/RSJ International Conference on Intelligent Robots and Systems1511–16 Piscataway, NJ: IEEE
     [Google Scholar]
  5. 5. 
    Kemeny J, Snell J, Knapp A. 1976. Denumerable Markov Chains New York: Springer
  6. 6. 
    Hansson H, Jonsson B. 1994. A logic for reasoning about time and reliability. Form. Asp. Comput. 6:512–35
     [Google Scholar]
  7. 7. 
    Pnueli A. 1981. The temporal semantics of concurrent programs. Theor. Comput. Sci. 13:45–60
     [Google Scholar]
  8. 8. 
    Forejt V, Kwiatkowska M, Norman G, Parker D 2011. Automated verification techniques for probabilistic systems. Formal Methods for Eternal Networked Software Systems: 11th International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM 2011 M Bernardo, V Issarny 53–113 Berlin: Springer
     [Google Scholar]
  9. 9. 
    Haddad S, Monmege B. 2018. Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. 735:111–31
     [Google Scholar]
  10. 10. 
    Brázdil T, Chatterjee K, Chmelík M, Forejt V, Křetínský J et al. 2014. Verification of Markov decision processes using learning algorithms. Automated Technology for Verification and Analysis: 12th International Symposium, ATVA 2014 F Cassez, JF Raskin 98–114 Cham, Switz: Springer
     [Google Scholar]
  11. 11. 
    Křetínský J, Meggendorfer T. 2020. Of cores: a partial-exploration framework for Markov decision processes. Log. Methods Comput. Sci. 16:43
     [Google Scholar]
  12. 12. 
    Baier C, Katoen JP. 2008. Principles of Model Checking Cambridge, MA: MIT Press
  13. 13. 
    de Alfaro L. 1997. Formal verification of probabilistic systems PhD Thesis, Stanford Univ. Stanford, CA:
  14. 14. 
    Bellman R. 1957. Dynamic Programming Princeton, NJ: Princeton Univ. Press
  15. 15. 
    Etessami K, Kwiatkowska M, Vardi M, Yannakakis M. 2008. Multi-objective model checking of Markov decision processes. Log. Methods Comput. Sci. 4:48
     [Google Scholar]
  16. 16. 
    Forejt V, Kwiatkowska M, Norman G, Parker D, Qu H 2011. Quantitative multi-objective verification for probabilistic systems. Tools and Algorithms for the Construction and Analysis of Systems: 17th International Conference, TACAS 2011 PA Abdulla, KRM Leino 112–27 Berlin: Springer
     [Google Scholar]
  17. 17. 
    Forejt V, Kwiatkowska M, Parker D 2012. Pareto curves for probabilistic model checking. Automated Technology for Verification and Analysis: 10th International Symposium, ATVA 2012 ed. S Chakraborty, M Mukund 317–32 Berlin: Springer
     [Google Scholar]
  18. 18. 
    Lahijanian M, Svorenova M, Morye AA, Yeomans B, Rao D et al. 2018. Resource-performance trade-off analysis for mobile robots. IEEE Robot. Autom. Lett. 3:1840–47
     [Google Scholar]
  19. 19. 
    Daws C 2004. Symbolic and parametric model checking of discrete-time Markov chains. Theoretical Aspects of Computing – ICTAC 2004: First International Colloquium Z Liu, K Araki 280–94 Berlin: Springer
     [Google Scholar]
  20. 20. 
    Hahn E, Hermanns H, Zhang L. 2011. Probabilistic reachability for parametric Markov models. Int. J. Softw. Tools Technol. Transf. 13:3–19
     [Google Scholar]
  21. 21. 
    Jansen N, Corzilius F, Volk M, Wimmer R, Ábrahám E et al. 2014. Accelerating parametric probabilistic verification. Quantitative Evaluation of Systems: 11th International Conference, QEST 2014 G Norman, W Sanders 404–20 Cham, Switz: Springer
     [Google Scholar]
  22. 22. 
    Hahn E, Han T, Zhang L 2011. Synthesis for PCTL in parametric Markov decision processes. NASA Formal Methods: Third International Symposium, NFM 2011 M Bobaru, K Havelund, GJ Holzmann, R Joshi 146–61 Berlin: Springer
     [Google Scholar]
  23. 23. 
    Quatmann T, Dehnert C, Jansen N, Junges S, Katoen JP 2016. Parameter synthesis for Markov models: faster than ever. Automated Technology for Verification and Analysis: 14th International Symposium, ATVA 2016 C Artho, A Legay, D Peled 50–67 Cham, Switz: Springer
     [Google Scholar]
  24. 24. 
    Givan R, Leach S, Dean T. 2000. Bounded-parameter Markov decision processes. Artif. Intell. 122:71–109
     [Google Scholar]
  25. 25. 
    Wolff E, Topcu U, Murray R 2012. Robust control of uncertain Markov decision processes with temporal logic specifications. 2012 51st IEEE Conference on Decision and Control3372–79 Piscataway, NJ: IEEE
     [Google Scholar]
  26. 26. 
    Puggelli A, Li W, Sangiovanni-Vincentelli A, Seshia S 2015. Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. Computer Aided Verification: 25th International Conference, CAV 2013 N Sharygina, H Veith 527–42 Berlin: Springer
     [Google Scholar]
  27. 27. 
    Hahn E, Hashemi V, Hermanns H, Lahijanian M, Turrini A 2019. Interval Markov decision processes with multiple objectives: from robust strategies to Pareto curves. ACM Trans. Model. Comput. Simul. 29:27
     [Google Scholar]
  28. 28. 
    Alur R, Henzinger T. 1999. Reactive modules. Form. Methods Syst. Des. 15:7–48
     [Google Scholar]
  29. 29. 
    Dehnert C, Junges S, Katoen JP, Volk M. 2017. A Storm is coming: a modern probabilistic model checker. Computer Aided Verification: 29th International Conference, CAV 2017 R Majumdar, V Kunčak 592–600 Cham, Switz: Springer
     [Google Scholar]
  30. 30. 
    Budde C, Dehnert C, Hahn E, Hartmanns A, Junges S, Turrini A 2017. JANI: quantitative model and tool interaction. Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference, TACAS 2017 A Legay, T Margaria 151–68 Berlin: Springer
     [Google Scholar]
  31. 31. 
    Hartmanns A, Hermanns H 2014. The Modest Toolset: an integrated environment for quantitative modelling and verification. Tools and Algorithms for the Construction and Analysis of Systems: 20th International Conference, TACAS 2014 E Ábrahám, K Havelund 593–98 Berlin: Springer
     [Google Scholar]
  32. 32. 
    Hahn EM, Li Y, Schewe S, Turrini A, Zhang L 2014. iscasMc: a web-based probabilistic model checker. FM 2014: Formal Methods C Jones, P Pihlajasaari, J Sun 312–17 Cham, Switz: Springer
     [Google Scholar]
  33. 33. 
    Hahn E, Hermanns H, Wachter B, Zhang L 2010. PARAM: a model checker for parametric Markov models. Computer Aided Verification: 22nd International Conference, CAV 2010 T Touili, B Cook, P Jackson 660–64 Berlin: Springer
     [Google Scholar]
  34. 34. 
    Dehnert C, Junges S, Jansen N, Corzilius F, Volk M et al. 2015. PROPhESY: a PRObabilistic ParamEter SYnthesis tool. Computer Aided Verification: 27th International Conference, CAV 2015 D Kroening, CS Pǎsǎreanu 214–31 Cham, Switz: Springer
     [Google Scholar]
  35. 35. 
    Lahijanian M, Andersson S, Belta C 2012. Temporal logic motion planning and control with probabilistic satisfaction. IEEE Trans. Robot. 28:396–409
     [Google Scholar]
  36. 36. 
    Lahijanian M, Andersson S, Belta C 2015. Formal verification and synthesis for discrete-time stochastic systems. IEEE Trans. Autom. Control 60:2031–45
     [Google Scholar]
  37. 37. 
    Fraser D, Giaquinta R, Hoffmann R, Ireland M, Miller A, Norman G. 2020. Collaborative models for autonomous systems controller synthesis. Form. Asp. Comput. 32:157–86
     [Google Scholar]
  38. 38. 
    Nardone V, Santone A, Tipaldi M, Glielmo L. 2016. Probabilistic model checking applied to autonomous spacecraft reconfiguration. 2016 IEEE Metrology for Aerospace556–60 Piscataway, NJ: IEEE
     [Google Scholar]
  39. 39. 
    Lacerda B, Faruq F, Parker D, Hawes N 2019. Probabilistic planning with formal performance guarantees for mobile service robots. Int. J. Robot. Res. 38:1098–123
     [Google Scholar]
  40. 40. 
    Zhao X, Robu V, Flynn D, Dinmohammadi F, Fisher M, Webster M. 2019. Probabilistic model checking of robots deployed in extreme environments. The Thirty-Third AAAI Conference on Artificial Intelligence8066–74 Palo Alto, CA: AAAI Press
     [Google Scholar]
  41. 41. 
    Li N, Adepu S, Kang E, Garlan D. 2020. Explanations for human-on-the-loop: a probabilistic model checking approach. SEAMS '20: Proceedings of the IEEE/ACM 15th International Symposium on Software Engineering for Adaptive and Self-Managing Systems181–87 New York: ACM
     [Google Scholar]
  42. 42. 
    Tomy M, Lacerda B, Hawes N, Wyatt J. 2019. Battery charge scheduling in long-life autonomous mobile robots. 2019 European Conference on Mobile Robots Piscataway, NJ: IEEE https://doi.org/10.1109/ECMR.2019.8870951
    [Crossref] [Google Scholar]
  43. 43. 
    Calinescu R, Ghezzi C, Kwiatkowska M, Mirandola R. 2012. Self-adaptive software needs quantitative verification at runtime. Commun. ACM 55:969–77
     [Google Scholar]
  44. 44. 
    Luckcuck M, Farrell M, Dennis L, Dixon C, Fisher M. 2019. Formal specification and verification of autonomous robotic systems: a survey. ACM Comput. Surv. 52:100
     [Google Scholar]
  45. 45. 
    Baier C, Bertrand N, Größer M 2008. On decision problems for probabilistic Büchi automata. Foundations of Software Science and Computational Structures: 11th International Conference, FOSSACS 2008 R Amadio 287–301 Berlin: Springer
     [Google Scholar]
  46. 46. 
    Chatterjee K, Chmelík M, Tracol M 2013. What is decidable about partially observable Markov decision processes with omega-regular objectives. Computer Science Logic 2013165–80 Saarbrücken, Ger: Schloss Dagstuhl
     [Google Scholar]
  47. 47. 
    Chatterjee K, Chmelík M, Gupta R, Kanodia A. 2016. Optimal cost almost-sure reachability in POMDPs. Artif. Intell. 234:26–48
     [Google Scholar]
  48. 48. 
    Madani O, Hanks S, Condon A. 2003. On the undecidability of probabilistic planning and related stochastic optimization problems. Artif. Intell. 147:5–34
     [Google Scholar]
  49. 49. 
    Poupart P. 2005. Exploiting structure to efficiently solve large scale partially observable Markov decision processes PhD Thesis, Univ. Toronto Toronto:
  50. 50. 
    Norman G, Parker D, Zou X 2015. Verification and control of partially observable probabilistic real-time systems. Formal Modeling and Analysis of Timed Systems: 13th International Conference, FORMATS 2015 S Sankaranarayanan, E Vicario 240–55 Cham, Switz: Springer
     [Google Scholar]
  51. 51. 
    Lovejoy W. 1991. Computationally feasible bounds for partially observed Markov decision processes. Oper. Res. 39:162–75
     [Google Scholar]
  52. 52. 
    Yu H, Bertsekas D 2004. Discretized approximations for POMDP with average cost. UAI '04: Proceedings of the 20th Conference on Uncertainty in Artificial Intelligence619–27 Arlington, VA: AUAI Press
     [Google Scholar]
  53. 53. 
    Bork A, Junges S, Katoen JP, Quatmann T. 2020. Verification of indefinite-horizon POMDPs. Automated Technology for Verification and Analysis: 18th International Symposium, ATVA 2020 DV Hung, O Sokolsky 288–304 Cham, Switz: Springer
     [Google Scholar]
  54. 54. 
    Bouton M, Tumova J, Kochenderfer M. 2020. Point-based methods for model checking in partially observable Markov decision processes. The Thirty-Fourth AAAI Conference on Artificial Intelligence10061–68 Palo Alto, CA: AAAI Press
     [Google Scholar]
  55. 55. 
    Chatterjee K, Chmelík M, Gupta R, Kanodia A. 2015. Qualitative analysis of POMDPs with temporal logic specifications for robotics applications. 2015 IEEE International Conference on Robotics and Automation325–30 Piscataway, NJ: IEEE
     [Google Scholar]
  56. 56. 
    Junges S, Jansen N, Wimmer R, Quatmann T, Winterer L et al. 2018. Finite-state controllers of POMDPs using parameter synthesis. UAI '18: Proceedings of the Thirty-Fourth Conference on Uncertainty in Artificial Intelligence519–29 Arlington, VA: AUAI Press
     [Google Scholar]
  57. 57. 
    Winterer L, Junges S, Wimmer R, Jansen N, Topcu U et al. 2021. Strategy synthesis for POMDPs in robot planning via game-based abstractions. IEEE Trans. Autom. Control 66:1040–54
     [Google Scholar]
  58. 58. 
    Carr S, Jansen N, Topcu U. 2020. Verifiable RNN-based policies for POMDPs under temporal logic constraints. Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence4121–27 Calif.: Int. Joint Conf. Artif. Intell.
     [Google Scholar]
  59. 59. 
    Giro S, Rabe M 2012. Verification of partial-information probabilistic systems using counterexample-guided refinements. Automated Technology for Verification and Analysis: 10th International Symposium, ATVA 2012 S Chakraborty, M Mukund 333–48 Berlin: Springer
     [Google Scholar]
  60. 60. 
    Cerný P, Chatterjee K, Henzinger T, Radhakrishna A, Singh R 2011. Quantitative synthesis for concurrent programs. Computer Aided Verification: 23rd International Conference, CAV 2011, ed. G Gopalakrishnan, S Qadeer 243–59 Berlin: Springer
     [Google Scholar]
  61. 61. 
    Suilen M, Jansen N, Cubuktepe M, Topcu U 2020. Robust policy synthesis for uncertain POMDPs via convex optimization. Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence4121–27 Calif.: Int. Joint Conf. Artif. Intell.
     [Google Scholar]
  62. 62. 
    Carr S, Jansen N, Wimmer R, Fu J, Topcu U. 2018. Human-in-the loop synthesis for partially observable Markov decision processes. 2018 American Control Conference762–69 Piscataway, NJ: IEEE
     [Google Scholar]
  63. 63. 
    Feng L, Wiltsche C, Humphrey L, Topcu U 2016. Synthesis of human-in-the-loop control protocols for autonomous systems. IEEE Trans. Autom. Sci. Eng. 13:450–62
     [Google Scholar]
  64. 64. 
    Alur R, Henzinger T, Kupferman O. 2002. Alternating-time temporal logic. J. ACM 49:672–713
     [Google Scholar]
  65. 65. 
    Chen T, Forejt V, Kwiatkowska M, Parker D, Simaitis A 2013. Automatic verification of competitive stochastic systems. Form. Methods Syst. Des. 43:61–92
     [Google Scholar]
  66. 66. 
    von Neumann J, Morgenstern O, Kuhn H, Rubinstein A. 1944. Theory of Games and Economic Behavior Princeton, NJ: Princeton Univ. Press
  67. 67. 
    Martin D. 1998. The determinacy of Blackwell games. J. Symbol. Log. 63:1565–81
     [Google Scholar]
  68. 68. 
    Condon A 1993. On algorithms for simple stochastic games. Advances in Computational Complexity Theory J-Y Cai 51–73 Providence, RI: Am. Math. Soc.
     [Google Scholar]
  69. 69. 
    Kelmendi E, Krämer J, Kretínský J, Weininger M 2018. Value iteration for simple stochastic games: stopping criterion and learning algorithm. Computer Aided Verification: 30th International Conference, CAV 2018 H Chockler, G Weissenbacher 623–42 Cham, Switz: Springer
     [Google Scholar]
  70. 70. 
    Chatterjee K, Henzinger T 2006. Strategy improvement and randomized subexponential algorithms for stochastic parity games. STACS 2006: 23rd Annual Symposium on Theoretical Aspects of Computer Science B Durand, W Thomas 512–23 Berlin: Springer
     [Google Scholar]
  71. 71. 
    Chatterjee K, Henzinger T. 2012. A survey of stochastic ω-regular games. J. Comput. Syst. Sci. 78:394–413
     [Google Scholar]
  72. 72. 
    Chen T, Kwiatkowska M, Simaitis A, Wiltsche C 2013. Synthesis for multi-objective stochastic games: an application to autonomous urban driving. Quantitative Evaluation of Systems: 10th International Conference, QEST 2013 K Joshi, M Siegle, M Stoelinga, PR D'Argenio 322–37 Berlin: Springer
     [Google Scholar]
  73. 73. 
    Basset N, Kwiatkowska M, Wiltsche C. 2018. Compositional strategy synthesis for stochastic games with multiple objectives. Inf. Comput. 261:536–87
     [Google Scholar]
  74. 74. 
    Basset N, Kwiatkowska M, Topcu U, Wiltsche C 2015. Strategy synthesis for stochastic games with multiple long-run objectives. Tools and Algorithms for the Construction and Analysis of Systems: 21st International Conference, TACAS 2015 C Baier, C Tinelli 256–71 Berlin: Springer
     [Google Scholar]
  75. 75. 
    Feng L, Wiltsche C, Humphrey L, Topcu U 2015. Controller synthesis for autonomous systems interacting with human operators. ICCPS '15: Proceedings of the ACM/IEEE Sixth International Conference on Cyber-Physical Systems70–79 New York: ACM
     [Google Scholar]
  76. 76. 
    Junges S, Jansen N, Katoen JP, Topcu U, Zhang R 2018. Model checking for safe navigation among humans. Quantitative Evaluation of Systems: 15th International Conference, QEST 2018 A McIver, A Horvath 207–22 Cham, Switz: Springer
     [Google Scholar]
  77. 77. 
    Glazier T, Cámara J, Schmerl B, Garlan D. 2015. Analyzing resilience properties of different topologies of collective adaptive systems. 2015 IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops55–60 Piscataway, NJ: IEEE
     [Google Scholar]
  78. 78. 
    Glazier T, Garlan D, Schmerl B. 2020. Automated management of collections of autonomic systems. 2020 IEEE International Conference on Autonomic Computing and Self-Organizing Systems82–91 Piscataway, NJ: IEEE
     [Google Scholar]
  79. 79. 
    Cámara J, Garlan D, Schmerl B, Pandey A. 2015. Optimal planning for architecture-based self-adaptation via model checking of stochastic games. SAC '15: Proceedings of the 30th Annual ACM Symposium on Applied Computing428–35 New York: ACM
     [Google Scholar]
  80. 80. 
    Chatterjee K, Henzinger T, Jobstmann B, Radhakrishna A 2010. Gist: a solver for probabilistic games. Computer Aided Verification: 22nd International Conference, CAV 2010 T Touili, B Cook, P Jackson 665–69 Berlin: Springer
     [Google Scholar]
  81. 81. 
    Cheng C, Knoll A, Luttenberger M, Buckl C 2011. GAVS+: an open platform for the research of algorithmic game solving. Tools and Algorithms for the Construction and Analysis of Systems: 17th International Conference, TACAS 2011 PA Abdulla, KRM Leino 258–61 Berlin: Springer
     [Google Scholar]
  82. 82. 
    Nash J. 1950. Equilibrium points in n-person games. PNAS 36:48–49
     [Google Scholar]
  83. 83. 
    Kwiatkowska M, Norman G, Parker D, Santos G 2021. Automatic verification of concurrent stochastic systems. Form. Methods Syst. Des. In press. https://doi.org/10.1007/s10703-020-00356-y
    [Crossref] [Google Scholar]
  84. 84. 
    Osborne M, Rubinstein A 2004. An Introduction to Game Theory Oxford, UK: Oxford Univ. Press
  85. 85. 
    Bouyer P, Markey N, Stan D 2014. Mixed Nash equilibria in concurrent games. 34th International Conference on Foundations of Software Technology and Theoretical Computer Science V Raman, SP Suresh 351–63 Saarbrücken, Ger: Schloss Dagstuhl
     [Google Scholar]
  86. 86. 
    de Alfaro L, Henzinger T, Kupferman O. 2007. Concurrent reachability games. Theor. Comput. Sci. 386:188–217
     [Google Scholar]
  87. 87. 
    Chatterjee K, de Alfaro L, Henzinger T. 2013. Strategy improvement for concurrent reachability and turn-based stochastic safety games. J. Comput. Syst. Sci. 79:640–57
     [Google Scholar]
  88. 88. 
    Chen T, Forejt V, Kwiatkowska M, Simaitis A, Wiltsche C 2013. On stochastic games with multiple objectives. Mathematical Foundations of Computer Science 2013: 38th International Symposium, MFCS 2013 K Chatterjee, J Sgall 266–77 Berlin: Springer
     [Google Scholar]
  89. 89. 
    Karmarkar N. 1984. A new polynomial-time algorithm for linear programming. Combinatorica 4:373–95
     [Google Scholar]
  90. 90. 
    Papadimitriou C. 1994. On the complexity of the parity argument and other inefficient proofs of existence. J. Comput. Syst. Sci. 48:498–532
     [Google Scholar]
  91. 91. 
    Hansen K, Ibsen-Jensen R, Miltersen P. 2011. The complexity of solving reachability games using value and strategy iteration. Theory Comput. Syst. 55:380–403
     [Google Scholar]
  92. 92. 
    Kwiatkowska M, Norman G, Parker D, Santos G 2020. Multi-player equilibria verification for concurrent stochastic games. Quantitative Evaluation of Systems: 17th International Conference, QEST 2020 M Gribaudo, DN Jansen, A Remke 74–95 Cham, Switz: Springer
     [Google Scholar]
  93. 93. 
    Daskalakis C, Goldberg P, Papadimitriou C. 2009. The complexity of computing a Nash equilibrium. Commun. ACM 52:289–97
     [Google Scholar]
  94. 94. 
    Chatterjee K, Majumdar R, Jurdziński M 2004. On Nash equilibria in stochastic games. Computer Science Logic: 18th International Workshop, CSL 2004, ed. RJ Aumann, S Hart 26–40 Berlin: Springer
     [Google Scholar]
  95. 95. 
    Ummels M. 2010. Stochastic multiplayer games: theory and algorithms PhD Thesis, RWTH Aachen Univ. Aachen, Ger:.
  96. 96. 
    Brihaye T, Bruyère V, Goeminne A, Raskin JF, van den Bogaard M. 2019. The complexity of subgame perfect equilibria in quantitative reachability games. 30th International Conference on Concurrency Theory WJ Fokkink, R van Glabbeek 1–16 Saarbrücken, Ger: Schloss Dagstuhl
     [Google Scholar]
  97. 97. 
    Gutierrez J, Najib M, Giuseppe P, Wooldridge M 2019. Equilibrium design for concurrent games. 30th International Conference on Concurrency Theory WJ Fokkink, R van Glabbeek 1–16 Saarbrücken, Ger: Schloss Dagstuhl
     [Google Scholar]
  98. 98. 
    Bouyer P, Markey N, Stan D 2016. Stochastic equilibria under imprecise deviations in terminal-reward concurrent games. Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification D Cantone, G Delzonne 61–75 Waterloo, Aust: Open Publ. Assoc.
     [Google Scholar]
  99. 99. 
    Jensen H. 1996. Model checking probabilistic real time systems. Proceedings of the 7th Nordic Workshop on Programming Theory247–61 Göteborg, Swed: Chalmers Tekniska Högsk./Göteborg Univ.
     [Google Scholar]
  100. 100. 
    Kwiatkowska M, Norman G, Segala R, Sproston J. 2002. Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282:101–50
     [Google Scholar]
  101. 101. 
    Beauquier D. 2003. Probabilistic timed automata. Theor. Comput. Sci. 292:65–84
     [Google Scholar]
  102. 102. 
    Kwiatkowska M, Norman G, Parker D, Sproston J 2006. Performance analysis of probabilistic timed automata using digital clocks. Form. Methods Syst. Des. 29:33–78
     [Google Scholar]
  103. 103. 
    Kwiatkowska M, Norman G, Parker D 2019. Verification and control of turn-based probabilistic real-time games. The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy M Alvim, K Chatzikokolakis, C Olarte, F Valencia 379–96 Cham, Switz: Springer
     [Google Scholar]
  104. 104. 
    Forejt V, Kwiatkowska M, Norman G, Trivedi A. 2016. Expected reachability-time games. Theor. Comput. Sci. 631:139–60
     [Google Scholar]
  105. 105. 
    Jurdziński M, Kwiatkowska M, Norman G, Trivedi A 2009. Concavely-priced probabilistic timed automata. CONCUR 2009 – Concurrency Theory: 20th International Conference M Bravetti, G Zavattaro 415–30 Berlin: Springer
     [Google Scholar]
  106. 106. 
    Kwiatkowska M, Norman G, Sproston J, Wang F 2007. Symbolic model checking for probabilistic timed automata. Inf. Comput. 205:1027–77
     [Google Scholar]
  107. 107. 
    Jovanovic A, Kwiatkowska M, Norman G, Peyras Q 2017. Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata. Theor. Comput. Sci. 669:1–21
     [Google Scholar]
  108. 108. 
    Kwiatkowska M, Norman G, Parker D 2009. Stochastic games for verification of probabilistic timed automata. Formal Modeling and Analysis of Timed Systems: 7th International Conference, FORMATS 2009 J Ouaknine, FW Vaandrager 212–27 Berlin: Springer
     [Google Scholar]
  109. 109. 
    Tkachev I, Abate A. 2013. Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems. HSCC '13: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control283–92 New York: ACM
     [Google Scholar]
  110. 110. 
    Haesaert S, Soudjani S, Abate A 2018. Temporal logic control of general Markov decision processes by approximate policy refinement. IFAC-PapersOnLine 51:1673–78
     [Google Scholar]
  111. 111. 
    Clarke E, Grumberg O, Jha S, Lu Y, Veith H 2000. Counterexample-guided abstraction refinement. Computer Aided Verification: 12th International Conference, CAV 2000 EA Emerson, AP Sistla 154–69 Berlin: Springer
     [Google Scholar]
  112. 112. 
    D'Argenio P, Jeannet B, Jensen H, Larsen K 2001. Reachability analysis of probabilistic systems by successive refinements. Process Algebra and Probabilistic Methods: Performance Modeling and Verification; Joint International Workshop, PAPM-PROBMIV 2001 L de Alfaro, S Gilmore 39–56 Berlin: Springer
     [Google Scholar]
  113. 113. 
    D'Argenio P, Jeannet B, Jensen H, Larsen K 2002. Reduction and refinement strategies for probabilistic analysis. Process Algebra and Probabilistic Methods: Performance Modeling and Verification; Second Joint International Workshop, PAPM-PROBMIV 2002 H Hermanns, R Segala 57–76 Berlin: Springer
     [Google Scholar]
  114. 114. 
    Segala R, Lynch N. 1995. Probabilistic simulations for probabilistic processes. Nordic J. Comput. 2:250–73
     [Google Scholar]
  115. 115. 
    Wachter B, Zhang L, Hermanns H. 2007. Probabilistic model checking modulo theories. Fourth International Conference on the Quantitative Evaluation of Systems129–40 Piscataway, NJ: IEEE
     [Google Scholar]
  116. 116. 
    Hermanns H, Wachter B, Zhang L 2008. Probabilistic CEGAR. Computer Aided Verification: 20th International Conference, CAV 2008 A Gupta, S Malik 162–75 Berlin: Springer
     [Google Scholar]
  117. 117. 
    Graf S, Saidi H 1997. Construction of abstract state graphs with PVS. Computer Aided Verification: 9th International Conference, CAV'97 O Grumberg 72–83 Berlin: Springer
     [Google Scholar]
  118. 118. 
    Han T, Katoen JP, Damman B. 2009. Counterexample generation in probabilistic model checking. IEEE Trans. Softw. Eng. 35:241–57
     [Google Scholar]
  119. 119. 
    Hahn E, Hermanns H, Wachter B, Zhang L 2010. PASS: abstraction refinement for infinite probabilistic models. Tools and Algorithms for the Construction and Analysis of Systems: 16th International Conference, TACAS 2010 ed. J Esparza, R Majumdar 353–57 Berlin: Springer
     [Google Scholar]
  120. 120. 
    Kattenbelt M, Kwiatkowska M, Norman G, Parker D 2010. A game-based abstraction-refinement framework for Markov decision processes. Form. Methods Syst. Des. 36:246–80
     [Google Scholar]
  121. 121. 
    Kwiatkowska M, Norman G, Parker D, Qu H. 2013. Compositional probabilistic verification through multi-objective model checking. Inf. Comput. 232:38–65
     [Google Scholar]
  122. 122. 
    Basset N, Kwiatkowska M, Wiltsche C 2014. Compositional controller synthesis for stochastic games. CONCUR 2014 – Concurrency Theory: 25th International Conference P Baldan, D Gorla 173–87 Berlin: Springer
     [Google Scholar]
  123. 123. 
    Chatterjee K, Doyen L. 2014. Partial-observation stochastic games: how to win when belief fails. ACM Trans. Comput. Log. 15:16
     [Google Scholar]
  124. 124. 
    Simaan M, May J. 1973. On the Stackelberg strategy in nonzero-sum games. J. Optim. Theory Appl. 11:533–55
     [Google Scholar]
  125. 125. 
    Aumann R. 1974. Subjectivity and correlation in randomized strategies. J. Math. Econ. 1:67–96
     [Google Scholar]
  126. 126. 
    Battigalli P, Dufwenberg M. 2009. Dynamic psychological games. J. Econ. Theory 244:67–96
     [Google Scholar]
  127. 127. 
    Kaelbling L, Littman M, Moore A 1996. Reinforcement learning: a survey. J. Artif. Intell. Res. 4:237–85
     [Google Scholar]
  128. 128. 
    d'Avila Garcez A, Lamb L, Gabbay D 2009. Neural-Symbolic Cognitive Reasoning Berlin: Springer
/content/journals/10.1146/annurev-control-042820-010947
Loading
Probabilistic Model Checking and Autonomy
Annual Review of Control, Robotics, and Autonomous Systems 5, 385 (2022); https://doi.org/10.1146/annurev-control-042820-010947
/content/journals/10.1146/annurev-control-042820-010947
/content/journals/10.1146/annurev-control-042820-010947
Loading

Data & Media loading...

  • Article Type: Review Article

Most Cited Most Cited RSS feed

This is a required field
Please enter a valid email address
Approval was a Success
Invalid data
An Error Occurred
Approval was partially successful, following selected items could not be processed due to error