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

Back