Automatic control synthesis for swarm robots from formation and location-based high-level specifications

In this paper, we propose an abstraction that captures high-level formation and location-based swarm behaviors, and an automated control synthesis framework to generate correct-by-construction behaviors. Our abstraction includes symbols representing both possible formations and physical locations in the workspace. We allow users to write linear temporal logic (LTL) specifications over the symbols to specify high-level tasks for the swarm. To satisfy a specification, we automatically synthesize a centralized symbolic plan, and environment and swarm-size-dependent motion controllers that are guaranteed to implement the symbolic transitions. In addition, using integer programming (IP), we assign robots to different sub-swarms to execute the synthesized symbolic plan. Our framework gives insights into controlling a large fleet of autonomous robots to achieve complex tasks which require composition of behaviors at different locations and coordination among different groups of robots in a correct-by-construction way. We demonstrate the proposed framework in simulation with 16 UAVs and 8 ground vehicles, and on a physical platform with 20 ground robots, showcasing the generality of the approach and discussing the implications of controlling constrained physical hardware.