Skip Navigation


Journal of Logic and Computation Advance Access originally published online on August 12, 2006
Journal of Logic and Computation 2006 16(6):765-787; doi:10.1093/logcom/exl009
This Article
Right arrow Full Text
Right arrow Full Text (PDF)
Right arrow All Versions of this Article:
16/6/765    most recent
exl009v1
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Similar articles in ISI Web of Science
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Walther, D.
Right arrow Articles by Wooldridge, M.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2006. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Original Articles

ATL Satisfiability is Indeed EXPTIME-complete

Dirk Walther

University of Liverpool, UK.

Carsten Lutz

TU Dresden, Germany. E-mail: lutz{at}tcs.inf.tu-dresden.de

Frank Wolter and Michael Wooldridge

University of Liverpool, UK. E-mail: frank{at}csc.liv.ac.uk; mjw{at}csc.liv.ac.uk

E-mail: dirk{at}csc.liv.ac.uk


  Abstract

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 article, 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 article, 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.


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer:
Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.