Linear Temporal Logic, Planning and Synthesis

In this project we showed how to compute infinte plans for LTL goals. Infinite plans are akin to the problem of control synteshis. Given an LTL formula, the tools developed encodes the LTL goal formula as Deterministic Buchi Automata states. The Automata is encoded along with the allowed transitions of the agent in the Planning Domain Description Language (PDDL). The problem becomes a fully observable non-deterministic planning problem (FOND) or a classical problem, depending on whether the environment can act non-deterministically.