# Deterministic Color-optimal Self-stabilizing Semi-synchronous Gathering: a Certified Algorithm

François Bonnet, Quentin Bramas, Pierre Courtieu, Xavier Défago, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain

► To cite this version:

François Bonnet, Quentin Bramas, Pierre Courtieu, Xavier Défago, Lionel Rieg, et al. Deterministic Color-optimal Self-stabilizing Semi-synchronous Gathering: a Certified Algorithm. SIROCCO 2025, Jun 2025, Delphi, Greece. pp.127-143, 10.1007/978-3-031-91736-3_8. hal-04988128

HAL Id: hal-04988128

https://hal.science/hal-04988128v1

Submitted on 6 Nov 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Deterministic Color-optimal Self-stabilizing Semi-synchronous Gathering: a Certified Algorithm*

François Bonnet<fnref n="1" />, Quentin Bramas², Pierre Courtieu<fnref n="3" />, Xavier Défago<fnref n="1" />, Lionel Rieg⁴, Sébastien Tixeuil⁵,⁶, and Xavier Urbain<fnref n="7" />✉

**Abstract.** 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 a deterministic gathering algorithm where robots may remember and communicate one bit of memory. This bit may be arbitrarily (and adversarially) set in the initial configuration. Our solution is thus memory optimal and self-stabilizing. Its proof of correctness is formally certified by the COQ proof assistant using the PACTOLE framework.

**Keywords:** Mobile robots · Proof assistant · Self-stabilization

## 1 Introduction

Mobile robot networks have garnered significant interest within the distributed computing community due to their wide range of potential applications, including search and rescue operations, environmental monitoring, and surveillance in hazardous environments. In the classical model used to mathematically study such robotic swarms [23], robots operate in Look-Compute-Move (LCM) cycles. During each cycle, a robot observes its surroundings to capture a snapshot of the positions of other robots, computes a destination based on this snapshot, and then moves to the calculated location.

Oblivious robots execute these cycles without retaining any memory of their past actions. In contrast, luminous robots [12] can retain and exchange a constant amount of information, represented by an individual light visible to other robots, the color of which can be altered by the hosting robot. The execution of these

<footnote n="1">¹Institute of Science Tokyo, Japan. ²University of Strasbourg, ICUBE, France.</footnote>

<footnote n="3">³CNAM, Cédric, France. ⁴Grenoble INP - UGA, CNRS (UMR 5104), Verimag, France. ⁵Sorbonne University, LIP6, France. ⁶Institut Universitaire de France.</footnote>

<footnote n="7">⁷Universite Claude Bernard Lyon 1, CNRS, INSA Lyon, LIRIS, UMR5205, France.</footnote>

<footnote>* This work was partially supported by ANR project SAPPORO 2019-CE25-0005.</footnote>
tasks is influenced by the synchronization level among the robots, which can
be either synchronous (FSYNC), semi-synchronous (SSYNC), or asynchronous
(ASYNC). In this study, we concentrate on the SSYNC model, where robots
perform LCM cycles in discrete rounds, with a fair scheduler ensuring that all
robots are activated within a finite number of steps.

The robots in this setting have minimal capabilities: they are anonymous,
run the same algorithm, and may be disoriented, meaning that their observations
are interpreted through local coordinate systems that may not align with those
of other robots. In distributed systems like these, an appealing property for
resilience against transient failures is self-stabilization [16]. Within the context
of mobile LCM robots, self-stabilization entails [15,14,1,19] that the robots can
begin from arbitrary initial locations, including configurations with multiplicity
points, and for luminous robots, that their memory (including the initial color
of their light) can be arbitrarily set.

In this paper, we tackle the fundamental problem of gathering these robots
starting from an arbitrary configuration in finite time to a unique location, not
known beforehand, and maintain them there forever. Note that the fact that the
robots must remain gathered forever implies that any algorithm solving the gather-
ing problem for arbitrary initial configuration is by definition self-stabilizing.
Despite its apparent simplicity, the gathering problem has attracted consider-
able attention [18]. A key result [23,9] establishes that in the SSYNC or ASYNC
models, no oblivious deterministic algorithm can solve the gathering problem
for two robots without additional assumptions. The core reasoning behind this
impossibility is that robots may possess symmetric coordinate systems and can
perpetuate this symmetry indefinitely. This finding can be extended [9] to the
bivalent scenario, where an even number of robots are initially evenly distributed
between two locations. Prencipe [21] further generalized this result, demonstrat-
ing that in SSYNC, when $n > 2$ robots start from distinct initial locations,
no oblivious deterministic algorithm can solve the gathering problem without
additional assumptions, such as multiplicity detection. On the other hand, in
the FSYNC model, it is possible to solve the gathering problem without such
additional assumptions [3]. In the ASYNC model, gathering becomes feasible if
$n > 2$ robots start from distinct initial locations and are equipped with weak
multiplicity detection [8].

The fundamental challenge in deterministically solving the gathering prob-
lem stems from the possibility of robots starting in a bivalent configuration.
Any other starting configuration is solvable [7,10], as maintaining a non-bivalent
configuration is an invariant in these algorithms. To overcome this impossibil-
ity, various assumptions have been explored in previous research. For instance,
Dieudonné *et al.*[15] addressed the problem by assuming an odd number of
robots, as this prevents the formation of any bivalent configuration. Défago *et
al.*[14] introduced probabilistic elements into the algorithm to resolve symmet-
rical situations, allowing for the handling of potentially bivalent initial config-
urations. However, this approach sacrifices deterministic correctness, achieving
gathering only in expected finite time. More recently, Asahiro *et al.*[1] explored
the use of deterministic robots that do not all execute the same algorithm, prov-
ing that two distinct algorithms are both necessary and sufficient to solve the
problem. In summary, within the oblivious setting, successful gathering requires
compromising on either flexibility[15], deterministic guarantees [14], or unifor-
mity [1].

