Document Open Access Logo

Probabilistic Model Checking for Strategic Equilibria-Based Decision Making: Advances and Challenges (Invited Talk)

Authors Marta Kwiatkowska , Gethin Norman , David Parker , Gabriel Santos , Rui Yan

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2022.4.pdf
  • Filesize: 0.92 MB
  • 22 pages

Document Identifiers

Author Details

Marta Kwiatkowska
  • University of Oxford, Oxford, UK
Gethin Norman
  • University of Glasgow, Glasgow, UK
  • University of Oxford, Oxford, UK
David Parker
  • University of Birmingham, Birmingham, UK
Gabriel Santos
  • University of Oxford, Oxford, UK
Rui Yan
  • University of Oxford, Oxford, UK

Funding

This project was funded by the ERC under the European Union’s Horizon 2020 research and innovation programme (http://www.fun2model.org, grant agreement No. 834115).

Cite AsGet BibTex

Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos, and Rui Yan. Probabilistic Model Checking for Strategic Equilibria-Based Decision Making: Advances and Challenges (Invited Talk). In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.MFCS.2022.4

Abstract

Game-theoretic concepts have been extensively studied in economics to provide insight into competitive behaviour and strategic decision making. As computing systems increasingly involve concurrently acting autonomous agents, game-theoretic approaches are becoming widespread in computer science as a faithful modelling abstraction. These techniques can be used to reason about the competitive or collaborative behaviour of multiple rational agents with distinct goals or objectives. This paper provides an overview of recent advances in developing a modelling, verification and strategy synthesis framework for concurrent stochastic games implemented in the probabilistic model checker PRISM-games. This is based on a temporal logic that supports finite- and infinite-horizon temporal properties in both a zero-sum and nonzero-sum setting, the latter using Nash and correlated equilibria with respect to two optimality criteria, social welfare and social fairness. We summarise the key concepts, logics and algorithms and the currently available tool support. Future challenges and recent progress in adapting the framework and algorithmic solutions to continuous environments and neural networks are also outlined.

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • Probabilistic model checking
  • stochastic games
  • equilibria

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. M. Akintunde, E. Botoeva, P. Kouvaros, and A. Lomuscio. Formal verification of neural agents in non-deterministic environments. In Proc. AAMAS'20, pages 25-33. Springer, 2020. Google Scholar
  2. M. Akintunde, E. Botoeva, P. Kouvaros, and A. Lomuscio. Verifying Strategic Abilities of Neural-symbolic Multi-agent Systems. In Proc. KR'20, pages 22-32. IJCAI Organization, September 2020. Google Scholar
  3. R. Alur and T. Henzinger. Reactive modules. Formal Methods in System Design, 15(1):7-48, 1999. Google Scholar
  4. R. Alur, T. Henzinger, and O. Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):672-713, 2002. Google Scholar
  5. R. Alur, T. Henzinger, F. Mang, S. Qadeer, S. Rajamani, and S. Tasiran. MOCHA: Modularity in model checking. In Proc. 10th Int. Conf. Computer Aided Verification (CAV'98), volume 1427 of LNCS, pages 521-525, Vancouver, 1998. Springer. Google Scholar
  6. R. Aumann. Subjectivity and correlation in randomized strategies. Journal of Mathematical Economics, 1(1):67-96, 1974. Google Scholar
  7. P. Bouyer, N. Markey, and D. Stan. Mixed Nash equilibria in concurrent games. In Proc. FSTTCS'14, volume 29 of LIPICS, pages 351-363, 2014. Google Scholar
  8. R. Brenguier. PRALINE: A tool for computing Nash equilibria in concurrent games. In Proc. CAV'13, volume 8044 of LNCS, pages 890-895. Springer, 2013. URL: http://www.lsv.fr/Software/praline/.
  9. T. Brihaye, V. Bruyère, A. Goeminne, J.-F. Raskin, and M. van den Bogaard. The complexity of subgame perfect equilibria in quantitative reachability games. In Proc. CONCUR'19, volume 140 of LIPIcs, pages 13:1-13:16. Leibniz-Zentrum für Informatik, 2019. Google Scholar
  10. P. Čermák, A. Lomuscio, F. Mogavero, and A. Murano. MCMAS-SLK: A model checker for the verification of strategy logic specifications. In Proc. CAV'14, volume 8559 of LNCS, pages 525-532. Springer, 2014. Google Scholar
  11. K. Chatterjee, L. de Alfaro, and T. Henzinger. Strategy improvement for concurrent reachability and turn-based stochastic safety games. Journal of Computer and System Sciences, 79(5):640-657, 2013. Google Scholar
  12. K. Chatterjee and T. Henzinger. Value iteration. In 25 Years of Model Checking, volume 5000 of LNCS, pages 107-138. Springer, 2008. Google Scholar
  13. K. Chatterjee, T. Henzinger, B. Jobstmann, and A. Radhakrishna. Gist: A solver for probabilistic games. In Proc. CAV'10, volume 6174 of LNCS, pages 665-669. Springer, 2010. URL: http://pub.ist.ac.at/gist/.
  14. K. Chatterjee, R. Majumdar, and M. Jurdziński. On Nash equilibria in stochastic games. In Proc. CSL'04, volume 3210 of LNCS, pages 26-40. Springer, 2004. Google Scholar
  15. T. Chen, V. Forejt, M. Kwiatkowska, D. Parker, and A. Simaitis. Automatic verification of competitive stochastic systems. Formal Methods in System Design, 43(1):61-92, 2013. Google Scholar
  16. C. Cheng, A. Knoll, M. Luttenberger, and C. Buckl. GAVS+: An open platform for the research of algorithmic game solving. In Proc. TACAS'11, volume 6605 of LNCS, pages 258-261. Springer, 2011. URL: https://sourceforge.net/projects/gavsplus/.
  17. L. de Alfaro, T. Henzinger, and O. Kupferman. Concurrent reachability games. Theoretical Computer Science, 386(3):188-217, 2007. Google Scholar
  18. L. de Alfaro and R. Majumdar. Quantitative solution of omega-regular games. Journal of Computer and System Sciences, 68(2):374-397, 2004. Google Scholar
  19. L. De Moura and N. Bjørner. Z3: An efficient SMT solver. In Proc. TACAS'08, volume 4963 of LNCS, pages 337-340. Springer, 2008. URL: https://github.com/Z3Prover/z3.
  20. B. Dutertre. Yices 2.2. In Proc. CAV'14, volume 8559 of LNCS, pages 737-744. Springer, 2014. URL: http://yices.csl.sri.com.
  21. V. Forejt, M. Kwiatkowska, G. Norman, and D. Parker. Automated verification techniques for probabilistic systems. In SFM'11, volume 6659 of LNCS, pages 53-113. Springer, 2011. Google Scholar
  22. Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual, 2021. URL: https://www.gurobi.com.
  23. J. Gutierrez, M. Najib, P. Giuseppe, and M. Wooldridge. Equilibrium design for concurrent games. In Proc. CONCUR'19, volume 140 of LIPIcs, pages 22:1-22:16. Leibniz-Zentrum für Informatik, 2019. Google Scholar
  24. J. Gutierrez, M. Najib, G. Perelli, and M. Wooldridge. EVE: A tool for temporal equilibrium analysis. In Proc. ATVA'18, volume 11138 of LNCS, pages 551-557. Springer, 2018. URL: https://github.com/eve-mas/eve-parity.
  25. Julian Gutierrez, Lewis Hammond, Anthony W. Lin, Muhammad Najib, and Michael J. Wooldridge. Rational verification for probabilistic systems. In Proc. 18th International Conference on Principles of Knowledge Representation and Reasoning (KR'21), pages 312-322, 2021. Google Scholar
  26. H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. FAC, 6(5):512-535, 1994. Google Scholar
  27. L. Hurwicz and S. Reiter. Designing Economic Mechanisms. Cambridge University Press, 2006. Google Scholar
  28. K. Julian and M. Kochenderfer. A reachability method for verifying dynamical systems with deep neural network controllers. CoRR, abs/1903.00520, 2019. URL: http://arxiv.org/abs/1903.00520.
  29. K. Julian, S. Sharma, J.-B. Jeannin, and M. Kochenderfer. Verifying aircraft collision avoidance neural networks through linear approximations of safe regions. CoRR, abs/1903.00762, 2019. URL: http://arxiv.org/abs/1903.00762.
  30. N. Karmarkar. A new polynomial-time algorithm for linear programming. Combinatorica, 4(4):373-395, 1984. Google Scholar
  31. J. Kemeny, J. Snell, and A. Knapp. Denumerable Markov Chains. Springer, 1976. Google Scholar
  32. M. Kwiatkowska, G. Norman, D. Parker, and G. Santos. Multi-player equilibria verification for concurrent stochastic games. In Proc. QEST'20, volume 12289 of LNCS, pages 74-95. Springer, 2020. Google Scholar
  33. M. Kwiatkowska, G. Norman, D. Parker, and G. Santos. PRISM-games 3.0: Stochastic game verification with concurrency, equilibria and time. In Proc. CAV'20, volume 12225 of LNCS, pages 475-487. Springer, 2020. Google Scholar
  34. M. Kwiatkowska, G. Norman, D. Parker, and G. Santos. Automatic verification of concurrent stochastic systems. Formal Methods in System Design, pages 1-63, 2021. Google Scholar
  35. M. Kwiatkowska, G. Norman, D. Parker, and G. Santos. Correlated equilibria and fairness in concurrent stochastic games. In Proc. TACAS'22, volume 13244 of LNCS, pages 60-78. Springer, 2022. Google Scholar
  36. S. LaValle. Robot motion planning: A game-theoretic foundation. Algorithmica, 26:430-465, 2000. Google Scholar
  37. C. Lemke and Jr J. Howson. Equilibrium points of bimatrix games. Journal of the Society for Industrial and Applied Mathematics, 12(2):413-423, 1964. Google Scholar
  38. M. Littman, N. Ravi, A. Talwar, and M. Zinkevich. An efficient optimal-equilibrium algorithm for two-player game trees. In Proc. UAI'06, pages 298-305. AUAI Press, 2006. Google Scholar
  39. A. Lomuscio, H. Qu, and F. Raimondi. MCMAS: A model checker for the verification of multi-agent systems. In Proc. 21st Int. Conf. Computer Aided Verification (CAV'09), volume 5643 of LNCS, pages 682-688. Springer, 2009. Google Scholar
  40. D. Lozovanu and S. Pickl. Determining Nash equilibria for stochastic positional games with discounted payoffs. In Proc. ADT'17, volume 10576 of LNAI, pages 339-343. Springer, 2017. Google Scholar
  41. LPSolve (version 5.5). URL: http://lpsolve.sourceforge.net/5.5/.
  42. O. Madani, S. Hanks, and A. Condon. On the undecidability of probabilistic planning and related stochastic optimization problems. Artificial Intelligence, 147(1-2):5-34, 2003. Google Scholar
  43. J. Marden and J. Shamma. Game theory and control. Annual Review of Control, Robotics, and Autonomous Systems, 1(1):105-134, 2018. Google Scholar
  44. D. Martin. The determinacy of Blackwell games. J. Symbolic Logic, 63(4):1565-1581, 1998. Google Scholar
  45. R. McKelvey, A. McLennan, and T. Turocy. Gambit: Software tools for game theory. URL: http://www.gambit-project.org.
  46. N. Nisan, T. Roughgarden, E. Tardos, and V. Vazirani. Algorithmic Game Theory. Cambridge University Press, 2007. Google Scholar
  47. M. Osborne and A. Rubinstein. An Introduction to Game Theory. Oxford University Press, 2004. Google Scholar
  48. R. Porter, E. Nudelman, and Y. Shoham. Simple search methods for finding a Nash equilibrium. In Proc. AAAI'04, pages 664-669. AAAI Press, 2004. Google Scholar
  49. H. Prasad, L. Prashanth, and S. Bhatnagar. Two-timescale algorithms for learning Nash equilibria in general-sum stochastic games. In Proc. AAMAS'15, pages 1371-1379. IFAAMAS, 2015. Google Scholar
  50. E. Prisner. Game Theory Through Examples. Mathematical Association of America, 1 edition, 2014. Google Scholar
  51. T. Raghavan and J. Filar. Algorithms for stochastic games - A survey. Zeitschrift für Operations Research, 35(6):437-472, November 1991. Google Scholar
  52. T. Sandholm, A. Gilpin, and V. Conitzer. Mixed-integer programming methods for finding Nash equilibria. In Proc. AAAI'05, pages 495-501. AAAI Press, 2005. Google Scholar
  53. U. Schwalbe and P. Walker. Zermelo and the early history of game theory. Games and Economic Behavior, 34(1):123-137, 2001. Google Scholar
  54. L. Shapley. Stochastic games. PNAS, 39:1095-1100, 1953. Google Scholar
  55. A. Toumi, J. Gutierrez, and M. Wooldridge. A tool for the automated verification of Nash equilibria in concurrent games. In Proc. ICTAC'15, volume 9399 of LNCS, pages 583-594. Springer, 2015. Google Scholar
  56. J. von Neumann. Zur Theorie der Gesellschaftsspiele. Mathematische Annalen, 100:295-320, 1928. Google Scholar
  57. J. von Neumann, O. Morgenstern, H. Kuhn, and A. Rubinstein. Theory of Games and Economic Behavior. Princeton University Press, 1944. Google Scholar
  58. A. Wächter. Short tutorial: Getting started with ipopt in 90 minutes. In Combinatorial Scientific Computing, number 09061 in Dagstuhl Seminar Proceedings. Leibniz-Zentrum für Informatik, 2009. URL: https://github.com/coin-or/Ipopt.
  59. R. Yan, G. Santos, X. Duan, D. Parker, and M. Kwiatkowska. Finite-horizon equilibria for neuro-symbolic concurrent stochastic games. In Proc. UAI'22, 2022. Google Scholar
  60. R. Yan, G. Santos, G. Norman, D. Parker, and M. Kwiatkowska. Strategy synthesis for zero-sum neuro-symbolic concurrent stochastic games, 2022. URL: http://arxiv.org/abs/2202.06255.
  61. PRISM-games web site. URL: http://www.prismmodelchecker.org/games/.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact