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.

Nir Lipovetzky
Nir Lipovetzky
Senior Lecturer in Artificial Intelligence

My interests span across research areas in AI planning, search, learning, verification, constraint programming, operations research and intention recognition.