The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games

Authors Thomas Brihaye, Véronique Bruyère, Aline Goeminne, Jean-François Raskin, Marie van den Bogaard



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.13.pdf
  • Filesize: 0.54 MB
  • 16 pages

Document Identifiers

Author Details

Thomas Brihaye
  • Université de Mons (UMONS), Belgium
Véronique Bruyère
  • Université de Mons (UMONS), Belgium
Aline Goeminne
  • Université de Mons (UMONS), Belgium
  • Université libre de Bruxelles (ULB), Belgium
Jean-François Raskin
  • Université libre de Bruxelles (ULB), Belgium
Marie van den Bogaard
  • Université libre de Bruxelles (ULB), Belgium

Cite AsGet BibTex

Thomas Brihaye, Véronique Bruyère, Aline Goeminne, Jean-François Raskin, and Marie van den Bogaard. The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CONCUR.2019.13

Abstract

We study multiplayer quantitative reachability games played on a finite directed graph, where the objective of each player is to reach his target set of vertices as quickly as possible. Instead of the well-known notion of Nash equilibrium (NE), we focus on the notion of subgame perfect equilibrium (SPE), a refinement of NE well-suited in the framework of games played on graphs. It is known that there always exists an SPE in quantitative reachability games and that the constrained existence problem is decidable. We here prove that this problem is PSPACE-complete. To obtain this result, we propose a new algorithm that iteratively builds a set of constraints characterizing the set of SPE outcomes in quantitative reachability games. This set of constraints is obtained by iterating an operator that reinforces the constraints up to obtaining a fixpoint. With this fixpoint, the set of SPE outcomes can be represented by a finite graph of size at most exponential. A careful inspection of the computation allows us to establish PSPACE membership.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal methods
  • Theory of computation → Logic and verification
  • Theory of computation → Solution concepts in game theory
Keywords
  • multiplayer non-zero-sum games played on graphs
  • quantitative reachability objectives
  • subgame perfect equilibria
  • constrained existence problem

Metrics

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

