Skip to main content
Open Access Publications from the University of California

UC Berkeley

UC Berkeley Previously Published Works bannerUC Berkeley

Linear temporal logic motion planning for teams of underactuated robots using satisfiability modulo convex programming

  • Author(s): Shoukry, Y
  • Nuzzo, P
  • Balkan, A
  • Saha, I
  • Sangiovanni-Vincentelli, AL
  • Seshia, SA
  • Pappas, GJ
  • Tabuada, P
  • et al.

We present an efficient algorithm for multi-robot motion planning from linear temporal logic (LTL) specifications. We assume that the dynamics of each robot can be described by a discrete-time, linear system together with constraints on the control inputs and state variables. Given an LTL formula specifying the multi-robot mission, our goal is to construct a set of collision-free trajectories for all robots, and the associated control strategies, to satisfy We show that the motion planning problem can be formulated as the feasibility problem for a formula p over Boolean and convex constraints, respectively capturing the LTL specification and the robot dynamics. We then adopt a satisfiability modulo convex (SMC) programming approach that exploits a monotonicity property of p to decompose the problem into smaller subproblems. Simulation results show that our algorithm is more than one order of magnitude faster than state-of-the-art sampling-based techniques for high-dimensional state spaces while supporting complex missions.

Many UC-authored scholarly publications are freely available on this site because of the UC's open access policies. Let us know how this access is important for you.

Main Content
Current View