Bounded Timed Propositional Temporal Logic with Past
Captures Timeline-based Planning with Bounded Constraints
Abstract
Within the timeline-based framework, planning
problems are modeled as sets of independent,
but interacting, components whose behavior over
time is described by a set of temporal constraints.
Timeline-based planning is being used successfully
in a number of complex tasks, but its theoretical
properties are not so well studied. In particular,
while it is known that Linear Temporal Logic (LTL)
can capture classical action-based planning, a similar logical characterization was not available for
timeline-based planning formalisms. This paper
shows that timeline-based planning with bounded
temporal constraints can be captured by a bounded
version of Timed Propositional Temporal Logic,
augmented with past operators, which is an extension of LTL originally designed for the verification
of real-time systems. As a byproduct, we get that
the proposed logic is expressive enough to capture
temporal action-based planning problems