Verifiable Control of Robotic Swarm from High-level Specifications

Designing controllers for safe, scalable and flexible collective behaviors of large numbers of robots is an important and challenging problem in swarm robotics. In this paper, we focus on provably-correct controller synthesis from high-level specifications and demonstrate the approach on several physical swarms. To this end, we first automatically synthesize discrete controllers (symbolic plans) from high-level task specifications expressed in temporal logic. Then, we automatically synthesize continuous controllers that implement the symbolic plans while ensuring collision avoidance and describe methods for mitigating deadlocks that might occur. In addition, centralized and decentralized continuous controller design are compared and analyzed. Finally, we demonstrate the flexibility and versatility of the control paradigm by applying it to three different examples of swarm systems with two different types of robots.