Synthesizing Algorithms to Avoid an Obstacle with a Swarm of Robots

Overview & Synopsis

Designing distributed algorithms for a swarm of robots and proving their soundness is a complex, highly combinatorial, and error-prone task. While some attempts at automation have been made, they have remained limited. We propose a partly automated method to synthesize algorithms that solve the perpetual exploration of a finite grid containing an obstacle using luminous myopic robots, with common chirality, in the fully synchronous Look-Compute-Move model. This generic method is supported by a proof-of-concept tool that generates algorithms and verifies them by simulation on small grids. The results of the simulation are generalized to larger grids with a pen-and-paper proof.