In the context of luminous robots, a partial affirmative answer to the central
question of whether a deterministic self-stabilizing gathering algorithm exists
in the SSYNC model has been provided for the case of two robots (i.e., the
rendezvous problem [25,13]). With two robots, any non-gathered configuration
is bivalent, yet the problem can still be solved deterministically in both the
SSYNC [25] and ASYNC [13] scheduling models, starting from any arbitrary
state, including light color. It has been established that two colors are both
necessary and sufficient to solve the rendezvous problem, making these solu-
tions optimal in that regard. Terai et al. [24] provided a partial answer to the
general case of self-stabilizing gathering $n \ge 2$ luminous robots. First, in the
SSYNC execution model, two colors are sufficient to gather from an arbitrary
placement of the robots, but their solution requires that all robots start with
the same color (hence, their solution is not self-stabilizing). Second, assuming a
centralized scheduler (that may activate only one robot at a time to execute a
Look-Compute-Move cycle), a fully-self-stabilizing solution is feasible. Overall,
to date, no self-stabilizing SSYNC solution has been found for scenarios involving
more than two robots, leading to clear open questions: In the luminous model,
does a self-stabilizing deterministic gathering algorithm exist in the SSYNC ex-
ecution model for more than two robots? If so, what is the minimum number of
colors required?

***Our Contribution.*** We provide a positive answer to the computability question and an optimal answer to the complexity question. In more details, we design and prove correct a self-stabilizing deterministic gathering algorithm that relies on strong multiplicity detection and makes use of two colors per light (a single color is tantamount to requiring the robots to be oblivious, and thus renders the problem impossible to solve). A noteworthy property of our approach lies in the use of formal methods to assess the correctness of our algorithm, and we make use of the PACTOLE library and the COQ proof assistant.

Our use of formal methods is commanded by observing that results in the mo-
bile robots area of Distributed Computing are traditionally described and proved
in natural language. However, algorithms, even when presented as pseudo-code,
cannot be fully understood without the *precise setting* in which they are exe-
cuted. *Implicit assumptions* are often considered folklore, but because properties
of distributed algorithms depend on very subtle hypotheses, even a small, barely
noticeable shift in these assumptions can drastically change an algorithm’s be-
havior. Such shifts still appear in the literature, leading to erroneous results be-
ing discovered sometimes years after publication (see recent error discoveries and
references therein [5,17]). Formal methods address this issue by using tools that
provide a non-ambiguous mathematical language. Given the difficulty of estab-
lishing correct results in mobile robotics, using a common, non-ambiguous format
for definitions is a significant advantage to ensure trust in the proved result (and improve its re-usability in subsequent work). Among closely related works, most algorithms [1,7,14,15,25] only have pen-and-paper correctness proofs. One notable exception is the luminous rendez-vous algorithm by Defago et al. [13] that makes use of model checking to prove its correctness (and also prove the correctness of Viglietta's algorithm [25] as a byproduct). Unfortunately, the approach of Defago et al. [13] is tightly coupled to a two-robots system, and is unlikely to scale to arbitrary size, as a key result of Sangnier et al. [22] in the context of parameterized model-checking shows that non-trivial properties (namely, liveness properties) are undecidable.

As a result, following the path of Courtieu et al. [10], we use a proof assistant, that is not bound by the limitations of the model-checking approach, to assess the correctness of our algorithm. Interestingly, since the algorithm of Courtieu et al. [10] solves gathering when the initial configuration is not bivalent, we were not only able to reuse its algorithm as a building block, but also its formal proof for (partially) proving our own solution, saving development time. A general comparison of our solution with previous works is presented in Table 1.

This article describes the algorithm, and gives an intuition of the key steps in the proof of its correctness. The actual complete proof is provided as a CoQ development. As explained in [4], assisted proofs are themselves correct by construction and thus, do not need a manual review by the community. However, a remaining crucial step is to ensure that the formal statements match the claimed results. In particular, the formal CoQ definitions and final theorem statements must be carefully checked to make sure that the formal development provides indeed the proofs of the relevant properties.

The source code of our formal development for CoQ 8.19 and 8.20 is available at the following URL: https://pactole.liris.cnrs.fr.

<table><caption>**Table 1.** A comparison of our algorithm with existing SSYNC solutions (most desirable properties are in boldface).</caption><thead><tr><th>Reference</th><th>Size</th><th>Deterministic</th><th>Uniform</th><th>Proof</th><th>Oblivious</th><th>Self-stabilizing</th></tr></thead><tbody><tr><td>[15]</td><td>n is odd</td><td>yes</td><td>yes</td><td>pen-and-paper</td><td>yes</td><td>yes</td></tr><tr><td>[25]</td><td>n = 2</td><td>yes</td><td>yes</td><td>pen-and-paper</td><td>no</td><td>yes</td></tr><tr><td>[7]</td><td>any</td><td>yes</td><td>yes</td><td>pen-and-paper</td><td>yes</td><td>no</td></tr><tr><td>[10]</td><td>any</td><td>yes</td><td>yes</td><td>proof assistant</td><td>yes</td><td>no</td></tr><tr><td>[14]</td><td>any</td><td>no</td><td>yes</td><td>pen-and-paper</td><td>yes</td><td>yes</td></tr><tr><td>[1]</td><td>any</td><td>yes</td><td>no</td><td>pen-and-paper</td><td>yes</td><td>yes</td></tr><tr><td>[13]</td><td>n = 2</td><td>yes</td><td>yes</td><td>model-checker</td><td>no</td><td>yes</td></tr><tr><td>[24]</td><td>any</td><td>yes</td><td>yes</td><td>pen-and-paper</td><td>no</td><td>no</td></tr><tr><td>This paper</td><td>any</td><td>yes</td><td>yes</td><td>proof assistant</td><td>no</td><td>yes</td></tr></tbody></table>
## 2 Model

We consider a distributed system where a set of $n \in \mathbb{N}^*$ entities, called robots, are located on an Euclidean plane. We identify each robot by a number in $[0, n-1] = \mathcal{N}$ for the analysis only as robots do not have access to their identity. Each robot $r$ has a location $l$, represented by coordinates in a global coordinate system, and a color $c$, represented by a boolean, true for the color WHITE and false for the color BLACK. A configuration of the system at time $t$, denoted $C(t)$ is a function that maps each robot identity to its state $(l, c)$. The set of all configurations is denoted $\mathcal{C}$.

The robots are said to be uniform as they all execute the same algorithm. They are disoriented in the sense that this algorithm takes as input, not the configuration $C(t)$, but a local perception of it called the observation. In this paper, the observation is obtained from the configuration $C(t)$ by removing the identity of the robots and by changing the coordinate system of the locations. We consider that each robot has its own coordinate system and that we can transform a location in the global coordinate system to the local coordinate system of $r$ using a similarity $\varphi_r$ that keeps the origin invariant (that is a combination of rotation, reflection, and scaling). To ensure that the robot knows where it is located, we also translate the locations so that a robot is always located at the origin of its local coordinate system (that is, it is ego-centered). We denote by $\mathbf{t}_r$ the translation of the plane mapping $C(t)(r)$ to $(0, 0)$. Formally, the observation of a robot $r$ in configuration $C(t)$ is the multiset

$$ \text{obs}(C(t), r) = \bigcup_{r' \in \mathcal{N}} \{(\varphi_r \circ \mathbf{t}_r(l), c) \mid (l, c) = C(t)(r')\} $$

