Nash equilibrium and bisimulation invariance. (English) Zbl 1442.68142

Summary: 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 setting involves computing the set of (Nash) equilibria in the concurrent game. However, we show that, with respect to the above model of strategies (arguably, the “standard” model in the computer science 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 logic formulae, may nevertheless have fundamentally different properties (solutions) from a game theoretic perspective. Our aim in this paper is to explore the issues raised by this discovery. After illustrating the issue by way of a motivating example, we present three models of strategies with respect to which the existence of Nash equilibria is preserved under bisimilarity. We 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 computer science literature.


68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B70 Logic in computer science
68T42 Agent technology and artificial intelligence
91A10 Noncooperative games
Full Text: DOI arXiv


[1] [AH99]Rajeev Alur and Thomas A. Henzinger. Reactive modules. Formal Methods in System Design, 15(1):7-48, 1999.
[2] [AHK02]R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-Time Temporal Logic. Journal of the ACM, 49(5):672-713, 2002. · Zbl 1326.68181
[3] [AHKV98] Rajeev Alur, Thomas A. Henzinger, Orna Kupferman, and Moshe Y. Vardi. Alternating refinement relations. In CONCUR, volume 1466 of LNCS, pages 163-178. Springer, 1998. · Zbl 1070.68524
[4] [AHM+98] Rajeev Alur, Thomas A. Henzinger, Freddy Y. C. Mang, Shaz Qadeer, Sriram K. Rajamani, and Serdar Tasiran. MOCHA: modularity in model checking. In CAV, volume 1427 of LNCS, pages 521-525. Springer, 1998.
[5] [BBMU11] P. Bouyer, R. Brenguier, Nicolas Markey, and M. Ummels. Nash equilibria in concurrent games with B¨uchi objectives. In S. Chakraborty and A. Kumar, editors, 31st International Conference · Zbl 1246.68122
[6] [BBMU15] P. Bouyer, R. Brenguier, Nicolas Markey, and M. Ummels. Pure Nash equilibria in concurrent deterministic games. Logical Methods in Computer Science, 11(2:9):1-72, 2015. · Zbl 1320.91010
[7] [BK08]C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.
[8] [Bre13]Romain Brenguier. PRALINE: A tool for computing nash equilibria in concurrent games. In CAV, volume 8044 of LNCS, pages 890-895. Springer, 2013.
[9] [Bry92]Randal E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv., 24(3):293-318, 1992.
[10] [CC02]Patrick Cousot and Radhia Cousot. On abstraction in software verification. In CAV, volume 2404 of LNCS, pages 37-56. Springer, 2002. · Zbl 1010.68506
[11] [CE81]Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logics of Programs, volume 131 of LNCS, pages 52-71. Springer, 1981.
[12] [CGL94]Edmund M. Clarke, Orna Grumberg, and David E. Long. Model checking and abstraction. ACM Trans. Program. Lang. Syst., 16(5):1512-1542, 1994.
[13] [CGP02]E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. MIT Press, 2002.
[14] [CHP10]Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Strategy logic. Inf. Comput., 208(6):677-693, 2010. · Zbl 1205.68197
[15] [CLMM14] Petr Cerm´ak, Alessio Lomuscio, Fabio Mogavero, and Aniello Murano. MCMAS-SLK: A model checker for the verification of strategy logic specifications. In CAV, volume 8559 of LNCS, pages 525-532. Springer, 2014.
[16] [DGL16]S. Demri, V. Goranko, and M. Lange. Temporal Logics in Computer Science, volume 58 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016.
[17] [DV95]R. De Nicola and F. W. Vaandrager. Three logics for branching bisimulation. Journal of the ACM, 42(2):458-487, 1995. · Zbl 0886.68064
[18] [FKL10]Dana Fisman, Orna Kupferman, and Yoad Lustig. Rational synthesis. In TACAS, volume 6015 of LNCS, pages 190-204. Springer, 2010. · Zbl 1284.68396
[19] [FS10]Bernd Finkbeiner and Sven Schewe. Coordination logic. In Anuj Dawar and Helmut Veith, editors, CSL, volume 6247 of LNCS, pages 305-319. Springer, 2010. · Zbl 1287.03070
[20] [GHPW17] Julian Gutierrez, Paul Harrenstein, Giuseppe Perelli, and Michael Wooldridge. Nash equilibrium and bisimulation invariance. In CONCUR, volume 85 of LIPIcs, pages 17:1-17:16. Schloss Dagstuhl, 2017.
[21] [GHW15a] Julian Gutierrez, Paul Harrenstein, and Michael Wooldridge. Expresiveness and complexity results for strategic reasoning. In CONCUR, volume 42 of LIPIcs, pages 268-282. Schloss Dagstuhl, 2015. · Zbl 1374.68332
[22] [GHW15b] Julian Gutierrez, Paul Harrenstein, and Michael Wooldridge. Iterated Boolean games. Inf. Comput., 242:53-79, 2015. · Zbl 1318.91012
[23] [GHW17a] Julian Gutierrez, Paul Harrenstein, and Michael Wooldridge. From model checking to equilibrium checking: Reactive modules for rational verification. Artificial Intelligence, 248:123-157, 2017. · Zbl 1420.68129
[24] [GHW17b] Julian Gutierrez, Paul Harrenstein, and Michael Wooldridge. Reasoning about equilibria in game-like concurrent systems. Ann. Pure Appl. Logic, 168(2):373-403, 2017. · Zbl 1400.03057
[25] [GNPW18] Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, and Michael Wooldridge. EVE: A tool for temporal equilibrium analysis. In ATVA, LNCS. Springer, 2018.
[26] [GW14]Julian Gutierrez and Michael Wooldridge. Equilibria of concurrent games on event structures. In CSL-LICS, pages 46:1-46:10. ACM, 2014. · Zbl 1401.68228
[27] [HM85]Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. J. ACM, 32(1):137-161, 1985. · Zbl 0629.68021
[28] [KNP11]Marta Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic real-time systems. In CAV, volume 6806 of LNCS, pages 585-591. Springer, 2011.
[29] [Koz83]Dexter Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333- 354, 1983. · Zbl 0553.03007
[30] [KPW16]Marta Kwiatkowska, David Parker, and Clemens Wiltsche. Prism-games 2.0: A tool for multiobjective strategy synthesis for stochastic games. In TACAS, volume 9636 of LNCS, pages 560-566. Springer, 2016.
[31] [Mil80]R. Milner. A Calculus of Communicating Systems, volume 92 of LNCS. Springer, 1980.
[32] [Mil89]R. Milner. Communication and Concurrency. Prentice Hall, 1989.
[33] [MMPV16] F. Mogavero, A. Murano, G. Perelli, and M. Y. Vardi. Reasoning about Strategies: on the Satisfiability Problem. CoRR, abs/1611.08541, 2016. · Zbl 1448.68312
[34] [MSZ13]M. Maschler, E. Solan, and S. Zamir. Game Theory. Cambridge University Press, 2013. · Zbl 1403.91003
[35] [OR94]M.J. Osborne and A. Rubinstein. A Course in Game Theory. MIT Press, 1994. · Zbl 1194.91003
[36] [Pau02]Marc Pauly. A modal logic for coalitional power in games. J. Log. Comput., 12(1):149-166, 2002. · Zbl 1003.91006
[37] [Pnu77]Amir Pnueli. The temporal logic of programs. In FOBS, pages 46-57. IEEE Computer Society, 1977.
[38] [PP03]Marc Pauly and Rohit Parikh. Game logic—an overview. Studia Logica, 75(2):165-182, 2003. · Zbl 1040.03013
[39] [San09]Davide Sangiorgi. On the origins of bisimulation and coinduction. ACM Trans. Program. Lang. Syst., 31(4), 2009. · Zbl 1285.68112
[40] [SR12]Davide Sangiorgi and Jan Rutten, editors. Advanced Topics in Bisimulation and Coinduction, volume 52 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2012.
[41] [TGW15]Alexis Toumi, Julian Gutierrez, and Michael Wooldridge. A tool for the automated verification of nash equilibria in concurrent games. In ICTAC, volume 9399 of LNCS, pages 583-594. Springer, 2015. · Zbl 1471.68157
[42] [van76]J. van Benthem. Modal Correspondence Theory. PhD thesis, University of Amsterdam, 1976.
[43] [vB02]Johan van Benthem. Extensive games as process models. Journal of Logic, Language and Information, 11(3):289-313, 2002. · Zbl 1003.03530
[44] [vdHLW06] Wiebe van der Hoek, Alessio Lomuscio, and Michael Wooldridge. On the complexity of practical ATL model checking. In AAMAS, pages 201-208. ACM, 2006.
[45] [vGW96]R: J. van Glabbeek and W. P. Weijland. Branching time and abstraction in bisimulation semantics. Journal of the ACM, 43(3):555-600, 1996. · Zbl 0882.68085
[46] [WGH+16] Michael Wooldridge, Julian Gutierrez, Paul Harrenstein, Enrico Marchioni, Giuseppe Perelli, and Alexis Toumi. Rational verification: From model checking to equilibrium checking. In AAAI, pages 4184-4191. AAAI Press, 2016.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.