Automated synthesis of decentralized controllers for robot swarms from high-level temporal logic specifications

The majority of work in the field of swarm robotics focuses on the bottom-up design of local rules for individual robots that create emergent swarm behaviors. In this paper, we take a top-down approach and consider the following problem: how can we specify a desired collective behavior and automatically synthesize decentralized controllers that can be distributed over robots to achieve the collective objective in a provably correct way? We propose a formal specification language for the high-level description of swarm behaviors on both the swarm and individual levels. We present algorithms for automated synthesis of decentralized controllers and synchronization skeletons that describe how groups of robots must coordinate to satisfy the specification. We demonstrate our proposed approach through an example in simulation.