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

Automated composition of motion primitives for multi-robot systems from safe LTL specifications

  • Author(s): Saha, I
  • Ramaithitima, R
  • Kumar, V
  • Pappas, GJ
  • Seshia, SA
  • et al.

© 2014 IEEE. We present a compositional motion planning framework for multi-robot systems based on an encoding to satisfiability modulo theories (SMT). In our framework, the desired behavior of a group of robots is specified using a set of safe linear temporal logic (LTL) properties. Our method relies on a library of motion primitives, each of which corresponds to a controller that ensures a particular trajectory in a given configuration. Using the closed-loop behavior of the robots under the action of different controllers, we formulate the motion planning problem as an SMT solving problem and use an off-the-shelf SMT solver to generate trajectories for the robots. Our approach can also be extended to synthesize optimal cost trajectories where optimality is defined with respect to the available motion primitives. Experimental results show that our framework can efficiently solve complex motion planning problems in the context of multi-robot systems.

Many UC-authored scholarly publications are freely available on this site because of the UC Academic Senate's Open Access Policy. Let us know how this access is important for you.

Main Content
Current View