loading...
Satisfiability in Alternating-time Temporal Logic
Ottawa, Canada June 22-June 25
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2003.121006018th Annual IEEE Symposium on Logic i ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Govert van Drimmelen, Rand Afrikaans University
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.
Citation:
Govert van Drimmelen, "Satisfiability in Alternating-time Temporal Logic," lics, pp.208, 18th Annual IEEE Symposium on Logic in Computer Science (LICS'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.