ATL is Indeed ExpTime-complete

D. WaltherD. Walther, Carsten LutzCarsten Lutz, Frank WolterFrank Wolter, M. WooldridgeM. Wooldridge

Download

D. Walther, Carsten Lutz, Frank Wolter, M. Wooldridge
ATL is Indeed ExpTime-complete
Journal of Logic and Computation, 16(6):765-787, 2006

Details
Bibtex

KurzfassungAbstract
The Alternating-time Temporal Logic (ATL) of Alur, Henzinger, and Kupferman is being increasingly widely applied in the specification and verification of open distributed systems and game-like multi-agent systems. In this paper, we investigate the computational complexity of the satisfiability problem for ATL. For the case where the set of agents is fixed in advance, this problem was settled at ExpTime-complete in a result of van Drimmelen. If the set of agents is not fixed in advance, then van Drimmelen's construction yields a 2ExpTime upper bound. In this paper, we focus on the latter case and define three natural variations of the satisfiability problem. Although none of these variations fixes the set of agents in advance, we are able to prove containment in ExpTime for all of them by means of a type elimination construction-thus improving the existing 2ExpTime upper bound to a tight ExpTime one.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@article{ WaLuWoWo-06b,
  author = {D. {Walther} and C. {Lutz} and F. {Wolter} and M. {Wooldridge}},
  journal = {Journal of Logic and Computation},
  number = {6},
  pages = {765--787},
  title = {{ATL} is Indeed {\sc ExpTime}-complete},
  volume = {16},
  year = {2006},
}