Document Open Access Logo

On the Complexity of SPEs in Parity Games

Authors Léonard Brice, Jean-François Raskin, Marie van den Bogaard

PDF
Thumbnail PDF

File

LIPIcs.CSL.2022.10.pdf
  • Filesize: 0.78 MB
  • 17 pages

Document Identifiers

Author Details

Léonard Brice
  • Université Gustave Eiffel, Marne-la-Vallée, France
  • Université Libre de Bruxelles, Belgium
Jean-François Raskin
  • Université Libre de Bruxelles, Belgium
Marie van den Bogaard
  • LIGM, Univ. Gustave Eiffel, CNRS, F-77454 Marne-la-Vallée, France

Funding

This work is partially supported by the ARC project Non-Zero Sum Game Graphs: Applications to Reactive Synthesis and Beyond (Fédération Wallonie-Bruxelles), the EOS project Verifying Learning Artificial Intelligence Systems (F.R.S.-FNRS & FWO), the COST Action 16228 GAMENET (European Cooperation in Science and Technology), and by the PDR project Subgame perfection in graph games (F.R.S.- FNRS).

Acknowledgements

We wish to thank anonymous reviewers for their useful observations.

Cite AsGet BibTex

Léonard Brice, Jean-François Raskin, and Marie van den Bogaard. On the Complexity of SPEs in Parity Games. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CSL.2022.10

Abstract

We study the complexity of problems related to subgame-perfect equilibria (SPEs) in infinite duration non zero-sum multiplayer games played on finite graphs with parity objectives. We present new complexity results that close gaps in the literature. Our techniques are based on a recent characterization of SPEs in prefix-independent games that is grounded on the notions of requirements and negotiation, and according to which the plays supported by SPEs are exactly the plays consistent with the requirement that is the least fixed point of the negotiation function. The new results are as follows. First, checking that a given requirement is a fixed point of the negotiation function is an NP-complete problem. Second, we show that the SPE constrained existence problem is NP-complete, this problem was previously known to be ExpTime-easy and NP-hard. Third, the SPE constrained existence problem is fixed-parameter tractable when the number of players and of colors are parameters. Fourth, deciding whether some requirement is the least fixed point of the negotiation function is complete for the second level of the Boolean hierarchy. Finally, the SPE-verification problem - that is, the problem of deciding whether there exists a play supported by a SPE that satisfies some LTL formula - is PSpace-complete, this problem was known to be ExpTime-easy and PSpace-hard.

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
  • Games on graphs
  • subgame-perfect equilibria
  • parity objectives

Metrics

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

Related Versions

References

  1. 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 Language and Automata Theory and Applications - 10th International Conference, LATA 2016, Prague, Czech Republic, March 14-18, 2016, Proceedings, volume 9618 of Lecture Notes in Computer Science, pages 3-23. Springer, 2016. Google Scholar
  2. Léonard Brice, Jean-François Raskin, and Marie van den Bogaard. Subgame-perfect equilibria in mean-payoff games. CoRR, abs/2101.10685, 2021. URL: http://arxiv.org/abs/2101.10685.
  3. Léonard Brice, Marie van den Bogaard, and Jean-François Raskin. On the complexity of spes in parity games. CoRR, abs/2107.07458, 2021. URL: http://arxiv.org/abs/2107.07458.
  4. 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 CONCUR, volume 140 of LIPIcs, pages 13:1-13:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  5. Thomas Brihaye, Julie De Pril, and Sven Schewe. Multiplayer cost games with simple nash equilibria. In Logical Foundations of Computer Science, International Symposium, LFCS 2013, San Diego, CA, USA, January 6-8, 2013. Proceedings, volume 7734 of Lecture Notes in Computer Science, pages 59-73. Springer, 2013. Google Scholar
  6. Véronique Bruyère. Computer aided synthesis: A game-theoretic approach. In Developments in Language Theory - 21st International Conference, DLT 2017, Liège, Belgium, August 7-11, 2017, Proceedings, volume 10396 of Lecture Notes in Computer Science, pages 3-35. Springer, 2017. Google Scholar
  7. Véronique Bruyère, Quentin Hautem, and Jean-François Raskin. Parameterized complexity of games with monotonically ordered omega-regular objectives. In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, volume 118 of LIPIcs, pages 29:1-29:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.29.
  8. János Flesch and Arkadi Predtetchinski. A characterization of subgame-perfect equilibrium plays in borel games of perfect information. Math. Oper. Res., 42(4):1162-1179, 2017. URL: https://doi.org/10.1287/moor.2016.0843.
  9. Erich Grädel and Michael Ummels. Solution Concepts and Algorithms for Infinite Multiplayer Games. In Krzysztof Apt and Robert van Rooij, editors, New Perspectives on Games and Interaction, volume 4 of Texts in Logic and Games, pages 151-178. Amsterdam University Press, 2008. URL: http://www.logic.rwth-aachen.de/~ummels/knaw07.pdf.
  10. Ralf Küsters. Memoryless determinacy of parity games. In Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors, Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], volume 2500 of Lecture Notes in Computer Science, pages 95-106. Springer, 2001. URL: https://doi.org/10.1007/3-540-36387-4_6.
  11. Noémie Meunier. Multi-Player Quantitative Games: Equilibria and Algorithms. PhD thesis, Université de Mons, 2016. Google Scholar
  12. Christos H. Papadimitriou. Computational complexity. Academic Internet Publ., 2007. Google Scholar
  13. Philippe Schnoebelen. The complexity of temporal logic model checking. In Philippe Balbiani, Nobu-Yuki Suzuki, Frank Wolter, and Michael Zakharyaschev, editors, Advances in Modal Logic 4, papers from the fourth conference on "Advances in Modal logic," held in Toulouse, France, 30 September - 2 October 2002, pages 393-436. King’s College Publications, 2002. Google Scholar
  14. Michael Ummels. Rational behaviour and strategy construction in infinite multiplayer games. In S. Arun-Kumar and Naveen Garg, editors, FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, volume 4337 of Lecture Notes in Computer Science, pages 212-223. Springer, 2006. URL: https://doi.org/10.1007/11944836_21.
  15. Gerd Wechsung. On the boolean closure of NP. In Lothar Budach, editor, Fundamentals of Computation Theory, FCT '85, Cottbus, GDR, September 9-13, 1985, volume 199 of Lecture Notes in Computer Science, pages 485-493. Springer, 1985. URL: https://doi.org/10.1007/BFb0028832.
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