loading...
The Planning Spectrum - One, Two, Three, Infinity
Ottawa, Canada June 22-June 25
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2003.121006318th 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 
   
Marco Pistore, University of Trento
Moshe Y. Vardi, Rice University
Linear Temporal Logic (LTL) is widely used for defining conditions on the execution paths of dynamic systems. In the case of dynamic systems that allow for nondeterministic evolutions, one has to specify, along with an LTL formula \varphi, which are the paths that are required to satisfy the formula. Two extreme cases are the universal interpretation A.\varphi, which requires to satisfy the formula for all the possible execution paths, and the existential interpretation E.\varphi, which requires to satisfy the formula for some execution paths. When LTL is applied to the definition of goals in planning problems on nondeterministic domains, these two extreme cases are too restrictive. It is often impossible to develop plans that achieve the goal in all the nondeterministic evolutions of a system, and it is too weak to require that the goal is satisfied by some executions. In this paper we explore alternative interpretations of an LTL formula that are between these extreme cases. We define a new language that permits an arbitrary combination of the A and E quantifiers, thus allowing, for instance, to require that each finite execution can be extended to an execution satisfying an LTL formula (AE.\varphi), or that there is some finite execution whose extensions all satisfy an LTL formula (EA.\varphi). We show that only eight of these combinations of path quantifiers are relevant, corresponding to an alternation of the quantifiers of length one (A and E), two (AE and EA), three (AEA and EAE), and infinity ((AE)\omega and (EA)\omega). We also presents a planning algorithm for the new language, that is based on an automata-theoretic approach, and studies its complexity.
Citation:
Marco Pistore, Moshe Y. Vardi, "The Planning Spectrum - One, Two, Three, Infinity," lics, pp.234, 18th Annual IEEE Symposium on Logic in Computer Science (LICS'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.