Planning for Temporally Extended Goals in Pure-Past Linear Temporal Logic: A Polynomial Reduction to Standard Planning

TL;DR

This paper introduces a polynomial translation method that enables existing planning tools to handle complex temporally extended goals expressed in Pure-Past LTL, bridging the gap between theory and practical application.

Contribution

The authors develop a polynomial translation technique from PPLTL planning problems to standard planning, allowing existing tools to efficiently handle complex temporal goals.

Findings

Translation is formally correct and computationally efficient.

Practical experiments show seamless integration with existing planning tools.

Handling PPLTL goals does not degrade the performance of state-of-the-art planners.

Abstract

We study temporally extended goals expressed in Pure-Past LTL (PPLTL). PPLTL is particularly interesting for expressing goals since it allows to express sophisticated tasks as in the Formal Methods literature, while the worst-case computational complexity of Planning in both deterministic and nondeterministic domains (FOND) remains the same as for classical reachability goals. However, while the theory of planning for PPLTL goals is well understood, practical tools have not been specifically investigated. In this paper, we make a significant leap forward in the construction of actual tools to handle PPLTL goals. We devise a technique to polynomially translate planning for PPLTL goals into standard planning. We show the formal correctness of the translation, its complexity, and its practical effectiveness through some comparative experiments. As a result, our translation enables state-of-the-art tools, such as FD or MyND, to handle PPLTL goals seamlessly, maintaining the impressive performances they have for classical reachability goals.