In practice, the observation can be given to the algorithm in a more convenient way, such as a list of pairs (in arbitrary order), or other structures as described in our formal proof in Section 4.

The system evolves when the robots are activated at each round. The update of the configuration is a construction formally defined by the PACTOLE framework we are using. The intuition behind this construction is as follows. At each round $t$, a subset $S(t) \subset \mathcal{N}$ of the agents are activated. Each active agent retrieves its observation $\text{obs}(C(t), r)$, then computes its destination by executing the same algorithm $A$ that takes as input an observation and returns a pair $(l_r, c_r)$ representing a new location $l_r$ and a new color $c_r$. From there, the new configuration $C(t+1)$ is simply the function that maps each robot $r$ to its new state (its new location in the global coordinate system and its new color) if it was activated, or its unchanged state otherwise:

$$ C(t+1)(r) = \begin{cases} C(t)(r) & \text{if } r \notin S(t) \\ (\mathbf{t}^{-1} \circ \varphi_r^{-1}(l_r), c_r) & \text{if } r \in S(t) \end{cases} $$

An execution is an infinite sequence of configurations. A gathered configuration is a configuration where all the robots share the same location. The set of gathered configurations is denoted *Gathered*. The gathering problem consists in
reaching a gathered configuration in a finite number of rounds from any initial configuration, and staying idle afterwards. Formally, an algorithm A solves the gathering problem if it satisfies:

$$ \forall C(0) \in C, \exists t, \forall t' \ge t, C(t) = C(t') \in \text{Gathered} $$

## 3 Algorithm Description

In this section, we present our algorithm solving the gathering problem without any restriction on the initial configuration. We first give a textual description of it, then a more formal definition closer to the one written in COQ, presented in the next section.

**Informal description** The algorithm consists of three main parts, depending on whether the configuration is color-bivalent, bivalent but not color-bivalent, or non-bivalent. A color-bivalent configuration consists of two towers of equal size at distinct locations, with as many BLACK and WHITE robots in each tower. A robot that is activated performs the following:

- IF the configuration is color-bivalent, the goal is to break the symmetry.

• IF the activated robot is WHITE, go to the middle of the two towers, change color to BLACK.

• IF the activated robot is BLACK, change color to WHITE.

- IF the configuration is bivalent but not color-bivalent, the number of BLACK robots is not the same in the two towers, and the activated robot goes to the tower with the higher number of BLACK robots.

- IF the configuration is not bivalent, use the SSYNC oblivious algorithm of [10] certified in COQ, which never creates a bivalent configuration thereafter.

<caption>**Algorithm 1:** Executed by a robot with observation obs</caption>

