Distributed implementations of global temporal logic motion specifications

We present a computational framework for automatic synthesis of decentralized communication and control strategies for a robotic team from global specifications given as temporal and logic statements about visiting regions of interest in a partitioned environment. We consider a purely discrete scenario where the robots move among the vertices of a graph. However, by employing recent results on invariance and facet reachability for dynamical system in environments with polyhedral partitions, the framework from this paper can be directly implemented for robots with nontrivial dynamics. While providing a rich specification language and guaranteeing the correctness of the solution, our approach is conservative, in the sense that we might not find a solution even if one exists. The overall amount of required computation is large. However, most of it is performed off-line before the deployment.