Welcome to the new version of CaltechAUTHORS. Login is currently restricted to library staff. If you notice any issues, please email coda@library.caltech.edu
Published January 15, 2016 | Accepted Version
Book Section - Chapter Open

Decoupled formal synthesis for almost separable systems with temporal logic specifications


We consider the problem of synthesizing controllers automatically for distributed robots that are loosely coupled using a formal synthesis approach. Formal synthesis entails construction of game strategies for a discrete transition system such that the system under the strategy satisfies a specification, given for instance in linear temporal logic (LTL). The general problem of automated synthesis for distributed discrete transition systems suffers from state-space explosion because the combined state-space has size exponential in the number of subsystems. Motivated by multi-robot motion planning problems, we focus on distributed systems whose interaction is nearly decoupled, allowing the overall specification to be decomposed into specifications for individual subsystems and a specification about the joint system. We treat specifically reactive synthesis for the GR(1) fragment of LTL. Each robot is subject to a GR(1) formula, and a safety formula describes constraints on their interaction. We propose an approach wherein we synthesize strategies independently for each subsystem; then we patch the separate controllers around interaction regions such that the specification about the joint system is satisfied.

Additional Information

© 2016 Springer Japan. Part of this work was done while the first author was visiting IMDEA in Madrid, Spain, during summer 2013.

Attached Files

Accepted Version - Livingston-Prabhakar-DARS2014.pdf


Files (208.3 kB)
Name Size Download all
208.3 kB Preview Download

Additional details

August 20, 2023
January 13, 2024