Reasoning about equilibria in game-like concurrent systems. (English) Zbl 1400.03057

The main purpose of this paper is to design a logical framework for reasoning about equilibria in multi-agent games. The arenas of such games are simple labelled graphs such that the games are of infinite duration and the players’ goals are considered to be temporal, i.e. expressible as formulas of some temporal logic. The authors then present a logic that syntactically extends the temporal branching-time logic CTL\(^*\) with a new kind of quantification which is to be read as “on all paths obtained as the outcome of a (Nash) equilibrium strategy profile”.
The main technical result of this paper is the classification of the computational complexity of the model checking problem for this logic which is in fact rather a family of logics, parametrised by the way that outcomes are specified in the underlying games and possibly by restrictions on the use of the equilibrium quantifiers. The general result portrays the model checking as quite difficult, namely hard for doubly exponential time, in very simple cases already.
The paper is very much written in an overview style. Focus is given to the motivation of this framework through various examples, as well as first results on the computational problems that naturally come with the introduction of a formal logic. Proof details are hardly given; instead this paper links to other papers from which techniques are taken or where similarities can be discovered. It also points out various aspects that have yet to be uncovered, resp. problems on such logics that have yet to be solved like general upper bounds for instance.


03B70 Logic in computer science
03B44 Temporal logic
91A40 Other game-theoretic models
68T27 Logic in artificial intelligence
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI


