Automated Synthesis of Multi-Robot Motion Plans from LTL Specifications
Indranil Saha, Rattanachai Ramaithitima, Vijay Kumar, George Pappas, Sanjit Seshia

Citation
Indranil Saha, Rattanachai Ramaithitima, Vijay Kumar, George Pappas, Sanjit Seshia. "Automated Synthesis of Multi-Robot Motion Plans from LTL Specifications". Talk or presentation, 4, November, 2014.

Abstract
We present an SMT (Satisfiability Modulo Theories) based compositional motion planning framework for multi-robot systems, where the runtime behavior of a group of robots is specified using a set of LTL (Linear Temporal Logic) formulas with quantifiers defined over the set of robots. Our method relies on a library of motion primitives that provides a set of controllers to be used to control the behavior of the robots in different configurations. Using the closed loop behavior of the robots under the action of different controllers, we encode the multi-robot motion planning problem as a bounded synthesis problem. The encoding of bounded synthesis problem gives rise to a finite set of constraints, the solution of which represents infinite length trajectories satisfying LTL specifications. We use the off-the-shelf SMT solver Z3 to solve the constraints and generate trajectories for the individual robots. We apply our technique to synthesize trajectories for a group of quadrotors for a set of surveillance missions. Experimental results show that our framework is capable of synthesizing trajectories for multi-robot systems automatically from complex LTL specifications.

Electronic downloads

Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Indranil Saha, Rattanachai Ramaithitima, Vijay Kumar, George
  Pappas, Sanjit Seshia. <a
  href="http://www.terraswarm.org/pubs/437.html"
  ><i>Automated Synthesis of Multi-Robot Motion Plans
  from LTL Specifications</i></a>, Talk or
  presentation,  4, November, 2014.

• Plain text

  Indranil Saha, Rattanachai Ramaithitima, Vijay Kumar, George
  Pappas, Sanjit Seshia. "Automated Synthesis of
  Multi-Robot Motion Plans from LTL Specifications". Talk
  or presentation,  4, November, 2014.

• BibTeX

  @presentation{SahaRamaithitimaKumarPappasSeshia14_AutomatedSynthesisOfMultiRobotMotionPlansFromLTLSpecifications,
      author = {Indranil Saha and Rattanachai Ramaithitima and
                Vijay Kumar and George Pappas and Sanjit Seshia},
      title = {Automated Synthesis of Multi-Robot Motion Plans
                from LTL Specifications},
      day = {4},
      month = {November},
      year = {2014},
      abstract = {We present an SMT (Satisfiability Modulo Theories)
                based compositional motion planning framework for
                multi-robot systems, where the runtime behavior of
                a group of robots is specified using a set of LTL
                (Linear Temporal Logic) formulas with quantifiers
                defined over the set of robots. Our method relies
                on a library of motion primitives that provides a
                set of controllers to be used to control the
                behavior of the robots in different
                configurations. Using the closed loop behavior of
                the robots under the action of different
                controllers, we encode the multi-robot motion
                planning problem as a bounded synthesis problem.
                The encoding of bounded synthesis problem gives
                rise to a finite set of constraints, the solution
                of which represents infinite length trajectories
                satisfying LTL specifications. We use the
                off-the-shelf SMT solver Z3 to solve the
                constraints and generate trajectories for the
                individual robots. We apply our technique to
                synthesize trajectories for a group of quadrotors
                for a set of surveillance missions. Experimental
                results show that our framework is capable of
                synthesizing trajectories for multi-robot systems
                automatically from complex LTL specifications.},
      URL = {http://terraswarm.org/pubs/437.html}
  }
  

Posted by Indranil Saha on 4 Nov 2014.
Groups: tools