Linear Temporal Logic, Planning and Synthesis

02 Jun 2013
code IJCAI-11 code IJCAI-13 PDF IJCAI-11 PDF IJCAI-13

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.

AI Planning, Linear Temporal Logic (LTL) Synthesis Verification
Avatar
Associate Professor in Artificial Intelligence

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

Related