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 emph{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.
