Automated Composition of Motion Primitives for Multi-Robot Systems from Safe LTL Specifications

Indranil Saha, Rattanachai Ramaithitima, Vijay Kumar, George J. Pappas, and Sanjit A. Seshia. Automated Composition of Motion Primitives for Multi-Robot Systems from Safe LTL Specifications. In Proceedings of the IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 1525–1532, September 2014.
For a quick demonstration of this work, see the accompanying video.

Download

[pdf] 

Abstract

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.

BibTeX

@InProceedings{saha-iros14,
  author = 	 {Indranil Saha and Rattanachai Ramaithitima and Vijay Kumar and George J. Pappas and Sanjit A. Seshia},
  title = 	 {Automated Composition of Motion Primitives for Multi-Robot Systems from Safe LTL Specifications},
  booktitle = 	 {Proceedings of the IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages = 	 {1525--1532},
  year = 	 {2014},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  month = 	 {September},
  OPTorganization = {},
  OPTpublisher = {},
  OPTannote = 	 {},
  abstract={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.},
}