```c
if bivalentobs(obs) then
  c ← observerlght(obs)
  if colorbivalentobs(obs) then
    if c == true i.e. is White then
      return (middle(obs), false)
    else
      return ((0, 0), true)
  else
    return (find_max_black(obs), c)
else
  execute gatherR2_old_pgm(obs)
```
**Pseudo-code** In pseudo-code, the algorithm is defined in Algorithm 1. It makes use of functions to check whether the observation *obs* is bivalent or color-bivalent, with *bivalentobs* and *color_bivalentobs* respectively. The functions *middle* and *find_max_black* are used to compute particular points of the observation as destinations, respectively the middle of both towers and the tower with the highest number of BLACK robots.

<figure><img src="image_2.png" /><figcaption>Fig. 1. Execution examples starting from color-bivalent configurations</figcaption></figure>

**Example of executions** Figure 1 illustrates three execution examples starting from color-bivalent configurations. For simplicity, we present the multiplicity points as a tower of robots, to better see the number of BLACK and WHITE robots at each location. In Execution *E*₁, a single BLACK robot is first activated, so that after one round the number of BLACK robots is not the same at the two locations, and the configuration is no longer color-bivalent (but remains bivalent). A similar result is obtained if more BLACK robots are activated, as soon as a different number of robots is activated on each location. If the same number of BLACK robots is activated, and the configuration remains color-bivalent then eventually all the robots become WHITE, as in execution *E*₃. The second configuration of execution *E*₁ is not color-bivalent, as one of the towers has more robots than the other, and every activated robot is ordered to move toward it. Eventually, all the robots gather in the same location.

In Execution *E*₂, a WHITE robot is activated in one of the towers. Here, regardless of the activation of the BLACK robots, the obtained configuration contains three points so is not bivalent. From there, executing the oblivious algorithm for non-bivalent configurations ensures that the robots eventually gather at a single point.

Consider now Execution *E*₃, which starts from a color-bivalent configuration where all robots are WHITE. If all are executed, they all move to the middle and join a single multiplicity point. If only a strict subset of one of the towers is
activated, then the obtained configuration contains three points and the config-
uration is not bivalent anymore. Otherwise, as in the illustration, if one tower
is activated and not the other, the obtained configuration is bivalent (distance
is halved) but one of the towers contains only BLACK robots, and the other
only WHITE robots, so the configuration is not color bivalent and the robots
eventually gather at a single location.

4 Formal proof

To ensure that our algorithm is correct we make use of PACTOLE<fnref n="1" />, a formal
library for the COQ proof assistant<fnref n="2" /> that is dedicated to autonomous mobile
robots.

Proof assistants are pieces of software that certify the soundness of a proof
provided by the user. In the case of COQ, this is achieved using type theory and
the Curry-Howard correspondence. In sharp contrast to automated provers, proof
assistants do not state that a property holds with full automation. Instead, they
check that a proof, usually developed interactively, is correct. With a tradeoff
between automation and expressiveness, statements can be very close to intuition
but proofs can be tedious. Hence, various libraries exist to assist the user in
various domains, notably by providing definitions and theorems that are void of
implicit assumptions, and specialized proof tactics to help with some (limited
form of) automation. PACTOLE is the de facto standard library currently being
developed for robotic swarms [11]. It has proven invaluable in establishing formal
correctness of several algorithms, among which the one of Courtieu et al. [10] we
reuse parts of. For an introduction to the COQ proof assistant, the reader may
refer to standard expositions [20,6]. A comprehensive presentation of PACTOLE
and its uses may be found in a recent survey [11].

The use of a proof assistant like COQ enforces that the context where we reuse
theorems and proofs from Courtieu et al. [10] is compatible with their soundness
(i.e. the current context and the original context of Courtieu et al. [10] permit
to derive the same results). In other words: all those theorems still hold in our
context, and we can build upon them. Hence, the first step is to define the context
(evolving space, synchronicity assumptions, etc.) similarly to that of Courtieu et
al. [10]. Then, we can specify our luminous robots (remember that the robots of
Courtieu et al. [10] were oblivious).

4.1 Description of our algorithm in PACTOLE

The self-stabilizing algorithm gatherR2 we propose may be seen as consisting
of three parts: respectively describing the behavior when confronted to a color-
bivalent observation, a bivalent but not color-bivalent observation, and finally,
an observation that is not bivalent. In the last case, our algorithm refers to the

<footnote n="1">¹ https://pactole.liris.cnrs.fr</footnote>

<footnote n="2">² https://coq.inria.fr/</footnote>
one from Courtieu et al. [10], hereafter named `gatherR2_old_pgm`, which has been proven to be sound and not leading to any bivalent configuration.

As a set of only two distinct colors suffices in our algorithm, we choose to instantiate this set `L` with Boolean values, `true` being `WHITE`, and `false` being `BLACK`. We can now define the state of a robot to be an ordered pair of type `location * L` consisting of its current location and light color.

As we want to reuse the algorithm of Courtieu et al. [10] with as little adaptation work as possible, we want to keep their original observation type (a multiset of location, well-suited to represent a configuration of anonymous robots with full global multiplicity). Yet, in our model, robots have lights and can observe them, including their own. Hence we define the new observation as a pair, with the observation from Courtieu et al. [10] as the first member, and a record consisting of the light color of the observer and a multiset of locations and light colors as second member.

Now, coherence between the observation with lights and the one without is proven once and for all. Crucially, there is *no need to modify* the algorithm of Courtieu et al. [10] (for example, no need to include a projection in their code to prune lights out), and any adaptation of previous results is rather light (see Section 4.3).

An algorithm is a function that takes an observation and returns a new robot state; and the code of ours is simply:

