Decoupled formal synthesis for almost separable systems with temporal logic specifications

Scott C. Livingston and Pavithra Prabhakar

We consider the problem of synthesizing controllers automatically for distributed robots that are loosely coupled using a formal synthesis approach. For- mal 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 dis- tributed 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 sys- tem. 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 indepen- dently for each subsystem; then we patch the separate controllers around interaction regions such that the specification about the joint system is satisfied.

International Symposium on Distributed Autonomous Robotic Systems (DARS), 2014
Download: BIB PS PDF