Document Open Access Logo

Characterising and Verifying the Core in Concurrent Multi-Player Mean-Payoff Games

Authors Julian Gutierrez, Anthony W. Lin , Muhammad Najib , Thomas Steeples, Michael Wooldridge

PDF
Thumbnail PDF

File

LIPIcs.CSL.2024.32.pdf
  • Filesize: 0.97 MB
  • 25 pages

Document Identifiers

Author Details

Julian Gutierrez
  • Monash University, Clayton, Australia
Anthony W. Lin
  • University of Kaiserslautern-Landau, Germany
  • Max-Planck Institute for Software Systems, Kaiserslautern, Germany
Muhammad Najib
  • Heriot-Watt University, Edinburgh, UK
Thomas Steeples
  • University of Oxford, UK
Michael Wooldridge
  • University of Oxford, UK

Funding

  • Gutierrez, Julian: Research partially sponsored by the DARPA Assured Neuro Symbolic Learning and Reasoning (ANSR) program under award number FA8750-23-2-1016.
  • Lin, Anthony W.: supported by European Research Council under European Union’s Horizon research and innovation programme (grant agreement no https://doi.org/10.3030/101089343)
  • Wooldridge, Michael: Supported by a UKRI Turing AI World Leading Researcher Fellowship (EP/W002949/1).

Acknowledgements

We wish to thank anonymous reviewers for their useful feedback.

Cite AsGet BibTex

Julian Gutierrez, Anthony W. Lin, Muhammad Najib, Thomas Steeples, and Michael Wooldridge. Characterising and Verifying the Core in Concurrent Multi-Player Mean-Payoff Games. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 32:1-32:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CSL.2024.32

Abstract

Concurrent multi-player mean-payoff games are important models for systems of agents with individual, non-dichotomous preferences. Whilst these games have been extensively studied in terms of their equilibria in non-cooperative settings, this paper explores an alternative solution concept: the core from cooperative game theory. This concept is particularly relevant for cooperative AI systems, as it enables the modelling of cooperation among agents, even when their goals are not fully aligned. Our contribution is twofold. First, we provide a characterisation of the core using discrete geometry techniques and establish a necessary and sufficient condition for its non-emptiness. We then use the characterisation to prove the existence of polynomial witnesses in the core. Second, we use the existence of such witnesses to solve key decision problems in rational verification and provide tight complexity bounds for the problem of checking whether some/every equilibrium in a game satisfies a given LTL or GR(1) specification. Our approach is general and can be adapted to handle other specifications expressed in various fragments of LTL without incurring additional computational costs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Verification by model checking
  • Theory of computation → Solution concepts in game theory
Keywords
  • Concurrent games
  • multi-agent systems
  • temporal logic
  • game theory

Metrics

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

Related Versions

References

  1. Alessandro Abate, Julian Gutierrez, Lewis Hammond, Paul Harrenstein, Marta Kwiatkowska, Muhammad Najib, Giuseppe Perelli, Thomas Steeples, and Michael Wooldridge. Rational verification: game-theoretic verification of multi-agent systems. Applied Intelligence, 51(9):6569-6584, 2021. Google Scholar
  2. S. Almagor, G. Avni, and O. Kupferman. Repairing Multi-Player Games. In CONCUR, volume 42 of LIPIcs, pages 325-339. Schloss Dagstuhl, 2015. Google Scholar
  3. 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, pages 333-347, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. Google Scholar
  4. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672-713, September 2002. URL: https://doi.org/10.1145/585265.585270.
  5. Robert J Aumann. The core of a cooperative game without side payments. Transactions of the American Mathematical Society, 98(3):539-552, 1961. Google Scholar
  6. Raphaël Berthon, Shibashis Guha, and Jean-François Raskin. Mixing probabilistic and non-probabilistic objectives in markov decision processes. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 195-208, 2020. Google Scholar
  7. Elisa Bertino, Finale Doshi-Velez, Maria Gini, Daniel Lopresti, and David Parkes. Artificial intelligence and cooperation. Technical Report White Paper 4, Computing Community Consortium, Washington, D.C., October 2020. URL: https://cra.org/ccc/wp-content/uploads/sites/2/2020/11/AI-and-Cooperation.pdf.
  8. Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, and Yaniv Sa'ar. Synthesis of reactive(1) designs. J. Comput. Syst. Sci., 78(3):911-938, May 2012. URL: https://doi.org/10.1016/j.jcss.2011.08.007.
  9. Udi Boker, Krishnendu Chatterjee, Thomas A. Henzinger, and Orna Kupferman. Temporal specifications with accumulative values. ACM Trans. Comput. Log., 15(4):1-25, August 2014. URL: https://doi.org/10.1145/2629686.
  10. Olga N Bondareva. Some applications of linear programming methods to the theory of cooperative games. Problemy kibernetiki, 10(119):139, 1963. Google Scholar
  11. Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. Pure Nash equilibria in concurrent deterministic games. Log. Meth. Comput. Sci., 11(2), June 2015. URL: https://doi.org/10.2168/lmcs-11(2:9)2015.
  12. Patricia Bouyer, Orna Kupferman, Nicolas Markey, Bastien Maubert, Aniello Murano, and Giuseppe Perelli. Reasoning about quality and fuzziness of strategic behaviors. ACM Transactions on Computational Logic, 24(3):1-38, 2023. Google Scholar
  13. Romain Brenguier and Jean-François Raskin. Pareto curves of multidimensional mean-payoff games. In Daniel Kroening and Corina S. Păsăreanu, editors, Computer Aided Verification, pages 251-267. Springer International Publishing, 2015. Google Scholar
  14. 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.
  15. Thomas Brihaye, Julie De Pril, and Sven Schewe. Multiplayer cost games with simple nash equilibria. In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science, pages 59-73, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  16. Nils Bulling and Valentin Goranko. Combining quantitative and qualitative reasoning in concurrent multi-player games. Autonomous Agents and Multi-Agent Systems, 36:1-33, 2022. Google Scholar
  17. Alberto Camacho, Meghyn Bienvenu, and Sheila A McIlraith. Towards a unified view of ai planning and reactive synthesis. In Proceedings of the International Conference on Automated Planning and Scheduling, volume 29, pages 58-67, 2019. Google Scholar
  18. Arindam Chakrabarti, Krishnendu Chatterjee, Thomas A. Henzinger, Orna Kupferman, and Rupak Majumdar. Verifying quantitative properties using bound functions. In Dominique Borrione and Wolfgang Paul, editors, Correct Hardware Design and Verification Methods, pages 50-64, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  19. Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, and Mariëlle Stoelinga. Resource interfaces. In Rajeev Alur and Insup Lee, editors, Embedded Software, pages 117-133, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg. Google Scholar
  20. Georgios Chalkiadakis, Edith Elkind, and Michael J. Wooldridge. Computational Aspects of Cooperative Game Theory. Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan & Claypool Publishers, 2011. URL: https://doi.org/10.2200/S00355ED1V01Y201107AIM016.
  21. Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Generalized Mean-payoff and Energy Games. In FSTTCS, pages 505-516, 2010. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2010.505.
  22. Krishnendu Chatterjee, Arkadeb Ghosal, Thomas A. Henzinger, Daniel Iercan, Christoph M. Kirsch, Claudio Pinello, and Alberto Sangiovanni-Vincentelli. Logical reliability of interacting real-time tasks. In 2008 Design, Automation and Test in Europe, pages 909-914, 2008. URL: https://doi.org/10.1109/DATE.2008.4484790.
  23. Krishnendu Chatterjee, Thomas A Henzinger, and Nir Piterman. Strategy logic. Information and Computation, 208(6):677-693, 2010. Google Scholar
  24. Vincent Conitzer and Caspar Oesterheld. Foundations of cooperative AI. In Brian Williams, Yiling Chen, and Jennifer Neville, editors, Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2023, Washington, DC, USA, February 7-14, 2023, pages 15359-15367. AAAI Press, 2023. URL: https://doi.org/10.1609/AAAI.V37I13.26791.
  25. Allan Dafoe, Yoram Bachrach, Gillian Hadfield, Eric Horvitz, Kate Larson, and Thore Graepel. Cooperative ai: machines must learn to find common ground. Nature, 593(7857):33-36, 2021. Google Scholar
  26. Allan Dafoe, Edward Hughes, Yoram Bachrach, Tantum Collins, Kevin R McKee, Joel Z Leibo, Kate Larson, and Thore Graepel. Open problems in cooperative ai. arXiv preprint arXiv:2012.08630, 2020. Google Scholar
  27. Aldric Degorre, Laurent Doyen, Raffaella Gentilini, Jean-François Raskin, and Szymon Toruńczyk. Energy and mean-payoff games with imperfect information. In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, pages 260-274, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. Google Scholar
  28. Stéphane Demri and Philippe Schnoebelen. The complexity of propositional linear temporal logics in simple cases. Information and Computation, 174(1):84-103, 2002. Google Scholar
  29. A. Ehrenfeucht and J. Mycielski. Positional strategies for mean payoff games. Int. J. Game Theory, 8(2):109-113, June 1979. URL: https://doi.org/10.1007/BF01768705.
  30. E. Allen Emerson and Chin-Laung Lei. Modalities for model checking: Branching time logic strikes back. Sci. Comput. Program., 8(3):275-306, June 1987. URL: https://doi.org/10.1016/0167-6423(87)90036-0.
  31. Ioannis Filippidis, Sumanth Dathathri, Scott C Livingston, Necmiye Ozay, and Richard M Murray. Control design for hybrid systems with tulip: The temporal logic planning toolbox. In 2016 IEEE Conference on Control Applications (CCA), pages 1030-1041. IEEE, 2016. Google Scholar
  32. Dana Fisman, Orna Kupferman, and Yoad Lustig. Rational synthesis. In 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 16, pages 190-204. Springer, 2010. Google Scholar
  33. Donald B Gillies. Solutions to general non-zero-sum games. Contributions to the Theory of Games, 4(40):47-85, 1959. Google Scholar
  34. Branko Grünbaum, Volker Kaibel, Victor Klee, and Günter M. Ziegler. Convex polytopes. Springer, New York, 2003. URL: http://www.springer.com/mathematics/geometry/book/978-0-387-00424-2.
  35. Zhaoyuan Gu, Nathan Boyd, and Ye Zhao. Reactive locomotion decision-making and robust motion planning for real-time perturbation recovery. In 2022 International Conference on Robotics and Automation (ICRA), pages 1896-1902, 2022. URL: https://doi.org/10.1109/ICRA46639.2022.9812068.
  36. Julian Gutierrez, Lewis Hammond, Anthony W. Lin, Muhammad Najib, and Michael J. Wooldridge. Rational verification for probabilistic systems. In Meghyn Bienvenu, Gerhard Lakemeyer, and Esra Erdem, editors, Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning, KR 2021, Online event, November 3-12, 2021, pages 312-322, 2021. URL: https://doi.org/10.24963/kr.2021/30.
  37. Julian Gutierrez, Paul Harrenstein, and Michael Wooldridge. Iterated boolean games. Inform. Comput., 242:53-79, June 2015. URL: https://doi.org/10.1016/j.ic.2015.03.011.
  38. Julian Gutierrez, Paul Harrenstein, and Michael J. Wooldridge. From model checking to equilibrium checking: Reactive modules for rational verification. Artif. Intell., 248:123-157, 2017. URL: https://doi.org/10.1016/j.artint.2017.04.003.
  39. Julian Gutierrez, Szymon Kowara, Sarit Kraus, Thomas Steeples, and Michael Wooldridge. Cooperative concurrent games. Artificial Intelligence, 314:103806, 2023. Google Scholar
  40. Julian Gutierrez, Sarit Kraus, and Michael J. Wooldridge. Cooperative concurrent games. In Edith Elkind, Manuela Veloso, Noa Agmon, and Matthew E. Taylor, editors, Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS '19, Montreal, QC, Canada, May 13-17, 2019, pages 1198-1206. International Foundation for Autonomous Agents and Multiagent Systems, 2019. URL: http://dl.acm.org/citation.cfm?id=3331822.
  41. Julian Gutierrez, Anthony W. Lin, Muhammad Najib, Thomas Steeples, and Michael Wooldridge. Characterising and verifying the core in concurrent multi-player mean-payoff games (full version), 2023. URL: https://arxiv.org/abs/2311.15883.
  42. Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, and Michael Wooldridge. Equilibrium Design for Concurrent Games. In Wan Fokkink and Rob van Glabbeek, editors, 30th International Conference on Concurrency Theory (CONCUR 2019), volume 140 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1-22:16, Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.22.
  43. Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, and Michael Wooldridge. On the complexity of rational verification. Annals of Mathematics and Artificial Intelligence, 91(4):409-430, 2023. Google Scholar
  44. Dexter Kozen. Lower bounds for natural proof systems. In 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pages 254-266, 1977. URL: https://doi.org/10.1109/SFCS.1977.16.
  45. Orna Kupferman, Giuseppe Perelli, and Moshe Y. Vardi. Synthesis with rational environments. Ann. Math. Artif. Intel., 78(1):3-20, June 2016. URL: https://doi.org/10.1007/s10472-016-9508-8.
  46. Shahar Maoz and Jan Oliver Ringert. Gr (1) synthesis for ltl specification patterns. In Proceedings of the 2015 10th joint meeting on foundations of software engineering, pages 96-106, 2015. Google Scholar
  47. Shahar Maoz and Yaniv Sa'ar. Assume-guarantee scenarios: Semantics and synthesis. In Robert B. France, Jürgen Kazmeier, Ruth Breu, and Colin Atkinson, editors, Model Driven Engineering Languages and Systems, pages 335-351, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. Google Scholar
  48. Nicolas Markey. Past is for free: on the complexity of verifying linear temporal properties with past. Acta Informatica, 40:431-458, 2004. Google Scholar
  49. Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y Vardi. Reasoning about strategies: On the model-checking problem. ACM Transactions on Computational Logic (TOCL), 15(4):1-47, 2014. Google Scholar
  50. C. Papadimitriou. Computational complexity. Addison-Wesley, Reading, Massachusetts, 1994. Google Scholar
  51. G. Perelli. Enforcing equilibria in multi-agent systems. In Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS '19, pages 188-196, 2019. URL: http://dl.acm.org/citation.cfm?id=3306127.3331692.
  52. Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pages 46-57. IEEE, September 1977. URL: https://doi.org/10.1109/sfcs.1977.32.
  53. Debraj Ray and Rajiv Vohra. Equilibrium binding agreements. Journal of Economic theory, 73(1):30-78, 1997. Google Scholar
  54. Herbert E Scarf. The core of an n person game. Econometrica: Journal of the Econometric Society, pages 50-69, 1967. Google Scholar
  55. Herbert E Scarf. On the existence of a coopertive solution for a general class of n-person games. Journal of Economic Theory, 3(2):169-181, 1971. Google Scholar
  56. A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733-749, July 1985. URL: https://doi.org/10.1145/3828.3837.
  57. Thomas Steeples, Julian Gutierrez, and Michael Wooldridge. Mean-payoff games with ω-regular specifications. In Proceedings of the 20th International Conference on Autonomous Agents and MultiAgent Systems, pages 1272-1280, 2021. Google Scholar
  58. M. Ummels and D. Wojtczak. The Complexity of Nash Equilibria in Limit-Average Games. In CONCUR, pages 482-496, 2011. URL: https://doi.org/10.1007/978-3-642-23217-6_32.
  59. Metin Uyanık. On the nonemptiness of the α-core of discontinuous games: Transferable and nontransferable utilities. Journal of Economic Theory, 158:213-231, 2015. Google Scholar
  60. Yaron Velner, Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Alexander Rabinovich, and Jean-François Raskin. The complexity of multi-mean-payoff and multi-energy games. Inform. Comput., 241:177-196, April 2015. URL: https://doi.org/10.1016/j.ic.2015.03.001.
  61. M. Wooldridge, J. Gutierrez, P. Harrenstein, E. Marchioni, G. Perelli, and A. Toumi. Rational Verification: From Model Checking to Equilibrium Checking. In AAAI, pages 4184-4191. AAAIPress, 2016. Google Scholar
  62. Uri Zwick and Mike Paterson. The complexity of mean payoff games on graphs. Theor. Comput. Sci., 158(1-2):343-359, May 1996. URL: https://doi.org/10.1016/0304-3975(95)00188-3.
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