Krishnendu Chatterjee and Thomas A. Henzinger and Nir Piterman

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2007-78

May 31, 2007

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-78.pdf

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 handle nonzero-sum games in a convenient and simple way. We show that the one-alternation fragment of strategy logic, is strong enough to express Nash-equilibrium, secure-equilibria, as well as 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 non-elementary, for the simple fragment that is used above we show that complexity is polynomial in the size of the game graph and optimal in the formula (ranging between 2EXPTIME and polynomial depending on the exact formulas).

---

BibTeX citation:

@techreport{Chatterjee:EECS-2007-78,
    Author= {Chatterjee, Krishnendu and Henzinger, Thomas A. and Piterman, Nir},
    Title= {Strategy Logic},
    Year= {2007},
    Month= {May},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-78.html},
    Number= {UCB/EECS-2007-78},
    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 handle nonzero-sum games in a convenient and simple way. We show that the one-alternation fragment of strategy logic, is strong enough to express Nash-equilibrium, secure-equilibria, as well as 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 non-elementary, for the simple fragment that is used above we show that complexity is polynomial in the size of the game graph and optimal in the formula (ranging between 2EXPTIME and polynomial depending on the exact formulas).},
}

EndNote citation:

%0 Report
%A Chatterjee, Krishnendu 
%A Henzinger, Thomas A. 
%A Piterman, Nir 
%T Strategy Logic
%I EECS Department, University of California, Berkeley
%D 2007
%8 May 31
%@ UCB/EECS-2007-78
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-78.html
%F Chatterjee:EECS-2007-78