```
Definition gatherR2 (obs : observation) : location * L :=
    if bivalentobs obs (* if bivalent then 2 distinct locations *)
    then let other_loc := find_other_loc (fst obs) origin in
        if color_bivalentobs obs (* is obs color bivalent? *)
        (* color bivalent: check own light *)
        then if observer_lght (snd obs) (* is own light white? *)
            (* yes: to middle + switch to black *)
            then (middle origin other_loc, false)
            (* no: stay + switch to white *)
        else (origin, true)
        (* bivalent & not color bivalent: go to max black lght *)
    else
        let maj_black := find_max_black obs origin other_loc in
            (maj_black, observer_lght (snd obs))
(* not bivalent: Courtieu et al. will do + keep light status *)
else (gatherR2_old_pgm (fst obs), observer_lght (snd obs)).
```

## 4.2 Structure of the formal proof

The formal development itself consists of two main stages.

Firstly, we define an observation taking lights into account; this new context is provided in file `WithMultiplicityLight.v` in the companion code repository. The file contains properties about bivalent and color-bivalent configurations.

Note that, so as to stay coherent with all previous developments on that topic (most notably with Courtieu et al. [10]), we use the formal definitions of gathering properties from the PACTOLE library. Let us recall some of them:
Relation `Gather pt e` means that at all rounds of an (infinite) execution `e`, robots are gathered at the same (unchanging) position `pt`.

**Definition** `Gather` (`pt`: `location`) (`e`: `execution`) : `Prop` :=
`Stream.forever` (`Streaminstant` (`gathered_at pt`)) `e`.

Relation `WillGather e` means that the (infinite) execution `e` is eventually
in `Gather` for a certain `pt`.

**Definition** `WillGather` (`e`: `execution`) : `Prop` :=
`Stream.eventually` (**fun** `e` ⇒ ∃ `pt`, `Gather pt e`) `e`.

The definition of a solution for gathering is thus:

**Definition** `FullSolGathering` (`rbg`: `robogram`) (`d`: `demon`) :=
∀ `config`: `configuration`, `WillGather` (`execute rbg d config`).

An algorithm `rbg` is a solution to Gathering for an activation demon `d` (that
is, for some choice of the environment) if for any configuration `config`, the
execution eventually leads to a gathered configuration. The main difference
from the solution of Courtieu et al. [10] is that our current proposal, using
`FullSolGathering` has no condition on the configuration, it is universally quan-
tified. Further note that it is the statement used in the proof of impossibility of
gathering without lights. We are thus dealing with the exact same property.

Secondly, we propose our new algorithm `gatherR2` and, in particular, we
establish formally that for any fair semi-synchronous demon and from any con-
figuration, every execution eventually leads to a configuration where all robots
are (and remain) gathered. In the code archive this development takes place
in file `Algorithm_withLight.v`, together with the adaptation of the results
regarding the original algorithm by Courtieu et al. [10].

The formal proof itself is organized as follows.

**The overall structure follows the algorithm.** Firstly, as the algorithm `gatherR2` differentiates three classes of configuration, namely the color-bivalent, bivalent but not color-bivalent, and the not-bivalent cases, so does the final proof. Its development is thus split into three COQ sections, namely `ColorBivalent`, `BivalentButNotColorBivalent`, and `NonBivalent`. Each of these sections contains, in particular, the general assumptions that define it, and specialized versions of some lemmas, such as the `round_simplify` lemma linking the behavior of the algorithm observed from the local and from the global frames of reference. For example: an obvious assumption in section `NonBivalent` is that the considered configuration is indeed not bivalent, and we can state (and prove) that in this case, robot lights do not change along the execution, that is: for any robot in that configuration, the value of its light after one round for `gatherR2` is the same as before the round. Here, `da` represents the choice of the environment for this round and is introduced earlier in the code.

**Section NonBivalent.**

**Variable** `cfg`: `configuration`.

**Hypothesis** `Hbivalent`: $
eg$ bivalent `cfg`.
**Lemma** `round_simplify_Lights`: $\forall id, getLight (round gatherR2 da cfg id) \equiv getLight (cfg id). 
**Proof...**

Notice that we need to repeat neither the configuration `config` nor the hypothesis `bivalent config` in the statement of lemma `round_simplify_Lights`.

<figure><img src="image_3.png" /><figcaption>**Fig. 2.** Reachability graph for the categories of observations. In blue, `CB` and `Biv` refer to the Color-Bivalent and Bivalent configurations respectively. In black, the different non-bivalent cases identified in the algorithm of Courtieu et al. [10], with self-loops omitted in the non-bivalent cases. The boxed area contains the triangle cases, all linked to `Maj`.</figcaption></figure>

**Exhaustive case analyses.** Secondly, the proof explains how a configuration may evolve from one class to another by a careful and exhaustive case analysis. This proof of exhaustivity is a significant effort; although it can be done in only 50 lines of code for the bivalent case as it always evolves either to itself or to a non-bivalent case, the proof for the color-bivalent case is considerably harder (more than 600 lines of code). We identify five sub-cases: one leading to a color bivalent configuration (all active robots are `BLACK` and the same number is activated on both towers), two leading to a bivalent but not color bivalent configuration (all active robots are `BLACK` but a different number is activated on each tower; all robots are `WHITE` and a full tower is activated), and two leading to a non-bivalent configuration (all robots are `WHITE` and more than a full tower moves; some robot does not move on each tower and some robot moves). Getting this exact case distinction correct is tricky and the proof assistant helps a lot in making sure one does not forget a corner case.
The various configuration classes used in the proof of correctness are pre-
sented in Figure 2, where a directed arrow from one class of configuration to
another denotes the possibility to change the current configuration class by exe-
cuting the algorithm. Since the selection of robots that execute their algorithm
in a given configuration is decided by an adversary, there may be more than one
outgoing arrow in some configuration classes. The classes in black color corre-
spond to those identified by Courtieu et al. [10], while the two new vertices: CB
(for color-bivalent) and Biv (for bivalent) correspond to new possibilities implied
by the algorithm being self-stabilizing.

