Equilibrium Design for Concurrent Games

Authors Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, Michael Wooldridge

Thumbnail PDF


  • Filesize: 0.56 MB
  • 16 pages

Document Identifiers

Author Details

Julian Gutierrez
  • Department of Computer Science, University of Oxford, UK
Muhammad Najib
  • Department of Computer Science, University of Oxford, UK
Giuseppe Perelli
  • Department of Computer Science, University of Göteborg, Sweden
Michael Wooldridge
  • Department of Computer Science, University of Oxford, UK

Cite AsGet BibTex

Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, and Michael Wooldridge. Equilibrium Design for Concurrent Games. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 22:1-22:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


In game theory, mechanism design is concerned with the design of incentives so that a desired outcome of the game can be achieved. In this paper, we study the design of incentives so that a desirable equilibrium is obtained, for instance, an equilibrium satisfying a given temporal logic property - a problem that we call equilibrium design. We base our study on a framework where system specifications are represented as temporal logic formulae, games as quantitative concurrent game structures, and players' goals as mean-payoff objectives. In particular, we consider system specifications given by LTL and GR(1) formulae, and show that implementing a mechanism to ensure that a given temporal logic property is satisfied on some/every Nash equilibrium of the game, whenever such a mechanism exists, can be done in PSPACE for LTL properties and in NP/Sigma^P_2 for GR(1) specifications. We also study the complexity of various related decision and optimisation problems, such as optimality and uniqueness of solutions, and show that the complexities of all such problems lie within the polynomial hierarchy. As an application, equilibrium design can be used as an alternative solution to the rational synthesis and verification problems for concurrent games with mean-payoff objectives whenever no solution exists, or as a technique to repair, whenever possible, concurrent games with undesirable rational outcomes (Nash equilibria) in an optimal way.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Computing methodologies → Multi-agent systems
  • Theory of computation → Algorithmic game theory
  • Games
  • Temporal logic
  • Synthesis
  • Model checking
  • Nash equilibrium


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


  1. Gadi Aleksandrowicz, Hana Chockler, Joseph Y. Halpern, and Alexander Ivrii. The Computational Complexity of Structure-based Causality. J. Artif. Int. Res., 58(1):431-451, January 2017. URL: http://dl.acm.org/citation.cfm?id=3176764.3176775.
  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. S. Almagor, O. Kupferman, and G. Perelli. Synthesis of Controllable Nash Equilibria in Quantitative Objective Games. In IJCAI, pages 35-41, 2018. Google Scholar
  4. B. Aminof, V. Malvone, A. Murano, and S. Rubin. Graded Strategy Logic: Reasoning about Uniqueness of Nash Equilibria. In AAMAS, pages 698-706. ACM, 2016. Google Scholar
  5. R. Bloem, B. Jobstmann, N. Piterman, A. Pnueli, and Y. Sa'ar. Synthesis of Reactive(1) designs. Journal of Computer and System Sciences, 78(3):911-938, 2012. Google Scholar
  6. A. Bohy, V. Bruyère, E. Filiot, and J. Raskin. Synthesis from LTL Specifications with Mean-Payoff Objectives. In TACAS, pages 169-184, 2013. Google Scholar
  7. U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman. Temporal Specifications with Accumulative Values. ACM Transactions on Computational Logic, 15(4):27:1-27:25, 2014. URL: http://dx.doi.org/10.1145/2629686.
  8. P. Bouyer, R. Brenguier, N. Markey, and M. Ummels. Pure Nash Equilibria in Concurrent Deterministic Games. Logical Methods in Computer Science, 11(2), 2015. Google Scholar
  9. K. Chatterjee and L. Doyen. Energy parity games. Theoretical Computer Science, 458:49-60, 2012. Google Scholar
  10. K. Chatterjee, L. Doyen, T. Henzinger, and J. Raskin. Generalized Mean-payoff and Energy Games. In FSTTCS, pages 505-516, 2010. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2010.505.
  11. K. Chatterjee, T. A. Henzinger, and M. Jurdzinski. Mean-Payoff Parity Games. In LICS, pages 178-187. IEEE Computer Society, 2005. Google Scholar
  12. H. Chockler and J. Halpern. Responsibility and Blame: A Structural-Model Approach. Journal of Artificial Intelligence Research, 22:93-115, 2004. Google Scholar
  13. 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
  14. D. Fisman, O. Kupferman, and Y. Lustig. Rational Synthesis. In TACAS, volume 6015 of LNCS, pages 190-204. Springer, 2010. Google Scholar
  15. J. Gutierrez, P. Harrenstein, G. Perelli, and M. Wooldridge. Nash Equilibrium and Bisimulation Invariance. In CONCUR, volume 85 of LIPIcs, pages 17:1-17:16. Schloss Dagstuhl, 2017. Google Scholar
  16. J. Gutierrez, P. Harrenstein, and M. Wooldridge. Iterated Boolean Games. Information and Computation, 242:53-79, 2015. Google Scholar
  17. J. Gutierrez, P. Harrenstein, and M. Wooldridge. From Model Checking to Equilibrium Checking: Reactive Modules for Rational Verification. Artificial Intelligence, 248:123-157, 2017. Google Scholar
  18. J. Gutierrez, A. Murano, G. Perelli, S. Rubin, and M. Wooldridge. Nash Equilibria in Concurrent Games with Lexicographic Preferences. In IJCAI, pages 1067-1073, 2017. URL: http://dx.doi.org/10.24963/ijcai.2017/148.
  19. J. Gutierrez, M. Najib, G. Perelli, and M. Wooldridge. EVE: A Tool for Temporal Equilibrium Analysis. In ATVA, volume 11138 of LNCS, pages 551-557. Springer, 2018. Google Scholar
  20. J. Gutierrez, M. Najib, G. Perelli, and M. Wooldridge. On Computational Tractability for Rational Verification. In IJCAI, 2019. To appear. Google Scholar
  21. L. Hurwicz and S. Reiter. Designing Economic Mechanisms. Cambridge University Press, 2006. Google Scholar
  22. M. Krentel. The Complexity of Optimization Problems. Journal of Computer and System Sciences, 36(3):490-509, 1988. URL: http://dx.doi.org/10.1016/0022-0000(88)90039-6.
  23. O. Kupferman, G. Perelli, and M. Y. Vardi. Synthesis with Rational Environments. Annals of Mathematics and Artificial Intelligence, 78(1):3-20, 2016. Google Scholar
  24. M. Wooldridge and U. Endriss and S. Kraus and J. Lang. Incentive engineering for Boolean games. Artificial Intelligence, 195:418-439, 2013. URL: http://dx.doi.org/10.1016/j.artint.2012.11.003.
  25. M. Maschler, E. Solan, and S. Zamir. Game Theory. Cambridge University Press, 2013. Google Scholar
  26. M.J. Osborne and A. Rubinstein. A Course in Game Theory. MIT Press, 1994. Google Scholar
  27. C. Papadimitriou. On the Complexity of Unique Solutions. Journal of the ACM, 31(2):392-400, 1984. URL: http://dx.doi.org/10.1145/62.322435.
  28. C. Papadimitriou. Computational complexity. Addison-Wesley, Reading, Massachusetts, 1994. Google Scholar
  29. C. Papadimitriou and M. Yannakakis. The Complexity of Facets (and some Facets of Complexity). Journal of Computer and System Sciences, 28(2):244-259, 1984. Google Scholar
  30. 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.
  31. A. Pnueli. The Temporal Logic of Programs. In FOCS, pages 46-57. IEEE, 1977. Google Scholar
  32. A. Pnueli and R. Rosner. On the Synthesis of a Reactive Module. In POPL, pages 179-190. ACM Press, 1989. Google Scholar
  33. M. Ummels and D. Wojtczak. The Complexity of Nash Equilibria in Limit-Average Games. In CONCUR, pages 482-496, 2011. URL: http://dx.doi.org/10.1007/978-3-642-23217-6_32.
  34. Y. Velner, K. Chatterjee, L. Doyen, T. Henzinger, A. Rabinovich, and J. Raskin. The Complexity of Multi-Mean-Payoff and Multi-Energy Games. Information and Computation, 241:177-196, 2015. Google Scholar
  35. U. Zwick and M. Paterson. The Complexity of Mean Payoff Games on Graphs. Theoretical Computer Science, 158(1):343-359, 1996. URL: http://dx.doi.org/10.1016/0304-3975(95)00188-3.
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail