The Planning Spectrum - One, Two, Three, Infinity
  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
f, which are the paths that are required to satisfy the formula. Two extreme
cases are the universal interpretation A.f, which requires that the formula be
satisfied for all execution paths, and the existential interpretation E.f,
which requires that the formula be satisfied for some execution path.
  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 execution.
  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.f), or that there is some finite execution whose
extensions all satisfy an LTL formula (EA.f). 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)* and (EA)*). We also present a planning algorithm for
the new language that is based on an automata-theoretic approach, and study its
complexity.
