Document Open Access Logo

Rational Verification for Nash and Subgame-Perfect Equilibria in Graph Games

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2023.26.pdf
  • Filesize: 0.63 MB
  • 15 pages

Document Identifiers

Related Versions

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
  • Nash equilibria
  • subgame-perfect equilibria

Metrics

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

Abstract

We study a natural problem about rational behaviors in multiplayer non-zero-sum sequential infinite duration games played on graphs: rational verification, that consists in deciding whether all the rational answers to a given strategy satisfy some specification. We give the complexities of that problem for two major concepts of rationality: Nash equilibria and subgame-perfect equilibria, and for three major classes of payoff functions: energy, discounted-sum, and mean-payoff.

Cite As Get BibTex

Léonard Brice, Jean-François Raskin, and Marie van den Bogaard. Rational Verification for Nash and Subgame-Perfect Equilibria in Graph Games. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 26:1-26:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.MFCS.2023.26

Author Details

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

References

  1. Udi Boker, Thomas A. Henzinger, and Jan Otop. The target discounted-sum problem. In 30th Annual ACM/IEEE Symp. on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 750-761. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.74.
  2. Patricia Bouyer, Ulrich Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, and Jirí Srba. Infinite runs in weighted timed automata with energy constraints. In Franck Cassez and Claude Jard, editors, Formal Modeling and Analysis of Timed Systems, 6th Int. Conf., FORMATS 2008, Saint Malo, France, September 15-17, 2008. Proc., volume 5215 of Lecture Notes in Computer Science, pages 33-47. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85778-5_4.
  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 Language and Automata Theory and Applications - 10th Int. Conf., LATA 2016, Prague, Czech Republic, March 14-18, 2016, Proc., volume 9618 of Lecture Notes in Computer Science, pages 3-23. Springer, 2016. Google Scholar
  4. Léonard Brice, Jean-François Raskin, and Marie van den Bogaard. Subgame-perfect equilibria in mean-payoff games. In Serge Haddad and Daniele Varacca, editors, 32nd Int. Conf. on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 of LIPIcs, pages 8:1-8:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2021.8.
  5. Léonard Brice, Jean-François Raskin, and Marie van den Bogaard. The complexity of SPEs in mean-payoff games. In Mikolaj Bojanczyk, Emanuela Merelli, and David P. Woodruff, editors, 49th Int. Colloquium on Automata, Languages, and Programming, ICALP 2022, July 4-8, 2022, Paris, France, volume 229 of LIPIcs, pages 116:1-116:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.ICALP.2022.116.
  6. Léonard Brice, Jean-François Raskin, and Marie van den Bogaard. On the complexity of SPEs in parity games. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conf.on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), volume 216 of LIPIcs, pages 10:1-10:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.10.
  7. Léonard Brice, Jean-François Raskin, and Marie van den Bogaard. Rational verification and checking for nash and subgame-perfect equilibria in graph games. CoRR, abs/2301.12913, 2023. URL: https://doi.org/10.48550/arXiv.2301.12913.
  8. 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 Wan J. Fokkink and Rob van Glabbeek, editors, 30th Int. Conf. on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands, volume 140 of LIPIcs, pages 13:1-13:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.13.
  9. Véronique Bruyère. Computer aided synthesis: A game-theoretic approach. In Developments in Language Theory - 21st Int. Conf., DLT 2017, Liège, Belgium, August 7-11, 2017, Proc., volume 10396 of Lecture Notes in Computer Science, pages 3-35. Springer, 2017. Google Scholar
  10. Véronique Bruyère. Synthesis of equilibria in infinite-duration games on graphs. ACM SIGLOG News, 8(2):4-29, 2021. URL: https://doi.org/10.1145/3467001.3467003.
  11. Véronique Bruyère, Jean-François Raskin, and Clément Tamines. Pareto-rational verification. In Bartek Klin, Slawomir Lasota, and Anca Muscholl, editors, 33rd Int. Conf. on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland, volume 243 of LIPIcs, pages 33:1-33:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.33.
  12. Krishnendu Chatterjee and Vishwanath Raman. Synthesizing protocols for digital contract signing. In Viktor Kuncak and Andrey Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation - 13th Int. Conf., VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012. Proc., volume 7148 of Lecture Notes in Computer Science, pages 152-168. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-27940-9_11.
  13. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors. Handbook of Model Checking. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8.
  14. Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors. The Adversarial Stackelberg Value in Quantitative Games, volume 168 of Leibniz Int. Proc. in Informatics (LIPIcs), Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.127.
  15. Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura. A metaprogramming framework for formal verification. Proc. ACM Program. Lang., 1(ICFP):34:1-34:29, 2017. URL: https://doi.org/10.1145/3110278.
  16. Dana Fisman, Orna Kupferman, and Yoad Lustig. Rational synthesis. In Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, 16th Int. Conf., TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proc., volume 6015 of Lecture Notes in Computer Science, pages 190-204. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12002-2_16.
  17. 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.
  18. Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, and Michael J. Wooldridge. Automated temporal equilibrium analysis: Verification and synthesis of multi-player games. Artif. Intell., 287:103353, 2020. URL: https://doi.org/10.1016/j.artint.2020.103353.
  19. Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, and Michael J. Wooldridge. On the complexity of rational verification. CoRR, abs/2207.02637, 2022. URL: https://doi.org/10.48550/arXiv.2207.02637.
  20. Steve Kremer and Jean-François Raskin. A game-based verification of non-repudiation and fair exchange protocols. In Kim Guldstrand Larsen and Mogens Nielsen, editors, CONCUR 2001 - Concurrency Theory, 12th Int. Conf., Aalborg, Denmark, August 20-25, 2001, Proc., volume 2154 of Lecture Notes in Computer Science, pages 551-565. Springer, 2001. URL: https://doi.org/10.1007/3-540-44685-0_37.
  21. Steve Kremer and Jean-François Raskin. A game-based verification of non-repudiation and fair exchange protocols. J. Comput. Secur., 11(3):399-430, 2003. URL: http://content.iospress.com/articles/journal-of-computer-security/jcs185, URL: https://doi.org/10.3233/jcs-2003-11307.
  22. Orna Kupferman, Giuseppe Perelli, and Moshe Y. Vardi. Synthesis with rational environments. Ann. Math. Artif. Intell., 78(1):3-20, 2016. URL: https://doi.org/10.1007/s10472-016-9508-8.
  23. Noémie Meunier. Multi-Player Quantitative Games: Equilibria and Algorithms. PhD thesis, Université de Mons, 2016. Google Scholar
  24. John 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. Dorsa Sadigh, Shankar Sastry, Sanjit A. Seshia, and Anca D. Dragan. Planning for autonomous cars that leverage effects on human actions. In David Hsu, Nancy M. Amato, Spring Berman, and Sam Ade Jacobs, editors, Robotics: Science and Systems XII, University of Michigan, Ann Arbor, Michigan, USA, June 18 - June 22, 2016, 2016. URL: https://doi.org/10.15607/RSS.2016.XII.029.
  27. Thomas Steeples, Julian Gutierrez, and Michael J. Wooldridge. Mean-payoff games with ω-regular specifications. In Frank Dignum, Alessio Lomuscio, Ulle Endriss, and Ann Nowé, editors, AAMAS '21: 20th Int. Conf. on Autonomous Agents and Multiagent Systems, Virtual Event, United Kingdom, May 3-7, 2021, pages 1272-1280. ACM, 2021. URL: https://doi.org/10.5555/3463952.3464099.
  28. Michael Ummels. Rational Behaviour and Strategy Construction in Infinite Multiplayer Games. Diploma thesis, RWTH Aachen, 2005. URL: http://www.logic.rwth-aachen.de/~ummels/diplom.pdf.
  29. Michael Ummels. The complexity of nash equilibria in infinite multiplayer games. In Roberto M. Amadio, editor, Foundations of Software Science and Computational Structures, 11th Int. Conf., FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proc., volume 4962 of Lecture Notes in Computer Science, pages 20-34. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78499-9_3.
  30. Yaron Velner, Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Alexander Moshe Rabinovich, and Jean-François Raskin. The complexity of multi-mean-payoff and multi-energy games. Inf. Comput., 241:177-196, 2015. Google Scholar
  31. Uri Zwick and Mike Paterson. The complexity of mean payoff games, volume 959, pages 1-10. Springer, April 2006. URL: https://doi.org/10.1007/BFb0030814.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact