Distributing Co-safe LTL Specifications to Mobile Robots

Abstract

This work considers the problem of decomposing a global motion specification given to a team of robots into parts that can be individually followed by agents, without any need of communication among them. The specification is given as a co-safe Linear Temporal Logic (LTL) formula over some regions of interest from a known and static environment. The main contribution is an algorithmic method for distributing the specification, while identifying necessary sequencing relations among some regions to be visited. Each of these sequences has to be assigned to a robot, and the concurrent movement of the agents accomplishes the global imposed mission.