Logic in Computer Science (LICS 2003)

Paper: Satisfiability in Alternating-time Temporal Logic (at LICS 2003)

Authors: Govert van Drimmelen

Abstract

Alternating-time Temporal Logic (ATL) is a branching-time temporal logic that naturally describes computations of multi-agent distributed systems and multi-player games. In particular, ATL explicitly allows for the expression of coalitional ability in such situations. We present an automata-based decision procedure for ATL, by translating the satisfiability problem for ATL to the nonemptiness problem for alternating automata on infinite trees. The key result that enables this translation is a bounded-branching tree model theorem for ATL, proving that a satisfiable formula is also satisfiable in a tree model of bounded branching degree. It follows that ATL is decidable in exponential time, which is also the optimal complexity: satisfiability in CTL, a fragment of ATL, is EXPTIME-complete. The paper thus answers a fundamental logical question about ATL and provides an example of how alternation in automata may elegantly express game-like transitions.

BibTeX

  @InProceedings{vanDrimmelen-SatisfiabilityinAlt,
    author = 	 {Govert van Drimmelen},
    title = 	 {Satisfiability in Alternating-time Temporal Logic},
    booktitle =  {Proceedings of the Eighteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2003},
    year =	 2003,
    editor =	 {Phokion G. Kolaitis},
    month =	 {June}, 
    pages =      {208--217},
    location =   {Ottawa, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }