Planning for Temporally Extended Goals in Pure-Past Linear Temporal Logic: A Polynomial Reduction to Standard Planning
This work addresses the gap between theoretical understanding and practical implementation of planning for complex temporal goals in AI, providing a tool for researchers and practitioners in automated planning.
The paper tackles the problem of planning for temporally extended goals expressed in Pure-Past Linear Temporal Logic (PPLTL) by developing a polynomial reduction to standard planning, enabling state-of-the-art tools like FD or MyND to handle these goals seamlessly while maintaining performance comparable to classical reachability goals.
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.