**Termination through measure decrease.** Thirdly, it remains to show that along any execution of our algorithm, the successive resulting configurations follow a finite path in this graph that ends up in state Gathered. This result is obtained with an extension of the measure used by Courtieu *et al.* [10]. The *weight* of an observation *s* is a pair of natural numbers, compared lexicographically, such that the first one is the weight of the corresponding phase *p* of the algorithm, and the second one is the result of a phase-weight function *w*<sub>*p*</sub> on the observation. We give to CB and Biv weights greater than for the other phases, with a maximum weight to phase CB. In our case, it is enough to give a weight of 8 to CB and 7 to Biv. Function *w*<sub>Biv</sub> is unnecessary as fairness forces the eventual activation of a robot that changes its state, meaning in this particular case that we end up with a tower strictly higher than the other. We may as well choose the constant function 0. Function *w*<sub>CB</sub> is simply the number of robots with their light set to BLACK in the observation. Remember that only robots with their light set to WHITE can change location. Obtaining a bivalent configuration after one round is thus either

- activating robots that move to create another tower, and exhaust one of the original towers. This means that all robots at a location were moving, hence all with their light set to WHITE. A resulting *bivalent* configuration consists thus of a tower with only lights set to BLACK, and a tower untouched hence with lights set to WHITE, otherwise the original configuration would not have been color bivalent. This resulting configuration is not color-bivalent.

- activating robots that don't move (i.e. just switch their light color) but in that case, they have to be activated in the same number on both locations otherwise we lose color bivalence.

The only way to stay in CB is indeed to activate the same number of robots
with light set to BLACK in each tower.

Let us call oldwick the weighting function of Courtieu et al. [10], the
global measure is then defined as:

