Non-Deterministic Planning with Temporally Extended Goals: LTL over Finite and Infinite Traces

Abstract

Temporally extended goals are critical to the specification of a diversity of real-world planning problems. Here we examine the problem of non-deterministic planning with temporally extended goals specified in linear temporal logic (LTL), interpreted over either finite or infinite traces. Unlike existing [IL planners, we place no restrictions on our [IL formulae beyond those necessary to distinguish finite from infinite interpretations. We generate plans by compiling [IL temporally extended goals into problem instances described in the Planning Domain Definition Language that are solved by a state-of-the-art fully observable non-deterministic planner. We propose several different compilations based on translations of [IL to alternating or non-deterministic (Buchi) automata, and evaluate various properties of the competing approaches. We address a diverse spectrum of [IL planning problems that, to this point, had not been solvable using AI planning techniques, and do so in a manner that demonstrates highly competitive performance.