Nash Equilibrium and Bisimulation Invariance

Authors Julian Gutierrez, Paul Harrenstein, Giuseppe Perelli, Michael Wooldridge



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2017.17.pdf
  • Filesize: 498 kB
  • 16 pages

Document Identifiers

Author Details

Julian Gutierrez
Paul Harrenstein
Giuseppe Perelli
Michael Wooldridge

Cite AsGet BibTex

Julian Gutierrez, Paul Harrenstein, Giuseppe Perelli, and Michael Wooldridge. Nash Equilibrium and Bisimulation Invariance. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CONCUR.2017.17

Abstract

Game theory provides a well-established framework for the analysis of concurrent and multi-agent systems. The basic idea is that concurrent processes (agents) can be understood as corresponding to players in a game; plays represent the possible computation runs of the system; and strategies define the behaviour of agents. Typically, strategies are modelled as functions from sequences of system states to player actions. Analysing a system in such a way involves computing the set of (Nash) equilibria in the game. However, we show that, with respect to the above model of strategies---the standard model in the literature---bisimilarity does not preserve the existence of Nash equilibria. Thus, two concurrent games which are behaviourally equivalent from a semantic perspective, and which from a logical perspective satisfy the same temporal formulae, nevertheless have fundamentally different properties from a game theoretic perspective. In this paper we explore the issues raised by this discovery, and investigate three models of strategies with respect to which the existence of Nash equilibria is preserved under bisimilarity. We also use some of these models of strategies to provide new semantic foundations for logics for strategic reasoning, and investigate restricted scenarios where bisimilarity can be shown to preserve the existence of Nash equilibria with respect to the conventional model of strategies in the literature.
Keywords
  • Bisumulation
  • Nash equilibrium
  • Multiagent systems
  • Strategy logic

Metrics

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

References

  1. S. Almagor, G. Avni, and O. Kupferman. Repairing multi-player games. In L. Aceto and D. de Frutos Escri, editors, Proceedings of the Twenty-Sixth Annual Conference on Concurrency Theory (CONCUR'15), Leibniz International Proceedings in Informatics (LIPIcs), pages 325-339, Madrid, Spain, 2015. Google Scholar
  2. R. Alur and T. A. Henzinger. Reactive modules. Formal Methods in System Design, 15(1):7-48, 1999. Google Scholar
  3. R. Alur, T. A. Henzinger, O. Kupferman, and M. Y. Vardi. Alternating refinement relations. In Proceedings of the 9th International Conference on Concurrency Theory (CONCUR'98), volume 1466 of LNCS, pages 163-178. Springer-Verlag, Berlin, Germany, 1998. Google Scholar
  4. R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-Time Temporal Logic. Journal of the ACM, 49(5):672-713, 2002. Google Scholar
  5. C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008. Google Scholar
  6. P. Bouyer, R. Brenguier, N. Markey, and M. Ummels. Nash equilibria in concurrent games with büchi objectives. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'11), Mumbai, India, pages 375-386, 2011. Google Scholar
  7. R. E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293-318, 1992. Google Scholar
  8. K. Chatterjee, T.A. Henzinger, and N. Piterman. Strategy logic. Information and Computation, 208(6):677-693, 2010. Google Scholar
  9. Edmund M. Clarke, Orna Grumberg, and David E. Long. Model checking and abstraction. ACM transactions on Programming Languages and Systems, 16(5):1512-1542, 1994. Google Scholar
  10. P. Cousot and R. Cousot. On abstraction in software verification. In Forteenth International Conference on Computer Aided Verification (CAV'02), volume 2404 of LNCS, pages 37-56. Springer, 2002. Google Scholar
  11. S. Demri, V. Goranko, and M. Lange. Temporal Logics in Computer Science: Finite State Systems, volume 58 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. Google Scholar
  12. B. Finkbeiner and S. Schewe. Coordination logic. In Anuj Dawar and Helmut Veith, editors, International Workshop on Computer Science Logic (CSL'10), volume 6247 of LNCS, pages 305-319. Springer, 2010. Google Scholar
  13. J. Gutierrez, P. Harrenstein, and M. Wooldridge. Expressiveness and complexity results for strategic reasoning. In Proceedings of the Twenty-Sixth Annual Conference on Concurrency Theory (CONCUR'15), volume 42 of Leibniz International Proceedings in Informatics (LIPIcs), pages 268-282, Madrid, Spain, 2015. Google Scholar
  14. J. Gutierrez, P. Harrenstein, and M. Wooldridge. Iterated Boolean games. Information and Computation, 242:53-79, 2015. Google Scholar
  15. J. Gutierrez, P. Harrenstein, and M. Wooldridge. Reasoning about equilibria in game-like concurrent systems. Annals of Pure and Applied Logic, 169(2):373-403, 2017. Google Scholar
  16. M. Hennessy and R. A. Connolly Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137-161, 1985. Google Scholar
  17. M. Maschler, E. Solan, and S. Zamir. Game Theory. Cambridge University Press, 2013. Google Scholar
  18. R. Milner. Communication and Concurrency. Prentice Hall, 1989. Google Scholar
  19. F. Mogavero, A. Murano, G. Perelli, and M. Y. Vardi. Reasoning about strategies: On the model-checking problem. ACM Transactions on Computational Logic, 15(4):1-47, 2014. Google Scholar
  20. F. Mogavero, A. Murano, G. Perelli, and M. Y. Vardi. Reasoning about Strategies: On the Satisfiability Problem. Logical Methods in Computer Science, 13(1:9), 2017. Google Scholar
  21. F. Mogavero, A. Murano, and M. Y. Vardi. Reasoning about strategies. In K. Lodaya and M. Mahajan, editors, Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'10), volume 8 of Leibniz International Proceedings in Informatics (LIPIcs), pages 133-144, 2010. Google Scholar
  22. M.J. Osborne and A. Rubinstein. A Course in Game Theory. MIT Press, 1994. Google Scholar
  23. M. Pauly. A modal logic for coalitional power in games. Journal of Logic and Computation, 12(1):149-166, 2002. Google Scholar
  24. M. Pauly and R. Parikh. Game logic - an overview. Studia Logica, 75(2):165-182, 2003. Google Scholar
  25. Davide Sangiorgi. On the origins of bisimulation and coinduction. ACM Transactions on Programming Languages and Systems, 31(4):111-151, 2009. Google Scholar
  26. J. F. A. K. van Benthem. Modal Correspondence Theory. PhD thesis, University of Amsterdam, 1976. Google Scholar
  27. J. F. A. K. van Benthem. Extensive games as process models. Journal of Logic, Language and Information, 11(3):289-313, 2002. Google Scholar
  28. M. Wooldridge, J. Gutierrez, P. Harrenstein, E. Marchioni, G. Perelli, and A. Toumi. Rational verification: From model checking to equilibrium checking. In D. Schuurmans and M. Wellman, editors, Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence (AAAI'16), pages 4184-4190, Phoenix, AZ, 2016. Google Scholar
  29. M.J. Wooldridge. Introduction to Multiagent Systems. John Wiley &Sons, 2001. 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