Function measure (obs : observation) : nat * nat :=
  if bivalentobs obs then
    if color_bivalentobs obs then (8, count_black obs)
    else (7, 0)
      (* By fairness eventually jumps to a maj tower case. *)
  else oldwick (fst obs).
      (* Courtieu et al.'s measure on lightless obs *)
The ordering defined by the lexicographic comparison of the left then right members of these weights is proven to be well-founded.

The arcs in the graphs of Figure 2 are proven to be all the arcs that can be.

Finally, we can show that the measure of the observation of a resulting configuration is always less than the measure of the observation of the initial configuration provided at least one robot changes state. Then, the proof of the main theorem consists in two nested well-founded inductions: the first one is about fairness ensuring that eventually some robot changes state, and the second one is on the decrease of the chosen measure.

## 4.3 Modification to the formal proof of Courtieu et al. ([10])

It is interesting to notice that the changes required to the proof of the non-bivalent case borrowed from Courtieu et al. [10] are minimal, demonstrating the effectiveness of code reusability with the PACTOLE framework. In particular, by preserving the original observation used as a component inside ours, and using the same notation !! config to refer to this component, the change of observation is completely transparent for the old proof.

The main change to the proof of Courtieu et al. [10] is the fact that a robot changing its state is not necessarily moving, it may change only its light color. In particular, this is the case for BLACK robots in a color-bivalent configuration. Because of that, we need to replace moving robots with changing ones in several theorem statements. In particular, the fairness of the demon is now used to ensure that eventually, some robot changes its state:

**Theorem** OneMustChange : ∀ config id,
(* Assuming the configuration is not gathered, ... *)
¬gathered_at (get_location (config id)) config →
(* then, there is a robot gmove that, ... *)
∃ gmove, ∀ da, SSYNC_da da →
(* if it is activated by any SSYNC demon, ... *)
List.In gmove (active da) →
(* then its state changes. *)
List.In gmove (changing gatherR2 da config).

The difference in the definitions of moving and changing only lies in the test: in changing we consider the full state of the robots (including their color) whereas in moving we only consider their location.

**Definition** moving rbg da config :=
List.filter
(fun id ⇒ negb (get_location (round rbg da config id)
≡ b get_location (config id)))
names.

**Definition** changing r da config :=
List.filter
(fun id ⇒ negb (round r da config id ≡ b config id))
names.
Nevertheless, we can reuse most of the previous proofs as is because lights
are only modified in the color-bivalent case. We can actually prove that moving
robots and changing robots are the same whenever the configuration is not color-
bivalent:

**Lemma** *changing_eq_moving : ∀ config, ¬color_bivalent config → changing gatherR2 da config = moving gatherR2 da config.*

4.4 Final statement and assumptions of the proof

Denoting as a similarity_demon a demon where the local frame of reference
it provides is centered on the observing robot, the full statement of the final
theorem we prove is :

**Theorem** Gathering_in_R2 : ∀ d : similarity_demon,
(* For any SSYNC fair demon *)
SSYNC (d : demon) → Fair d →
(* the gatherR2 algorithm solves the gathering problem. *)
FullSolGathering gatherR2 d.

That is: for any demon d, if d is in the SSYNC relation (i.e., is semi-synchronous) then if d is in the Fair relation (i.e., is fair) then FullSolGathering holds for our algorithm and d. Put simply: any execution based on a fair SSYNC demon of our algorithm will eventually lead, from any configuration, to a situation where all robots are, and stay, gathered at a certain location. As previously noted, the initial configuration is truly arbitrary: no assumption is made about the initial placement of the robots, or the initial light color of the robots. So, our algorithm is self-stabilizing.

Using Print Assumptions Gathering_in_R2, we can list the 15 axioms that our formal proof relies on. Interestingly, they are exactly the same as the ones of the proof of Courtieu et al. [10], meaning that our extension does not add any additional axiom. These axioms can be described as follows:

- The axiomatic description of $\mathbb{R}$ from Coq's standard library (3 axioms);

- An axiomatic description of the smallest enclosing circle together with its properties (8 axioms);

- Geometric properties:

- Properties of the barycenter of 3 points (3 axioms);

- Through three points, at most a single circle can be drawn.

**Proof effort** The proof effort in this development remains manageable. Defining
observations with lights and the relevant contexts amounts to about 300 lines of
specifications and 1000 lines of actual proof in WithMultiplicityLight.v in
the companion code repository.

Regarding the definition of our new algorithm with the complete proof of
its correctness and universality, the file Algorithm_withLight.v stretches to
about 1100 lines of specifications and 5240 lines of proof. Remember though that
this includes for a significant part the proofs of Courtieu et al. [10] reformulated
to handle observations with lights.

Other changes to improve the Pactole framework are minor: renaming the
moving property into changing, introducing moving and stationary into the
file Core/Formalism.v and propagating the renaming to the original algo-
rithm [10]; introducing two predicates on\_loc and occupied to better distin-
guish robots and their locations in the file Core/Configurations.v.

5 Concluding remarks

We presented the first fully-self-stabilizing (no constraints are put on the number
of robots or on the initial configuration) deterministic uniform gathering algo-
rithm for robots operating in the semi-synchronous Look-Compute-Move model.
Our execution model, algorithm description, and correctness proof all use a com-
mon formal language, ensuring confidence in the claimed results. A byproduct
of our approach lies in the adapt and reuse techniques we employed to build
upon previously published formal developments in the PACTOLE framework. We
believe that future work will also be able to further develop the code we provide
to the community.

The most obvious open question raised by our work is the extension of the
positive result to weaker scheduling constraints, namely the ASYNC execution
model. On the one hand, the possibility for two robots to gather in this set-
ting [13] hints at a positive outcome. On the other hand, the inability to directly
scale the model-checking solution of Defago et al. [13] implies that many ad-
ditional formal developments to the PACTOLE framework are necessary, as its
support for the ASYNC model is still in early stage of development [2] (in par-
ticular, a number of basic lemmas are missing in this model).

References

1. Yuichi Asahiro and Masafumi Yamashita. Minimum algorithm sizes for self-stabilizing gathering and related problems of autonomous mobile robots (extended abstract). In Shlomi Dolev and Baruch Schieber, editors, *Stabilization, Safety, and Security of Distributed Systems - 25th International Symposium, SSS 2023, Jersey City, NJ, USA, October 2-4, 2023, Proceedings*, volume 14310 of *Lecture Notes in Computer Science*, pages 312–327. Springer, 2023. doi:10.1007/978-3-031-44274-2\_23.

2. Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Continuous vs. discrete asynchronous moves: A certified approach for mobile robots. In Mohamed Faouzi Atig and Alexander A. Schwarzmann, editors, *Networked Systems - 7th International Conference, NETYS 2019, Marrakech, Morocco, June 19-21, 2019, Revised Selected Papers*, volume 11704 of *Lecture Notes in Computer Science*, pages 93–109. Springer, 2019. doi:10.1007/978-3-030-31277-0\_7.

3. Thibaut Balabonski, Amélie Delga, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Synchronous gathering without multiplicity detection: a certified
algorithm. *Theory Comput. Syst.*, 63(2):200-218, 2019. doi:10.1007/S00224-017-9828-z.

4. Andrej Bauer. How to review formalized mathematics. Blog post, August 2013. http://math.andrej.com/2013/08/19/how-to-review-formalized-mathematics/.

5. Béatrice Bérard, Pascal Lafourcade, Laure Millet, Maria Potop-Butucaru, Yann Thierry-Mieg, and Sébastien Tixeuil. Formal verification of mobile robot protocols. *Distributed Comput.*, 29(6):459-487, 2016. doi:10.1007/S00446-016-0271-1.

6. Yves Bertot and Pierre Castéran. *Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions*. Texts in Theoretical Computer Science. Springer, 2004. URL: http://www.labri.fr/publications/13a/2004/BC04.

7. Quentin Bramas and Sébastien Tixeuil. Wait-free gathering without chirality. In Christian Scheideler, editor, *Structural Information and Communication Complexity - 22nd International Colloquium, SIROCCO 2015, Montserrat, Spain, July 14-16, 2015, Post-Proceedings*, volume 9439 of *Lecture Notes in Computer Science*, pages 313-327. Springer, 2015. doi:10.1007/978-3-319-25258-2\_22.

8. Mark Cieliebak, Paola Flocchini, Giuseppe Prencipe, and Nicola Santoro. Distributed computing by mobile robots: Gathering. *SIAM J. Comput.*, 41(4):829-879, 2012. doi:10.1137/100796534.

9. Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Impossibility of gathering, a certification. *Inf. Process. Lett.*, 115(3):447-452, 2015. doi:10.1016/J.IPL.2014.11.001.

10. Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Certified universal gathering in $\mathbb{R}^2$ for oblivious mobile robots. In Cyril Gavoille and David Ilcinkas, editors, *Distributed Computing - 30th International Symposium, DISC 2016, Paris, France, September 27-29, 2016. Proceedings*, volume 9888 of *Lecture Notes in Computer Science*, pages 187-200. Springer, 2016. doi:10.1007/978-3-662-53426-7\_14.

11. Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Swarms of Mobile Robots: Towards Versatility with Safety. *Leibniz Transactions on Embedded Systems*, 8(2):02:1-02:36, 2022. URL: https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.2, doi:10.4230/LITES.8.2.2.

12. Shantanu Das, Paola Flocchini, Giuseppe Prencipe, Nicola Santoro, and Masafumi Yamashita. Autonomous mobile robots with lights. *Theor. Comput. Sci.*, 609:171-184, 2016. doi:10.1016/J.TCS.2015.09.018.

13. Xavier Défago, Adam Heriban, Sébastien Tixeuil, and Koichi Wada. Using model checking to formally verify rendezvous algorithms for robots with lights in euclidean space. *Robotics Auton. Syst.*, 163:104378, 2023. doi:10.1016/J.ROBOT.2023.104378.

14. Xavier Défago, Maria Potop-Butucaru, and Philippe Raipin Parvédy. Self-stabilizing gathering of mobile robots under crash or byzantine faults. *Distributed Comput.*, 33(5):393-421, 2020. doi:10.1007/S00446-019-00359-x.

15. Yoann Dieudonné and Franck Petit. Self-stabilizing gathering with strong multiplicity detection. *Theor. Comput. Sci.*, 428:47-57, 2012. doi:10.1016/J.TCS.2011.12.010.

16. Edsger W. Dijkstra. Self-stabilizing systems in spite of distributed control. *Commun. ACM*, 17(11):643-644, 1974. doi:10.1145/361179.361202.
17. Ha Thi Thu Doan, François Bonnet, and Kazuhiro Ogata. Model checking of robot gathering. In James Aspnes, Alysson Bessani, Pascal Felber, and João Leitão, editors, 21st International Conference on Principles of Distributed Systems, OPODIS 2017, Lisbon, Portugal, December 18-20, 2017, volume 95 of LIPIcs, pages 12:1-12:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPICS.OPODIS.2017.12.

18. Paola Flocchini. Gathering. In Paola Flocchini, Giuseppe Prencipe, and Nicola Santoro, editors, *Distributed Computing by Mobile Entities, Current Research in Moving and Computing*, volume 11340 of *Lecture Notes in Computer Science*, pages 63–82. Springer, 2019. doi:10.1007/978-3-030-11072-7_4.

19. Keita Nakajima, Kaito Takase, and Koichi Wada. Efficient self-stabilizing simulations of energy-restricted mobile robots by asynchronous luminous mobile robots. In Yuval Emek, editor, *Structural Information and Communication Complexity - 31st International Colloquium, SIROCCO 2024, Vietri sul Mare, Italy, May 27-29, 2024, Proceedings*, volume 14662 of *Lecture Notes in Computer Science*, pages 494–500. Springer, 2024. doi:10.1007/978-3-031-60603-8_28.

20. Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hrițcu, Vilhelm Sjöberg, and Brent Yorgey. *Logical Foundations*. Software Foundations series, volume 1. Electronic textbook, May 2025. URL: https://softwarefoundations.cis.upenn.edu/lf-current/index.html.

21. Giuseppe Prencipe. Impossibility of gathering by a set of autonomous mobile robots. *Theor. Comput. Sci.*, 384(2-3):222-231, 2007. doi:10.1016/J.TCS.2007.04.023.

22. Arnaud Sangnier, Nathalie Sznajder, Maria Potop-Butucaru, and Sébastien Tixeuil. Parameterized verification of algorithms for oblivious robots on a ring. *Formal Methods Syst. Des.*, 56(1):55-89, 2020. doi:10.1007/S10703-019-00335-Y.

23. Ichiro Suzuki and Masafumi Yamashita. Distributed anonymous mobile robots: Formation of geometric patterns. *SIAM J. Comput.*, 28(4):1347-1363, 1999. doi: 10.1137/S009753979628292X.

24. Satoshi Terai, Koichi Wada, and Yoshiaki Katayama. Gathering problems for autonomous mobile robots with lights. *Theor. Comput. Sci.*, 941:241-261, 2023. URL: https://doi.org/10.1016/j.tcs.2022.11.018, doi:10.1016/J.TCS.2022.11.018.

25. Giovanni Viglietta. Rendezvous of two robots with visible bits. In Paola Flocchini, Jie Gao, Evangelos Kranakis, and Friedhelm Meyer auf der Heide, editors, *Algorithms for Sensor Systems - 9th International Symposium on Algorithms and Experiments for Sensor Systems, Wireless Networks and Distributed Robotics, ALGOSENSORS 2013, Sophia Antipolis, France, September 5-6, 2013, Revised Selected Papers*, volume 8243 of *Lecture Notes in Computer Science*, pages 291-306. Springer, 2013. doi:10.1007/978-3-642-45346-5_21.