A Caltech Library Service

Decoupled formal synthesis for almost separable systems with temporal logic specifications

Livingston, Scott C. and Prabhakar, Pavithra (2016) Decoupled formal synthesis for almost separable systems with temporal logic specifications. In: Distributed Autonomous Robotic Systems. Springer Tracts in Advanced Robotics. No.112. Springer , Tokyo, pp. 371-385. ISBN 978-4-431-55877-4.

[img] PDF (v2, addition of keywords and minor adjustment to the introduction) - Accepted Version
See Usage Policy.


Use this Persistent URL to link to this item:


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.

Item Type:Book Section
Related URLs:
URLURL TypeDescription DOIArticle
Contact Email
Additional Information:© 2016 Springer Japan. Part of this work was done while the first author was visiting IMDEA in Madrid, Spain, during summer 2013.
Subject Keywords:reactive synthesis, LTL, collision avoidance, motion planning
Series Name:Springer Tracts in Advanced Robotics
Issue or Number:112
Record Number:CaltechAUTHORS:20141231-105326855
Persistent URL:
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:53155
Deposited By: Scott Livingston
Deposited On:06 Jan 2015 21:00
Last Modified:10 Nov 2021 19:48

Repository Staff Only: item control page