Skip to main content
Temporal Logic Motion Planning for Mobile Robots
Lab Papers (GRASP)
  • Geogios E Fainekos, University of Pennsylvania
  • Hadas Kress-Gazit, University of Pennsylvania
  • George J Pappas, University of Pennsylvania
Document Type
Conference Paper
Date of this Version
Suggested Citation:
Fainekos, G., H. Kress-Gazit and G.J. Pappas. (2005). "Temporal Logic Motion Planning for Mobile Robts." Proceedings of the 2005 IEEE International Conference on Robotics and Automation. Barcelona, Spain. April 2005.

©2005 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.
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.
  • Motion planning,
  • temporal logics,
  • model checking,
  • discrete abstrations,
  • hybrid control
Citation Information
Geogios E Fainekos, Hadas Kress-Gazit and George J Pappas. "Temporal Logic Motion Planning for Mobile Robots" (2005)
Available at: