The Planning Spectrum - One, Two, Three, Infinity
M. Pistore, M. Y. Vardi

TL;DR
This paper introduces a new logical language for planning in nondeterministic systems, allowing flexible combinations of universal and existential path quantifiers, and provides an automata-based planning algorithm.
Contribution
It defines a novel language with combined path quantifiers for LTL in planning, expanding beyond traditional universal and existential interpretations.
Findings
Identifies eight relevant quantifier combinations for the new language.
Develops an automata-theoretic planning algorithm for the language.
Analyzes the complexity of the planning approach.
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
