---
res:
bibo_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).@eng
bibo_authorlist:
- foaf_Person:
foaf_givenName: Krishnendu
foaf_name: Krishnendu Chatterjee
foaf_surname: Chatterjee
foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0002-4561-241X
- foaf_Person:
foaf_givenName: Thomas A
foaf_name: Thomas Henzinger
foaf_surname: Henzinger
foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
orcid: 0000−0002−2985−7724
- foaf_Person:
foaf_givenName: Nir
foaf_name: Piterman, Nir
foaf_surname: Piterman
bibo_doi: 10.1007/978-3-540-74407-8_5
bibo_volume: 4703
dct_date: 2007^xs_gYear
dct_publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik@
dct_title: Strategy logic@
...