Paper Info
Title
Decoupled Formal Synthesis for Almost Separable Systems with Temporal Logic Specifications
Abstract
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.
Year
DOI
Venue
2014
10.1007/978-4-431-55879-8_26
Springer Tracts in Advanced Robotics
Keywords
Field
DocType
Reactive synthesis,LTL,Collision avoidance,Motion planning
Transition system,Motion planning,Formal synthesis,Exponential function,Computer science,Separable space,Linear temporal logic,Temporal logic,Robot,Distributed computing
Conference
Volume
ISSN
Citations 
112
1610-7438
0
PageRank 
References 
Authors
0.34
12
2
Name
Order
Citations
PageRank
Scott C. Livingston1242.58
Pavithra Prabhakar221925.69