References

  1. Nicolas Basset, Ismaël Jecker, Arno Pauly, Jean-François Raskin, and Marie van den Bogaard. Beyond Admissibility: Dominance Between Chains of Strategies. In CSL, volume 119 of LIPIcs, pages 10:1-10:22. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. Google Scholar
  2. Dietmar Berwanger. Admissibility in Infinite Games. In STACS, volume 4393 of LNCS, pages 188-199. Springer, 2007. Google Scholar
  3. Romain Brenguier, Lorenzo Clemente, Paul Hunter, Guillermo A. Pérez, Mickael Randour, Jean-François Raskin, Ocan Sankur, and Mathieu Sassolas. Non-Zero Sum Games for Reactive Synthesis. In LATA, volume 9618 of LNCS, pages 3-23. Springer, 2016. Google Scholar
  4. Romain Brenguier, Arno Pauly, Jean-François Raskin, and Ocan Sankur. Admissibility in Games with Imperfect Information (Invited Talk). In CONCUR, volume 85 of LIPIcs, pages 2:1-2:23. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017. Google Scholar
  5. Romain Brenguier, Guillermo A. Pérez, Jean-Francois Raskin, and Ocan Sankur. Admissibility in Quantitative Graph Games. In FSTTCS, volume 65 of LIPIcs, pages 42:1-42:14, 2016. Google Scholar
  6. Romain Brenguier, Jean-François Raskin, and Ocan Sankur. Assume-admissible synthesis. In CONCUR, LIPIcs 42, pages 100-113. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  7. Romain Brenguier, Jean-François Raskin, and Mathieu Sassolas. The complexity of admissibility in Omega-regular games. In CSL-LICS, pages 23:1-23:10. ACM, 2014. Google Scholar
  8. Thomas Brihaye, Véronique Bruyère, Julie De Pril, and Hugo Gimbert. On Subgame Perfection in Quantitative Reachability Games. Logical Methods in Computer Science, 9(1), 2012. Google Scholar
  9. Thomas Brihaye, Véronique Bruyère, Aline Goeminne, and Jean-François Raskin. Constrained Existence Problem for Weak Subgame Perfect Equilibria with ω-Regular Boolean Objectives. In GandALF, pages 16-29, 2018. Google Scholar
  10. Thomas Brihaye, Véronique Bruyère, Aline Goeminne, and Jean-François Raskin. Constrained existence problem for weak subgame perfect equilibria with omega-regular Boolean objectives. CoRR, abs/1806.05544, 2018. Google Scholar
  11. Thomas Brihaye, Véronique Bruyère, Noémie Meunier, and Jean-François Raskin. Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability. In CSL, volume 41 of LIPIcs, pages 504-518. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  12. Thomas Brihaye, Julie De Pril, and Sven Schewe. Multiplayer Cost Games with Simple Nash Equilibria. In LFCS, volume 7734 of Lecture Notes in Computer Science, pages 59-73. Springer, 2013. Google Scholar
  13. Véronique Bruyère. Computer Aided Synthesis: A Game-Theoretic Approach. In DLT, volume 10396 of LNCS, pages 3-35. Springer, 2017. Google Scholar
  14. Véronique Bruyère, Stéphane Le Roux, Arno Pauly, and Jean-François Raskin. On the Existence of Weak Subgame Perfect Equilibria. In FOSSACS, volume 10203 of LNCS, pages 145-161, 2017. Google Scholar
  15. K. Chatterjee, T. A. Henzinger, and M. Jurdzinski. Games with secure equilibria. Theoretical Computer Science, 365:67-82, 2006. Google Scholar
  16. Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Strategy logic. Inf. Comput., 208(6):677-693, 2010. Google Scholar
  17. Rodica Condurache, Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin. The Complexity of Rational Synthesis. In ICALP, volume 55 of LIPIcs, pages 121:1-121:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. Google Scholar
  18. Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin. Rational Synthesis Under Imperfect Information. In LICS, pages 422-431. ACM, 2018. Google Scholar
  19. Dana Fisman, Orna Kupferman, and Yoad Lustig. Rational Synthesis. In TACAS, volume 6015 of LNCS, pages 190-204. Springer, 2010. Google Scholar
  20. János Flesch, Jeroen Kuipers, Ayala Mashiah-Yaakovi, Gijs Schoenmakers, Eilon Solan, and Koos Vrieze. Perfect-Information Games with Lower-Semicontinuous Payoffs. Mathematics of Operation Research, 35:742-755, 2010. Google Scholar
  21. Erich Grädel and Michael Ummels. Solution Concepts and Algorithms for Infinite Multiplayer Games. In New Perspectives on Games and Interaction, volume 4, pages 151-178. Amsterdam University Press, 2008. Google Scholar
  22. Orna Kupferman, Giuseppe Perelli, and Moshe Y. Vardi. Synthesis with Rational Environments. In EUMAS, LNCS 8953, pages 219-235. Springer, 2014. Google Scholar
  23. Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi. Reasoning About Strategies. In FSTTCS 2010, volume 8 of LIPIcs, pages 133-144. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2010. Google Scholar
  24. J. F. Nash. Equilibrium points in n-person games. In PNAS, volume 36, pages 48-49. National Academy of Sciences, 1950. Google Scholar
  25. Martin J. Osborne. An introduction to game theory. Oxford Univ. Press, 2004. Google Scholar
  26. A. Pnueli and R. Rosner. On the Synthesis of a Reactive Module. In POPL, pages 179-190. ACM Press, 1989. Google Scholar
  27. Michael Ummels. Rational Behaviour and Strategy Construction in Infinite Multiplayer Games. In FSTTCS, volume 4337 of LNCS, pages 212-223. Springer, 2006. Google Scholar
  28. Michael Ummels. The Complexity of Nash Equilibria in Infinite Multiplayer Games. In FOSSACS, volume 4962 of LNCS, pages 20-34. Springer, 2008. Google Scholar
  29. Michael Ummels and Dominik Wojtczak. The Complexity of Nash Equilibria in Limit-Average Games. In CONCUR, volume 6901 of LNCS, pages 482-496. Springer, 2011. Google Scholar
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