Reasoning about the Past on Temporal Specifications for Motion Planning

Due to the nice balance between the expressive power and the computational cost of associated algorithms, propositional temporal logic (PTL) has recently been used with great success as a specification language for robot motion planning, which is the problem of finding a collision-free route from an initial to a final configuration in a given environment. Elaborated specifications involving temporal ordering such as sequencing or coverage can be succinctly expressed by PTL formulae. The generation of plans satisfying PTL formulae are then reduced to the model checking problem, which concerns the satisfaction of PTL formulae with respect to a given model (in this case the environment). However, in case there is not a plan satisfying the given specification in the current environment, one may also be interested in finding a plan satisfying such specification in some other environment. In the present work, this problem is studied in the context of PTL specifications enriched with past operators. These constructs are used to express backward navigation in the environment. Other interesting reasoning problems such as the equivalence or subsumption of specifications are also studied.