Temporal Logic Motion Planning for Mobile Robots
Fainsekos, Kress-Gazit, Pappas
robotics ltl linear temporal logic path planning motion
@inproceedings{fainekos:icra-2005,
title={Temporal Logic Motion Planning for Mobile Robots},
author={Fainekos, G.E. and Kress-Gazit, H. and Pappas, G.J.},
booktitle={{IEEE} International Conference on Robotics and Automation},
pages={2020--2025},
year={2005},
organization={IEEE}
}
[ Download PDF ]
Abstract:
In this paper, we consider the problem of robot motion planning in order to satisfy formulas expressible in temporal logics. Temporal logics naturally express traditional robot specifications such as reaching a goal or avoiding an obstacle, but also more sophisticated specifications such as sequencing, coverage, or temporal ordering of different tasks. In order to provide computational solutions to this problem, we first construct discrete abstractions of robot motion based on some environmental decomposition. We then generate discrete plans satisfying the temporal logic formula using powerful model checking tools, and finally translate the discrete plans to continuous trajectories using hybrid control. Critical to our approach is providing formal guarantees ensuring that if the discrete plan satisfies the temporal logic formula, then the continuous motion also satisfies the exact same formula.
Discretize the space by some decomposition
Specify goals and constraints over the robot's path via linear temporal logic
- E.g., Must go to area a2, then a3, then a4, then back to a1, without going through a2 or a3.
Negate that specification and run through a model checker to come up with a counter-example of the negation
- This counter-example is a plan that satisfies the specification
Run that sequence through a continuous space motion planner to generate the actual path the robot must follow
- Bisimulation properties of the decomposition and planner enable proof that the plan over the discretized space will be applicable in the continuous space