Document Open Access Logo

Expresiveness and Complexity Results for Strategic Reasoning

Authors Julian Gutierrez, Paul Harrenstein, Michael Wooldridge

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2015.268.pdf
  • Filesize: 481 kB
  • 15 pages

Document Identifiers

Subject Classification

Keywords
  • Temporal logic
  • Nash equilibrium
  • game models
  • formal verification

Metrics

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

Abstract

This paper presents a range of expressiveness and complexity results for the specification, computation, and verification of Nash equilibria in multi-player non-zero-sum concurrent games in which players have goals expressed as temporal logic formulae. Our results are based on a novel approach to the characterisation of equilibria in such games: a semantic characterisation based on winning strategies and memoryful reasoning. This characterisation allows us to obtain a number of other results relating to the analysis of equilibrium properties in temporal logic.  

We show that, up to bisimilarity, reasoning about Nash equilibria in multi-player non-zero-sum concurrent games can be done in ATL^* and that constructing equilibrium strategy profiles in such games can be done in 2EXPTIME using finite-memory strategies. We also study two simpler cases, two-player games and sequential games, and show that the specification of equilibria in the latter setting can be obtained in a temporal logic that is weaker than ATL^*. Based on these results, we settle a few open problems, put forward new logical characterisations of equilibria, and provide improved answers and alternative solutions to a number of questions.

Cite As Get BibTex

Julian Gutierrez, Paul Harrenstein, and Michael Wooldridge. Expresiveness and Complexity Results for Strategic Reasoning. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 268-282, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CONCUR.2015.268

Author Details

Julian Gutierrez
Paul Harrenstein
Michael Wooldridge

References

  1. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672-713, 2002. Google Scholar
  2. Krishnendu Chatterjee and Thomas A. Henzinger. A survey of stochastic ω-regular games. J. Comput. Syst. Sci., 78(2):394-413, 2012. Google Scholar
  3. Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Strategy logic. Inf. Comput., 208(6):677-693, 2010. Google Scholar
  4. Bernd Finkbeiner and Sven Schewe. Coordination logic. In CSL, volume 6247 of LNCS, pages 305-319. Springer, 2010. Google Scholar
  5. Julian Gutierrez, Paul Harrenstein, and Michael Wooldridge. Iterated Boolean games. Inf. Comput., 242:53-79, 2015. Google Scholar
  6. Julian Gutierrez and Michael Wooldridge. Equilibria of concurrent games on event structures. In CSL-LICS. ACM, 2014. Google Scholar
  7. Orna Kupferman and Moshe Y. Vardi. Memoryful branching-time logic. In LICS, pages 265-274. IEEE Computer Society, 2006. Google Scholar
  8. François Laroussinie. Temporal logics for games. Bulletin of the EATCS, 100:79-98, 2010. Google Scholar
  9. François Laroussinie and Nicolas Markey. Quantified CTL: expressiveness and complexity. LMCS, 10(4), 2014. Google Scholar
  10. François Laroussinie and Nicolas Markey. Augmenting ATL with strategy contexts. Inf. Comput., 2015. To appear. Google Scholar
  11. Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y. Vardi. Reasoning about strategies: On the model-checking problem. ACM Trans. Comput. Log., 15(4):34, 2014. Google Scholar
  12. Fabio Mogavero, Aniello Murano, and Luigi Sauro. On the boundary of behavioral strategies. In LICS, pages 263-272. IEEE Computer Society, 2013. Google Scholar
  13. Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi. Relentful strategic reasoning in alternating-time temporal logic. J. Log. Comput., 2015. To appear. Google Scholar
  14. Martin Osborne and Ariel Rubinstein. A Course in Game Theory. The MIT Press, 1994. Google Scholar
  15. Sven Schewe. ATL* satisfiability is 2EXPTIME-complete. In ICALP, volume 5126 of LNCS, pages 373-385. Springer, 2008. Google Scholar
  16. Wiebe van der Hoek and Michael Wooldridge. Logics for multiagent systems. AI Magazine, 33(3):92-105, 2012. Google Scholar
  17. Igor Walukiewicz. A landscape with games in the background. In LICS, pages 356-366. IEEE Computer Society, 2004. Google Scholar
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