*Krishnendu Chatterjee,
Thomas A. Henzinger,
and Nir Piterman*

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).

*Proceedings of the
18th International Conference on Concurrency Theory*
(CONCUR),
Lecture Notes in Computer Science 4703,
Springer, 2007, pp. 59-73.

Download inofficial, sometimes updated PostScript / PDF document. © 2007 Springer.