Planning for temporally extended goals in pure-past linear temporal logic

We study planning for temporally extended goals expressed in Pure-Past Linear Temporal Logic (PPLTL) in the context of deterministic (i.e., classical) and fully observable nondeterministic (FOND) domains. PPLTL is the variant of Linear-time Temporal Logic on finite traces (LTLf) that refers to the past rather than the future. Although PPLTL is as expressive as LTLf, we show that it is computationally much more effective for planning. In particular, we show that checking the validity of a plan for a PPLTL formula is Markovian. This is achieved by introducing a linear number of additional propositional variables that capture the validity of the entire formula in a modular fashion. The solution encoding introduces only a linear number of new fluents proportional to the size of the PPLTL goal and does not require any additional spurious action. We implement our solution technique in a system called Plan4Past, which can be used alongside state-of-the-art classical and FOND planners. Our empirical analysis demonstrates the practical effectiveness of Plan4Past in both classical and FOND problems, showing that the resulting planner performs overall better than other planning approaches for LTLf goals.