Work in swarm robotics typically 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 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 algorithms on a case study.
展开▼
