Planning with Linear Temporal Logic Goals: Two Translation Approaches

Finite Linear Temporal Logic (fLTL) is a compelling language for representing goals in automated planning. The main approach for planning with these goals is to translate them into (regular) final-state goals, which are the standard supported by all highly engineered planning systems. In this talk I will present two of these translation approaches. The first one, which is worst-case exponential, builds an non-deterministic finite-state automaton for the fLTL formula, while the second builds an alternating automaton. The automata are then encoded in a standard planning language. Our empirical evaluation suggests that both of these approaches have strengths and weaknesses.