Abstract
Classical planning has been notably successful in synthesizing ?nite plans to achieve states where propositional goals hold. In the last few years, classical planning has also been extended to incorporate temporally extended goals, expressed in temporal logics such as LTL, to impose restrictions on the state sequences generated by ?nite plans. In this work, we take the next step and consider the computation of in?nite plans for achieving arbitrary LTL goals. We show that in?nite plans can also be obtained ef?ciently by calling a classical planner once over a classical planning encoding that represents and extends the composition of the planning domain and the Bu?chi automaton representing the goal. This compilation scheme has been implemented and a number of experiments are reported.