Complan
Complan is a prototype tool for compositional multi-robot motion planning from complex specification.
Complan has been used to synthesize trajectories automatically for a group of four quadrotors, satisfying a set of safety properties.
A video showing the experiments on the quadrotors is available here.
Automated Composition of Motion Primitives for Multi-Robot Systems
from Safe LTL Specifications
paper
Indranil Saha, Rattanachai Ramaitithima, Vijay Kumar, George J. Pappas and Sanjit A. Seshia
IROS 2014
Implan: A Scalable Incremental Motion Planning Framework for Multi-Robot Systems
paper  
Indranil Saha, Rattanachai Ramaithitima, Vijay Kumar, George Pappas and Sanjit A. Seshia
ICCPS 2016
A preliminary version of the tool can be downloaded from here.
The tool should run on any Unix based platform.
After you download the tool, place it to the directory where you want to run the tool and
use the following commad.
tar -xvzf complan.tgz
This command will create a directory name complan_distribution in the same folder.
To know how to run the tool, please see the README file in the top directory.
Complan uses Z3 as the backend SMT solver. You should have Z3 installed and available
in your path. For the information on how to get Z3 and install it in your machine,
please refer to Z3 Homepage.
Please report any bug to Indranil Saha at saha.indra[at]gmail[dot]com.
This project was supported in part by TerraSwarm, one of six centers of STARnet, a Semiconductor Research Corporation program sponsored by MARCO and DARPA, and by the NSF project ExCAPE (grants CCF- 1138996 and CCF-1139138).