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

Yasser Shoukry, Pierluigi Nuzzo, Ayca Balkan, Indranil Saha, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, George J. Pappas, and Paulo Tabuada. Linear temporal logic motion planning for teams of underactuated robots using satisfiability modulo convex programming. In 56th IEEE Annual Conference on Decision and Control (CDC), pp. 1132–1137, 2017.

Download

[HTML] 

Abstract

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.

BibTeX

@inproceedings{shoukry-cdc17,
  author    = {Yasser Shoukry and
               Pierluigi Nuzzo and
               Ayca Balkan and
               Indranil Saha and
               Alberto L. Sangiovanni{-}Vincentelli and
               Sanjit A. Seshia and
               George J. Pappas and
               Paulo Tabuada},
  title     = {Linear temporal logic motion planning for teams of underactuated robots
               using satisfiability modulo convex programming},
  booktitle = {56th {IEEE} Annual Conference on Decision and Control (CDC)},
  pages     = {1132--1137},
  year      = {2017},
  abstract  = {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.},
}