Citation
Krishnendu Chatterjee, Tom Henzinger, Nir Piterman. "Strategy Logic". Technical report, University of California, Berkeley, UCB/EECS-2007-78, May, 2007.

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

Electronic downloads

• http://www.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-78.html

• HTML

  Krishnendu Chatterjee, Tom Henzinger, Nir Piterman. <a
  href="http://chess.eecs.berkeley.edu/pubs/312.html"
  ><i>Strategy Logic</i></a>, Technical
  report,  University of California, Berkeley,
  UCB/EECS-2007-78, May, 2007.

• Plain text

  Krishnendu Chatterjee, Tom Henzinger, Nir Piterman.
  "Strategy Logic". Technical report,  University of
  California, Berkeley, UCB/EECS-2007-78, May, 2007.

• BibTeX

  @techreport{ChatterjeeHenzingerPiterman07_StrategyLogic,
      author = {Krishnendu Chatterjee and Tom Henzinger and Nir
                Piterman},
      title = {Strategy Logic},
      institution = {University of California, Berkeley},
      number = {UCB/EECS-2007-78},
      month = {May},
      year = {2007},
      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).},
      URL = {http://chess.eecs.berkeley.edu/pubs/312.html}
  }
  

Posted by Christopher Brooks on 7 Jun 2007.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.