Computing Infinite Plans for LTL Goals Using a Classical Planner
Fabio Patrizi, Nir lipovetzky, Giuseppe De Giacomo and Hector Geffner
Classical planning has been notably successful in the synthesis of finite plans to achieve final states where given propositional goals hold. In the last few years, classical planning has also been extended to incorporate temporal extended goals expressed in temporal logics such as LTL to impose restrictions on the states sequences generated by the finite plans as well. In this work, we take the next step and consider the computation of infinite plans for achieving arbitrary LTL goals. We show that also such infinite plans can be efficiently obtained by calling a classical planner over a classical planning encoding that represents and extends the composition of the planning domain and the Buchi automaton representing the LTL goal. This compilation scheme has been implemented and a wide range of experiments over many domains and goals are reported.