Document Open Access Logo

As Soon as Possible but Rationally

Authors Véronique Bruyère , Christophe Grandmont , Jean-François Raskin

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2024.14.pdf
  • Filesize: 0.89 MB
  • 20 pages

Document Identifiers

Author Details

Véronique Bruyère
  • Université de Mons (UMONS), Belgium
Christophe Grandmont
  • Université de Mons (UMONS), Belgium
  • Université Libre de Bruxelles (ULB), Belgium
Jean-François Raskin
  • Université Libre de Bruxelles (ULB), Belgium

Funding

This work has been supported by the Fonds de la Recherche Scientifique – FNRS under Grant n° T.0023.22 (PDR Rational).
  • Raskin, Jean-François: Supported by Fondation ULB (https://www.fondationulb.be/en/)

Cite As Get BibTex

Véronique Bruyère, Christophe Grandmont, and Jean-François Raskin. As Soon as Possible but Rationally. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.CONCUR.2024.14

Abstract

This paper addresses complexity problems in rational verification and synthesis for multi-player games played on weighted graphs, where the objective of each player is to minimize the cost of reaching a specific set of target vertices. In these games, one player, referred to as the system, declares his strategy upfront. The other players, composing the environment, then rationally make their moves according to their objectives. The rational behavior of these responding players is captured through two models: they opt for strategies that either represent a Nash equilibrium or lead to a play with a Pareto-optimal cost tuple.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal methods
  • Theory of computation → Solution concepts in game theory
  • Theory of computation → Logic and verification
Keywords
  • Games played on graphs
  • rational verification
  • rational synthesis
  • Nash equilibrium
  • Pareto-optimality
  • quantitative reachability objectives

Metrics

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

Related Versions

References

  1. Shaull Almagor, Orna Kupferman, and Giuseppe Perelli. Synthesis of controllable nash equilibria in quantitative objective game. In Jérôme Lang, editor, Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden, pages 35-41. ijcai.org, 2018. URL: https://doi.org/10.24963/IJCAI.2018/5.
  2. Rajeev Alur, Aldric Degorre, Oded Maler, and Gera Weiss. On Omega-Languages Defined by Mean-Payoff Conditions. In Luca de Alfaro, editor, Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, volume 5504 of Lecture Notes in Computer Science, pages 333-347. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00596-1_24.
  3. Luis Barguñó, Carles Creus, Guillem Godoy, Florent Jacquemard, and Camille Vacher. The Emptiness Problem for Tree Automata with Global Constraints. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom, pages 263-272. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/LICS.2010.28.
  4. Romain Brenguier and Jean-François Raskin. Pareto Curves of Multidimensional Mean-Payoff Games. In Daniel Kroening and Corina S. Pasareanu, editors, Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, volume 9207 of Lecture Notes in Computer Science, pages 251-267. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21668-3_15.
  5. 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 International Conference 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.
  6. 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 International 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.
  7. Léonard Brice, Jean-François Raskin, and Marie van den Bogaard. Rational Verification for Nash and Subgame-Perfect Equilibria in Graph Games. In Jérôme Leroux, Sylvain Lombardy, and David Peleg, editors, 48th International Symposium on Mathematical Foundations of Computer Science, MFCS 2023, August 28 to September 1, 2023, Bordeaux, France, volume 272 of LIPIcs, pages 26:1-26:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.MFCS.2023.26.
  8. 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. Inf. Comput., 278:104594, 2021. URL: https://doi.org/10.1016/J.IC.2020.104594.
  9. 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 International Conference 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.
  10. Thomas Brihaye, Véronique Bruyère, Aline Goeminne, and Nathan Thomasset. On relevant equilibria in reachability games. J. Comput. Syst. Sci., 119:211-230, 2021. URL: https://doi.org/10.1016/J.JCSS.2021.02.009.
  11. Thomas Brihaye, Véronique Bruyère, and Gaspard Reghem. Quantitative Reachability Stackelberg-Pareto Synthesis is NEXPTIME-Complete. In Olivier Bournez, Enrico Formenti, and Igor Potapov, editors, Reachability Problems - 17th International Conference, RP 2023, Nice, France, October 11-13, 2023, Proceedings, volume 14235 of Lecture Notes in Computer Science, pages 70-84. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-45286-4_6.
  12. Thomas Brihaye, Julie De Pril, and Sven Schewe. Multiplayer Cost Games with Simple Nash Equilibria. In Sergei N. Artëmov and Anil Nerode, editors, 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. URL: https://doi.org/10.1007/978-3-642-35722-0_5.
  13. Thomas Brihaye, Gilles Geeraerts, Axel Haddad, and Benjamin Monmege. To Reach or not to Reach? Efficient Algorithms for Total-Payoff Games. In Luca Aceto and David de Frutos-Escrig, editors, 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, volume 42 of LIPIcs, pages 297-310. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPICS.CONCUR.2015.297.
  14. Thomas Brihaye and Aline Goeminne. Multi-weighted Reachability Games. In Olivier Bournez, Enrico Formenti, and Igor Potapov, editors, Reachability Problems - 17th International Conference, RP 2023, Nice, France, October 11-13, 2023, Proceedings, volume 14235 of Lecture Notes in Computer Science, pages 85-97, Cham, 2023. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-45286-4_7.
  15. Thomas Brihaye, Aline Goeminne, James C. A. Main, and Mickael Randour. Reachability Games and Friends: A Journey Through the Lens of Memory and Complexity (Invited Talk). In Patricia Bouyer and Srikanth Srinivasan, editors, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2023, December 18-20, 2023, IIIT Hyderabad, Telangana, India, volume 284 of LIPIcs, pages 1:1-1:26. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2023.1.
  16. Véronique Bruyère. Synthesis of Equilibria in Infinite-Duration Games on Graphs. ACM SIGLOG News, 8(2):4-29, May 2021. URL: https://doi.org/10.1145/3467001.3467003.
  17. Véronique Bruyère, Christophe Grandmont, and Jean-François Raskin. As soon as possible but rationally. CoRR, abs/2403.00399, 2024. URL: https://doi.org/10.48550/arXiv.2403.00399.
  18. Véronique Bruyère, Jean-François Raskin, and Clément Tamines. Stackelberg-Pareto Synthesis. In Serge Haddad and Daniele Varacca, editors, 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 of LIPIcs, pages 27:1-27:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.CONCUR.2021.27.
  19. 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 International Conference 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.
  20. Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Generalized Mean-payoff and Energy Games. In Kamal Lodaya and Meena Mahajan, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, December 15-18, 2010, Chennai, India, volume 8 of LIPIcs, pages 505-516. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2010.505.
  21. Rodica Condurache, Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin. The Complexity of Rational Synthesis. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 121:1-121:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.ICALP.2016.121.
  22. A. Ehrenfeucht and J. Mycielski. Positional strategies for mean payoff games. International Journal of Game Theory, 8(2):109-113, June 1979. URL: https://doi.org/10.1007/BF01768705.
  23. Diego Figueira and Leonid Libkin. Path Logics for Querying Graphs: Combining Expressiveness and Efficiency. In Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Kyoto, Japan, July 2015. IEEE. URL: https://doi.org/10.1109/LICS.2015.39.
  24. Nathanaël Fijalkow and Florian Horn. Les jeux d'accessibilité généralisée. Tech. Sci. Informatiques, 32(9-10):931-949, 2013. URL: https://doi.org/10.3166/TSI.32.931-949.
  25. Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin. The Adversarial Stackelberg Value in Quantitative Games. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020), volume 168 of Leibniz International Proceedings in Informatics (LIPIcs), pages 127:1-127:18, Dagstuhl, Germany, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.127.
  26. 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 International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, 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.
  27. Christophe Grandmont. Rational Synthesis and Verification in Multiplayer Reachability Games Played on Graphs. Master’s thesis, UMONS, June 2023. Google Scholar
  28. 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.
  29. Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, and Michael J. Wooldridge. On the complexity of rational verification. Ann. Math. Artif. Intell., 91(4):409-430, 2023. URL: https://doi.org/10.1007/S10472-022-09804-3.
  30. David Hyland, Julian Gutierrez, Shankaranarayanan Krishna, and Michael J. Wooldridge. Rational verification with quantitative probabilistic goals. In Mehdi Dastani, Jaime Simão Sichman, Natasha Alechina, and Virginia Dignum, editors, Proceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2024, Auckland, New Zealand, May 6-10, 2024, pages 871-879. ACM, 2024. URL: https://doi.org/10.5555/3635637.3662941.
  31. Marcin Jurdzinski, Francois Laroussinie, and Jeremy Sproston. Model Checking Probabilistic Timed Automata with One or Two Clocks. Logical Methods in Computer Science, Volume 4, Issue 3, September 2008. URL: https://doi.org/10.2168/LMCS-4(3:12)2008.
  32. Felix Klaedtke and Harald Rueß. Monadic Second-Order Logics with Cardinalities. In Jos C. M. Baeten, Jan Karel Lenstra, Joachim Parrow, and Gerhard J. Woeginger, editors, Automata, Languages and Programming, pages 681-696, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg. Google Scholar
  33. Orna Kupferman, Giuseppe Perelli, and Moshe Y. Vardi. Synthesis with Rational Environments. In Nils Bulling, editor, Multi-Agent Systems - 12th European Conference, EUMAS 2014, Prague, Czech Republic, December 18-19, 2014, Revised Selected Papers, volume 8953 of Lecture Notes in Computer Science, pages 219-235. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-17130-2_15.
  34. Orna Kupferman and Noam Shenwald. The Complexity of LTL Rational Synthesis. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 25-45, Cham, 2022. Springer International Publishing. Google Scholar
  35. John F. Nash. Equilibrium points in n-person games. Proceedings of the National Academy of Sciences of the United States of America, 36:48-49, 1950. URL: https://doi.org/10.1073/pnas.36.1.48.
  36. Martin J. Osborne. An introduction to game theory. Oxford Univ. Press, 2004. Google Scholar
  37. Christos H. Papadimitriou and Mihalis Yannakakis. On the Approximability of Trade-offs and Optimal Access of Web Sources. In 41st Annual Symposium on Foundations of Computer Science, FOCS 2000, 12-14 November 2000, Redondo Beach, California, USA, pages 86-92. IEEE Computer Society, 2000. URL: https://doi.org/10.1109/SFCS.2000.892068.
  38. Amir Pnueli and Roni Rosner. On the Synthesis of a Reactive Module. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989, pages 179-190. ACM Press, 1989. URL: https://doi.org/10.1145/75277.75293.
  39. Senthil Rajasekaran, Suguman Bansal, and Moshe Y. Vardi. Multi-Agent Systems with Quantitative Satisficing Goals. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China, pages 280-288. ijcai.org, 2023. URL: https://doi.org/10.24963/IJCAI.2023/32.
  40. Mickael Randour. Games with multiple objectives. In Nathanaël Fijalkow, editor, Games on Graphs. Online, 2023. URL: https://doi.org/10.48550/arxiv.2305.10546.
  41. Mickael Randour, Jean-François Raskin, and Ocan Sankur. Percentile queries in multi-dimensional Markov decision processes. Formal Methods Syst. Des., 50(2-3):207-248, 2017. URL: https://doi.org/10.1007/S10703-016-0262-7.
  42. Larry J. Stockmeyer. The polynomial-time hierarchy. Theoretical Computer Science, 3(1):1-22, 1976. URL: https://doi.org/10.1016/0304-3975(76)90061-X.
  43. Stephen Travers. The complexity of membership problems for circuits over sets of integers. Theoretical Computer Science, 369(1):211-229, 2006. URL: https://doi.org/10.1016/j.tcs.2006.08.017.
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 About DROPS Imprint Privacy Contact