Bounded Timed Propositional Temporal Logic with Past Captures Timeline-based Planning with Bounded Constraints

Bounded Timed Propositional Temporal Logic with Past Captures Timeline-based Planning with Bounded Constraints

Dario Della Monica, Nicola Gigante, Angelo Montanari, Pietro Sala, Guido Sciavicco

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
Main track. Pages 1008-1014. https://doi.org/10.24963/ijcai.2017/140

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.
Keywords:
Knowledge Representation, Reasoning, and Logic: Geometric, Spatial, and Temporal Reasoning
Planning and Scheduling: Planning and Scheduling
Planning and Scheduling: Theoretical Foundations of Planning