Deterministic color-optimal self-stabilizing semi-synchronous gathering: Two certified algorithms

• We propose two new algorithms for mobile robots that solves the gathering problem. • Our algorithms are self-stabilizing and use the minimum possible memory (two states per robot). • Our results are formally proved with the Coq proof assistant with the Pactole framework. We consider the problem of gathering in finite time and at the same location, not known beforehand, a set of deterministic semi-synchronous robots, starting from an arbitrary initial configuration that may even be bivalent (that is, a configuration where the robots are evenly split on two different locations). This problem is known to be unsolvable when the robots are oblivious, that is, when they cannot remember their past actions. We present two deterministic gathering algorithms where robots may remember and communicate a single bit of memory. This bit may be arbitrarily (and adversarially) set in the initial configuration. Our solutions are thus memory optimal and self-stabilizing. The first algorithm makes use of multiplicity detection, while the second solely uses robot colors. Their proof of correctness is formally certified by the Coq proof assistant using the Pactole framework.