LTLf to PDDL

This web site shows the work done for the fulfillment of the "Reasoning Robots" module of the exam "Elective in Artificial Intelligence" at Università di Roma "La Sapienza".

The goal of the project shown here is to demonstrate how it is possible to compile LTL formulas with finite trace (LTLf) within a PDDL task, taking into account temporal extended properties. In particular a Waiter-Robot problem is considered, in which a robot must satisfy the customer by bringing him a drink in a home environment. First of all a LTLf formula is converted into the corresponding Deterministic Finite Automa (DFA) and then the necessary PDDL predicates and fluents are implemented so that they automatically track the current state of the DFA. It is expected that once the plan has reached its goal state also the DFA reach its end state.