Linear Temporal Logic Motion Planning for Teams of Underactuated Robots Using Satisfiability Modulo Convex Programming
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. The workspace is characterized by a set of obstacles and a set of regions of interest, where both the obstacles and the regions are polyhedra. Given an LTL formula phi, 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 Psi. We show that the motion planning problem can be formulated as the feasibility problem for a formula ' 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 phi to decompose the problem into smaller subproblems. At each iteration, a Boolean satisfiability solver searches for candidate high-level discrete plans while completely abstracting the low-level continuous dynamics. Convex programming is then used to check the feasibility of the proposed plans against the dynamic constraints, or generate succinct explanations for their infeasibility to reduce the search space. New candidate plans can then be efficiently generated until a feasible one is found. 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.