FOND Planning for Pure-Past Linear Temporal Logic Goals.

Recently, Pure-Past Temporal Logic (PPLTL) has been shown to be very effective for specifying temporally extended goals in deterministic planning domains. In this paper, we show its effectiveness also for FOND planning, both for strong and strong-cyclic plans. We present a notably simple encoding of FOND planning for PPLTL goals into standard FOND planning for reachability goals.  The encoding only introduces few fluents (at most linear in the PPLTL goal) without adding any spurious action and allows planners to lazily build the relevant part of the DFA for the goal formula on-the-fly during the search. We formally prove its correctness, implement it in a tool called Plan4Past, and experimentally show its practical effectiveness.