Abstract
We introduce strategy logic, a logic that treats strategies in two-player games as explicit first-order objects. The explicit treatment of strategies allows us to specify properties of nonzero-sum games in a simple and natural way. We show that the one-alternation fragment of strategy logic is strong enough to express the existence of Nash equilibria and secure equilibria, and subsumes other logics that were introduced to reason about games, such as ATL, ATL *, and game logic. We show that strategy logic is decidable, by constructing tree automata that recognize sets of strategies. While for the general logic, our decision procedure is nonelementary, for the simple fragment that is used above we show that the complexity is polynomial in the size of the game graph and optimal in the size of the formula (ranging from polynomial to 2EXPTIME depending on the form of the formula).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable concurrent program specifications. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) Automata, Languages and Programming. LNCS, vol. 372, pp. 1–17. Springer, Heidelberg (1989)
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM 49, 672–713 (2002)
Blass, A., Gurevich, Y., Nachmanson, L., Veanes, M.: Play to test. In: Grieskamp, W., Weise, C. (eds.) FATES 2005. LNCS, vol. 3997, pp. 32–46. Springer, Heidelberg (2006)
Chatterjee, K., Henzinger, T.A.: Assume guarantee synthesis. In: 30th TACAS. LNCS, vol. 4424, pp. 261–275. Springer, Heidelberg (2007)
Chatterjee, K., Henzinger, T.A., Jurdziński, M.: Games with secure equilibria. In: 19th LICS, pp. 160–169. IEEE Computer Society Press, Los Alamitos (2004)
Chatterjee, K., Henzinger, T.A., Piterman, N.: Strategy logic. Technical Report UCB/EECS-2007-78, UC Berkeley (2007)
de Alfaro, L., Henzinger, T.A.: Interface automata. In: 9th FASE, pp. 109–120. ACM Press, New York (2001)
Dill, D.L.: Trace theory for automatic hierarchical verification of speed independent circuits. MIT Press, Cambridge (1989)
Emerson, E.A., Jutla, C., Sistla, A.P.: On model-checking for fragments of μ-calculus. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 385–396. Springer, Heidelberg (1993)
Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: 7th POPL, pp. 163–173. ACM Press, New York (1980)
Henzinger, T.A., Kupferman, O., Rajamani, S.: Fair simulation. Information and Computation 173(1), 64–81 (2002)
Kaiser, L.: Game quantification on automatic structures and hierarchical model checking games. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 411–425. Springer, Heidelberg (2006)
Nash Jr., J.F.: Equilibrium points in n-person games. Proceedings of the National Academy of Sciences 36, 48–49 (1950)
Jurdziński, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000)
Kamp, J.A.W.: Tense Logic and the Theory of Order. PhD thesis, UCLA (1968)
Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)
Kupferman, O., Vardi, M.Y., Wolper, P.: Module checking. Information and Computation 164, 322–344 (2001)
Martin, D.A.: Borel determinacy. Annals of Mathematics 65, 363–371 (1975)
Milner, R.: An algebraic definition of simulation between programs. In: 2nd IJCAI, pp. 481–489. British Computer Society (1971)
Muller, D.E., Schupp, P.E.: Alternating automata on infinite trees. Theoretical Computer Science 54, 267–276 (1987)
Owen, G.: Game Theory. Academic Press, London (1995)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: 16th POPL, pp. 179–190. ACM Press, New York (1989)
Rabin, M.O.: Decidability of second order theories and automata on infinite trees. Transaction of the AMS 141, 1–35 (1969)
Ramadge, P.J.G., Wonham, W.M.: The control of discrete event systems. IEEE Transactions on Control Theory 77, 81–98 (1989)
Thomas, W.: On the synthesis of strategies in infinite games. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 1–13. Springer, Heidelberg (1995)
Thomas, W.: Languages, automata, and logic. In: Handbook of Formal Languages, ch. 7. Beyond Words, vol. 3, pp. 389–455. Springer, Heidelberg (1997)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chatterjee, K., Henzinger, T.A., Piterman, N. (2007). Strategy Logic. In: Caires, L., Vasconcelos, V.T. (eds) CONCUR 2007 – Concurrency Theory. CONCUR 2007. Lecture Notes in Computer Science, vol 4703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74407-8_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-74407-8_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74406-1
Online ISBN: 978-3-540-74407-8
eBook Packages: Computer ScienceComputer Science (R0)