[1] Abramsky, S., Semantics of interaction: an introduction to game semantics, Newton Institute Publications, (1996), Cambridge University
[2] Alur, R.; Henzinger, T. A., Reactive modules, Form. Methods Syst. Des., 15, 1, 7-48, (1999)
[3] Alur, R.; Henzinger, T. A.; Kupferman, O., Alternating-time temporal logic, J. ACM, 49, 5, 672-713, (2002) · Zbl 1326.68181
[4] Alur, R.; Henzinger, T. A.; Mang, F. Y.C.; Qadeer, S.; Rajamani, S. K.; Tasiran, S., MOCHA: modularity in model checking, (CAV, LNCS, vol. 1427, (1998), Springer), 521-525
[5] Alur, R.; La Torre, S.; Madhusudan, P., Playing games with boxes and diamonds, (CONCUR, LNCS, vol. 2761, (2003), Springer), 127-141 · Zbl 1274.68173
[6] Browne, M. C.; Clarke, E. M.; Grumberg, O., Characterizing finite Kripke structures in propositional temporal logic, Theoret. Comput. Sci., 59, 115-131, (1988) · Zbl 0677.03011
[7] Chatterjee, K.; Henzinger, T. A.; Piterman, N., Strategy logic, Inform. and Comput., 208, 6, 677-693, (2010) · Zbl 1205.68197
[8] Chen, T.; Forejt, V.; Kwiatkowska, M. Z.; Parker, D.; Simaitis, A., PRISM-games: a model checker for stochastic multi-player games, (TACAS, LNCS, vol. 7795, (2013), Springer), 185-191 · Zbl 1381.68151
[9] Clarke, E. M.; Emerson, E. A., Design and synthesis of synchronization skeletons using branching time temporal logic, (Logics of Programs, LNCS, vol. 131, (1981), Springer-Verlag Berlin, Germany), 52-71
[10] Clarke, E. M.; Grumberg, O.; Peled, D. A., Model checking, (2000), The MIT Press Cambridge, MA
[11] Daskalakis, C.; Goldberg, P. W.; Papadimitriou, C. H., The complexity of computing a Nash equilibrium, (STOC, Seattle, WA, (2006)) · Zbl 1301.68142
[12] Ehlers, R.; Lafortune, S.; Tripakis, S.; Vardi, M., Reactive synthesis vs. supervisory control: bridging the gap, (2013), EECS Department, University of California Berkeley, Tech. Rep. UCB/EECS-2013-162
[13] Emerson, E. A., Temporal and modal logic, (Handbook of Theoretical Computer Science Volume B: Formal Models and Semantics, (1990), Elsevier Science Publishers B.V. Amsterdam), 996-1072 · Zbl 0900.03030
[14] Emerson, E. A.; Halpern, J. Y., ‘sometimes’ and ‘not never’ revisited: on branching time versus linear time temporal logic, J. ACM, 33, 1, 151-178, (1986) · Zbl 0629.68020
[15] Emerson, E. A.; Halpern, J. Y., Decision procedures and expressiveness in the temporal logic of branching time, J. Comput. System Sci., 30, 1, 1-24, (1985) · Zbl 0559.68051
[16] Emerson, E. A.; Jutla, C. S., The complexity of tree automata and logics of programs (extended abstract), (FOCS, (1988)), 328-337
[17] Esparza, J.; Heljanko, K., Unfoldings - A partial-order approach to model checking, Monogr. Theoret. Comput. Sci. EATCS Ser., (2008), Springer · Zbl 1153.68035
[18] (Gabbay, D.; Gärdenfords, P.; Siekmann, J.; Benthem, J. V.; Vardi, M.; Woods, J., Handbook of Modal Logic, vol. 3, (2007), Elsevier)
[19] Ghica, D. R., Applications of game semantics: from program analysis to hardware synthesis, (LICS, (2009), IEEE Computer Society), 17-26
[20] Gutierrez, J.; Harrenstein, P.; Wooldridge, M., Iterated Boolean games, (IJCAI, (2013), IJCAI/AAAI)
[21] Gutierrez, J.; Harrenstein, P.; Wooldridge, M., Reasoning about equilibria in game-like concurrent systems, (KR, (2014), AAAI)
[22] Gutierrez, J.; Harrenstein, P.; Wooldridge, M., Expressiveness and complexity results for strategic reasoning, (CONCUR, LIPIcs, vol. 42, (2015), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik), 268-282 · Zbl 1374.68332
[23] Gutierrez, J.; Harrenstein, P.; Wooldridge, M., Iterated Boolean games, Inform. and Comput., 242, 53-79, (2015) · Zbl 1318.91012
[24] Habermehl, P., On the complexity of the linear-time mu-calculus for Petri-nets, (ICATPN, LNCS, vol. 1248, (1997), Springer), 102-116
[25] Harrenstein, P.; van der Hoek, W.; Meyer, J. J.; Witteveen, C., Boolean games, (Theoretical Aspects of Rationality and Knowledge, TARK VIII, (2001)), 287-298
[26] Hyland, M., Game semantics, Newton Institute Publications, (1997), Cambridge University · Zbl 0919.68084
[27] Kozen, D., Lower bounds for natural proof systems, (FOCS, (1977), IEEE Computer Society), 254-266
[28] Kozen, D., Results on the propositional mu-calculus, Theoret. Comput. Sci., 27, 333-354, (1983) · Zbl 0553.03007
[29] Kupferman, O., Recent challenges and ideas in temporal synthesis, (SOFSEM, LNCS, vol. 7147, (2012), Springer), 88-98
[30] Kupferman, O.; Madhusudan, P.; Thiagarajan, P. S.; Vardi, M. Y., Open systems in reactive environments: control and synthesis, (CONCUR, LNCS, vol. 1877, (2000), Springer), 92-107 · Zbl 0999.68124
[31] Kupferman, O.; Vardi, M. Y., Memoryful branching-time logic, (LICS, (2006), IEEE Computer Society), 265-274
[32] Kupferman, O.; Vardi, M. Y.; Wolper, P., An automata-theoretic approach to branching time model checking, J. ACM, 47, 2, 312-360, (2000) · Zbl 1133.68376
[33] Laroussinie, F.; Markey, N.; Schnoebelen, P., Temporal logic with forgettable past, (LICS, (2002), IEEE Computer Society), 383-392
[34] Lomuscio, A.; Qu, H.; Raimondi, F., MCMAS: a model checker for the verification of multi-agent systems, (CAV, LNCS, vol. 5643, (2009), Springer), 682-688
[35] MacLane, S., Categories for the working Mathematician, (1998), Springer
[36] Mogavero, F.; Murano, A.; Perelli, G.; Vardi, M. Y., What makes ATL^{⁎} decidable? A decidable fragment of strategy logic, (CONCUR, LNCS, vol. 7454, (2012), Springer), 193-208 · Zbl 1365.68329
[37] Mogavero, F.; Murano, A.; Sauro, L., On the boundary of behavioral strategies, (LICS, (2013), IEEE Computer Society), 263-272 · Zbl 1367.68290
[38] Mogavero, F.; Murano, A.; Vardi, M. Y., Reasoning about strategies, (FSTTCS, LIPIcs, vol. 8, (2010), Schloss Dagstuhl), 133-144 · Zbl 1245.68138
[39] Mogavero, F.; Murano, A.; Vardi, M. Y., Relentful strategic reasoning in alternating-time temporal logic, (LPAR, LNCS, vol. 6355, (2010), Springer), 371-386 · Zbl 1310.68144
[40] Mohalik, S.; Walukiewicz, I., Distributed games, (FSTTCS, LNCS, vol. 2914, (2003), Springer), 338-351 · Zbl 1205.68089
[41] Nielsen, M.; Winskel, G., Models for concurrency, (Handbook of Logic in Computer Science, (1995), Oxford University Press), 1-148
[42] (Nisan, N.; Rougarden, T.; Tardos, E.; Vazirani, V. V., Algorithmic Game Theory, (2007), Cambridge University Press)
[43] Osborne, M. J.; Rubinstein, A., A course in game theory, (1994), The MIT Press Cambridge, MA · Zbl 1194.91003
[44] Parikh, R., The logic of games and its applications, (Topics in the Theory of Computation, (1985), Elsevier) · Zbl 0552.90110
[45] Pnueli, A., The temporal logic of programs, (FOCS, (1977), IEEE), 46-57
[46] Pnueli, A.; Rosner, R., On the synthesis of a reactive module, (POPL, (1989), ACM Press), 179-190
[47] Sistla, A. P.; Clarke, E. M., The complexity of propositional linear temporal logics, J. ACM, 32, 3, 733-749, (1985) · Zbl 0632.68034
[48] Toumi, A.; Gutierrez, J.; Wooldridge, M., A tool for the automated verification of Nash equilibria in concurrent games, (ICTAC, LNCS, (2015), Springer), 583-594 · Zbl 1471.68157
[49] Ummels, M.; Wojtczak, D., The complexity of Nash equilibria in limit-average games, (CONCUR, LNCS, vol. 6901, (2011), Springer), 482-496 · Zbl 1343.68177
[50] Ummels, M.; Wojtczak, D., The complexity of Nash equilibria in stochastic multiplayer games, Log. Methods Comput. Sci., 7, 3, (2011) · Zbl 1238.91025
[51] Vardi, M. Y., A temporal fixpoint calculus, (POPL, (1988), ACM Press), 250-259
[52] Walukiewicz, I., A landscape with games in the background, (LICS, (2004), IEEE Computer Society), 356-366
[53] Wooldridge, M.; Gutierrez, J.; Harrenstein, P.; Marchioni, E.; Perelli, G.; Toumi, A., Rational verification: from model checking to equilibrium checking, (AAAI, (2016), AAAI), 4184-4190
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.