# Comment se rassembler (avec certitude) quand on est confus et désorienté

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.. Comment se rassembler (avec certitude) quand on est confus et désorienté. ALGOTEL 2025 – 27èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications, Jun 2025, Saint Valery-sur-Somme, France. hal-05002153

HAL Id: hal-05002153

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

Submitted on 14 Apr 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
# Comment se rassembler (avec certitude)
quand on est confus et désorienté

François Bonnet¹ et Quentin Bramas² et Pierre Courtieu³ et Xavier Défago¹
et Lionel Rieg⁴ et Sébastien Tixeuil⁵ et Xavier Urbain⁶

¹Institute of Science Tokyo, ²Université de Strasbourg, ³CNAM, CEDRIC, ⁴Grenoble INP ENSIMAG, VERI-MAG, ⁵Sorbonne Université, LIP6, IUF ⁶Université Lyon 1, LIRIS

Nous considérons le problème du rassemblement en temps fini et au même endroit, non connu à l'avance, d'un ensemble de robots déterministes semi-synchrones dans le plan euclidien, partant d'une configuration initiale arbitraire qui peut même être bivalente (c'est-à-dire une configuration où les robots sont répartis également sur deux emplacements différents). Ce problème est connu pour être insoluble lorsque les robots sont oublieux, c'est-à-dire lorsqu'ils ne peuvent pas se souvenir de leurs actions passées. Nous présentons un algorithme de rassemblement déterministe où les robots peuvent retenir et communiquer un bit de mémoire. Ce bit peut être arbitrairement défini dans la configuration initiale. Notre solution est donc optimale en termes de mémoire et auto-stabilisante. Sa preuve de correction est formellement certifiée par l'assistant de preuve Coq en utilisant la bibliothèque Pactole.

**Mots-clefs** : Robots mobiles, Méthodes formelles, Rassemblement, Auto-stabilisation

## 1 Introduction

Les réseaux de robots mobiles ont suscité un intérêt considérable en raison de leur large éventail d'applications potentielles, notamment les opérations de recherche et de sauvetage et la surveillance des environnements dangereux. Dans le modèle classique utilisé pour étudier mathématiquement ces essais robotiques [SY99], les robots fonctionnent en cycles Observer-Calculer-se Déplacer (OCD). Dans chaque cycle, un robot observe son environnement pour acquérir les positions des autres robots, calcule une destination en fonction de cette observation, puis se déplace vers l'emplacement calculé.

Les robots oublieux exécutent ces cycles sans conserver la mémoire de leurs actions passées. En revanche, les robots lumineux peuvent conserver et échanger une quantité constante d'informations, représentée par une lumière individuelle visible par les autres robots dont la couleur peut être modifiée par le robot hôte. L'exécution est influencée par le niveau de synchronisation entre les robots. Ici, nous nous concentrons sur le modèle semi-synchrone (SSYNC), où l'exécution est découpée en rondes et, à chaque ronde d'exécution, un sous-ensemble non-vide de robots effectue un cycle complet, avec un ordonnanceur équitable.

Les robots sont anonymes, exécutent le même algorithme et peuvent être désorientés, ce qui signifie que leurs observations sont interprétées à travers des systèmes de coordonnées locaux qui peuvent ne pas s'aligner avec ceux des autres robots. En particulier, il n'y a pas de système de coordonnées commun ni de chiralité commune. Une propriété attrayante pour résister aux pannes transitoires est l'auto-stabilisation, qui autorise les robots à commencer à partir de positions initiales arbitraires, y compris des configurations avec des points où plusieurs robots partagent la même position, et pour les robots lumineux, où leur mémoire peut être initialement définie de manière arbitraire.

Dans cet article, nous abordons le problème fondamental de rassembler ces robots à partir d'une configuration arbitraire en un temps fini vers un emplacement unique, inconnu à l'avance, et de les y maintenir. Malgré sa simplicité apparente, ce problème partant d'une configuration initiale bivalente (où les robots sont également répartis sur deux positions distinctes) est impossible à résoudre dans le modèle SSYNC par des robots oublieux [SY99]. Pour surmonter cette impossibilité, plusieurs hypothèses ont été explorées dans des recherches antérieures. Par exemple, Dieudonné et al. [DP12] ont supposé un nombre impair de
<table><caption>**TABLE 1:** Une comparaison de notre algorithme avec les solutions auto-stabilisantes existantes dans le modèle SSYNC et [CRTU16] (les propriétés les plus souhaitables sont en gras).</caption><thead><tr><th>Référence</th><th>Taille</th><th>Déterministe</th><th>Uniforme</th><th>Preuve</th><th>Oublieux</th><th>Auto-stabilisant</th></tr></thead><tbody><tr><td>[DP12]</td><td>n est impair</td><td>oui</td><td>oui</td><td>papier et crayon</td><td>oui</td><td>oui</td></tr><tr><td>[Vig13]</td><td>n = 2</td><td>oui</td><td>oui</td><td>papier et crayon</td><td>non</td><td>oui</td></tr><tr><td>[CRTU16]</td><td>arbitraire</td><td>oui</td><td>oui</td><td>assistant de preuve</td><td>oui</td><td>non</td></tr><tr><td>[DPP20]</td><td>arbitraire</td><td>non</td><td>oui</td><td>papier et crayon</td><td>oui</td><td>oui</td></tr><tr><td>[AY23]</td><td>arbitraire</td><td>oui</td><td>non</td><td>papier et crayon</td><td>oui</td><td>oui</td></tr><tr><td>Cet article</td><td>arbitraire</td><td>oui</td><td>oui</td><td>assistant de preuve</td><td>non</td><td>oui</td></tr></tbody></table>

robots, empêchant la formation d'une configuration bivalente. Défago et al. [DPP20] utilisent un algorithme probabiliste pour résoudre les situations symétriques, mais la correction de l'algorithme n'est pas garantie dans toutes les exécutions. Plus récemment, Asahiro et al. [AY23] ont exploré l'utilisation de robots déterministes qui n'exécutent pas tous le même algorithme, prouvant que deux algorithmes distincts sont à la fois nécessaires et suffisants. En résumé, dans le contexte oublieux, le rassemblement nécessite de faire des compromis sur la flexibilité [DP12], les garanties déterministes [DPP20], ou l'uniformité [AY23]. Dans le contexte des robots lumineux, une solution auto-stabilisée déterministe existe pour deux robots et deux couleurs dans le modèle SSYNC [Vig13], interrogeant la possibilité d'une solution à $n \ge 2$ robots.

**Notre Contribution.** Nous concevons et prouvons la correction d'un algorithme de rassemblement déterministe auto-stabilisant qui utilise deux couleurs par lumière (une seule couleur équivaut à exiger que les robots soient oublieux, rendant ainsi le problème impossible à résoudre). Une propriété remarquable de notre approche réside dans l'utilisation de méthodes formelles pour évaluer la correction de notre algorithme, et nous utilisons la bibliothèque PACTOLE et l'assistant de preuve CoQ. Si les preuves assistées sont correctes par construction et n'ont donc pas besoin d'une relecture manuelle par la communauté, il convient de s'assurer que les énoncés formels correspondent aux résultats revendiqués. En particulier, les définitions formelles et les énoncés finaux des théorèmes dans CoQ doivent être soigneusement vérifiés pour s'assurer que le développement formel fournit bien les preuves des propriétés pertinentes†. Le code source complet de notre développement formel (pour CoQ 8.19 et 8.20) est disponible à l'URL suivante : https://pactole.liris.cnrs.fr.

Une comparaison générale de notre solution avec les travaux précédents est présentée dans la Table 1.

## 2 Notre Algorithme

On suppose des robots lumineux qui peuvent retenir et communiquer deux couleurs (NOIR et BLANC). Le terme de tour désigne un empilement de robots sur la même position. L'algorithme distingue l'observation de configurations couleur-bivalentes, bivalentes (mais non couleur-bivalente), ou non bivalentes. Une configuration couleur-bivalente consiste en deux tours de taille égale à des emplacements distincts, avec autant de robots NOIRS et BLANCS dans chaque tour. Le pseudo-code utilisé pendant la phase de calcul (qui retourne la nouvelle position et la nouvelle couleur de la lumière) est défini dans l'Algorithme 1. Il utilise une variable binaire $c$ pour stocker la couleur courante, des fonctions pour vérifier si l'observation obs est bivalente ou couleur-bivalente, avec $bivalentobs$ et $color_bivalentobs$ respectivement. Les fonctions middle et find_max_black sont utilisées pour calculer des points particuliers de l'observation comme destinations, respectivement le milieu des deux tours et la tour avec le plus grand nombre de robots NOIRS. Enfin, la fonction gatherR2_old_pgm exécute l'algorithme de Courtieu et al. [CRTU16], qui suppose une configuration non-bivalente pour effectuer le rassemblement.

La figure 1 propose trois exécutions possibles $E_1$, $E_2$ et $E_3$ à partir de configurations couleur-bivalentes. Dans $E_1$, un seul robot NOIR est d'abord activé, de sorte qu'ensuite, le nombre de robots NOIRS diffère sur chaque tour, et la configuration n'est plus couleur-bivalente (mais reste bivalente). Chaque robot activé se déplace alors vers la tour comprenant le plus de robots NOIRS. Dans $E_2$, un robot BLANC est activé dans l'une des tours. Ici, indépendamment de l'activation des robots NOIRS, la configuration obtenue contient

<footnote>†. À ce sujet nous recommandons la lecture de l'excellent article de blog de Andrej Bauer : https://math.andrej.com/2013/08/19/how-to-review-formalized-mathematics/.</footnote>
<caption>**Algorithm 1:** Exécuté par un robot avec l'observation *obs*</caption>

```
if bivalentobs(obs) then
    if colorbivalentobs(obs) then
        if c == BLANC then
            return (middle(obs), NOIR)
        else
            return ((0, 0), BLANC)
    else
        return (find_max_black(obs), c)
else
    exécuter gatherR2_old_pgm(obs)
```

<figure><img src="image_2.png" /><figcaption>**FIGURE 1 :** Exemples d'exécution à partir de configuration couleur-bivalentes</figcaption></figure>

trois points et n'est donc pas bivalente. Ensuite, l'exécution de l'algorithme oublieux pour les configurations non bivalentes garantit que les robots finissent par se rassembler en un seul point. Dans $E_3$, tous les robots sont BLANCS. Si tous sont exécutés, ils se déplacent vers le milieu et forment un point de multiplicité unique. Si seul un sous-ensemble strict de l'une des tours est activé, alors la configuration obtenue contient trois points et la configuration n'est plus bivalente. Sinon, comme dans $E_3$, si une tour est activée et pas l'autre, la configuration obtenue est bivalente mais l'une des tours ne contient que des robots NOIRS, et l'autre des robots BLANCS, donc la configuration n'est plus couleur-bivalente et les robots se rassemblent ultimement.

## 3 Survol de la preuve

Nous instancions tout d'abord les couleurs avec des valeurs booléennes, *true* étant BLANC, et *false* étant NOIR. Nous pouvons maintenant définir l'état d'un robot comme étant un couple ordonné de type `location*L` composé de sa position actuelle et de la couleur de sa lumière. Pour réutiliser l'algorithme de Courtieu *et al.* [CRTU16] avec le moins de travail d'adaptation possible, nous conservons leur type d'observation original (un multiensemble de positions). Cependant, dans notre modèle, les robots ont des lumières et peuvent les observer, y compris les leurs. Nous définissons donc la nouvelle observation comme une paire, avec l'observation de Courtieu *et al.* [CRTU16] comme premier élément, et un enregistrement composé de la couleur de la lumière de l'observateur et d'un multiensemble de positions et de couleurs de lumière comme second élément. Puis, nous prouvons la cohérence entre l'observation avec lumières et celle sans une fois pour toutes, sans modifier l'algorithme de Courtieu *et al.* [CRTU16], pour adapter facilement les résultats précédents. Le développement formel lui-même se compose de deux étapes principales.

Premièrement, nous définissons une observation prenant en compte les lumières. Pour rester cohérent avec tous les développements précédents sur ce sujet, nous utilisons les définitions formelles des propriétés de rassemblement de la bibliothèque PACTOLE. En particulier, la relation `Gather pte e` signifie qu'à toutes les rondes d'une exécution (infinie) *e*, les robots sont rassemblés au même endroit (inchangé) *pt* et la
relation WillGather est signifie que l'exécution (infinie) est ultimement dans Gather pour un certain pt.
La définition d'une solution pour le rassemblement est donc la suivante :

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

Un algorithme rbg est une solution au rassemblement pour un ordonnancement d si, pour toute configuration config, l'exécution conduit ultimement à une configuration rassemblée. La principale différence par rapport à la solution de Courtieu et al. [CRTU16] est que notre proposition actuelle ne pose aucune condition sur la configuration : elle est quantifiée universellement.

Deuxièmement, nous proposons notre nouvel algorithme `gatherR2` et, en particulier, nous établissons formellement que pour tout ordonnancement semi-synchrone équitable et à partir de toute configuration, chaque exécution conduit ultimement à une configuration où tous les robots sont (et restent) rassemblés. Ce développement se trouve dans le fichier `CaseStudies/Gathering/InR2/Algorithm_withLight.v` dans l'archive de code, ainsi que l'adaptation des résultats de l'algorithme original de Courtieu et al. [CRTU16].

La preuve formelle elle-même est organisée en trois sections, correspondant aux configurations couleur-bivalentes, bivalentes, et non-bivalentes. Chacune de ces sections contient, en particulier, les hypothèses générales qui la définissent, et des versions spécialisées de certains lemmes. Par exemple : une hypothèse évidente dans la section NonBivalent est que la configuration considérée n'est effectivement pas bivalente, et nous pouvons affirmer (et prouver) que dans ce cas, les lumières des robots ne changent pas au cours de l'exécution (car l'algorithme oublieux est utilisé à partir d'une telle configuration). L'énoncé complet du théorème final que nous prouvons est :

**Theorem** Gathering_in_R2 : V d : similarity_demon, SSYNC (d : demon) → Fair d → FullSolGathering gatherR2 d.

C'est-à-dire : pour tout ordonnancement d, si d est dans la relation SSYNC (c'est-à-dire, est semi-synchrone) alors si d est dans la relation Fair (c'est-à-dire, est équitable) alors FullSolGathering est vérifié pour notre algorithme et d. En termes simples : toute exécution basée sur un ordonnancement SSYNC équitable de notre algorithme conduira finalement, à partir de toute configuration, à une situation où tous les robots sont, et restent, rassemblés à un certain endroit.

## 4 Conclusion

Nous avons présenté et prouvé formellement en Coq le premier algorithme auto-stabilisant de rassemblement d'un nombre arbitraire de robots lumineux dans le modèle SSYNC. Par ailleurs, le nombre de couleurs utilisé est optimal. En listant les 15 axiomes sur lesquels repose notre preuve formelle, nous constatons qu'ils sont identiques à ceux de Courtieu et al. [CRTU16], ce qui signifie que notre extension n'ajoute aucun axiome supplémentaire. L'effort de preuve dans ce développement reste gérable. La définition des observations avec lumières et des contextes pertinents représente environ 300 lignes de spécifications et 1000 lignes de preuve réelle dans WithMultiplicityLight.v. En ce qui concerne la définition de notre nouvel algorithme avec la preuve complète de sa correction et de son universalité, le fichier Algorithm_withLight.v s'étend sur environ 1100 lignes de spécifications et 5240 lignes de preuve (incluant en grande partie les preuves de Courtieu et al. [CRTU16] reformulées pour gérer les observations avec lumières).

## Références

[AY23] Y Asahiro and M Yamashita. Minimum algorithm sizes for self-stabilizing gathering and related problems of autonomous mobile robots. In SSS 2023, volume 14310, pages 312–327, 2023.

[CRTU16] P Courtieu, L Rieg, S Tixeuil, and X Urbain. Certified universal gathering in $\mathbb{R}^2$ for oblivious mobile robots. In DISC 2016, volume 9888, pages 187–200, 2016.

[DP12] Y Dieudonné and F Petit. Self-stabilizing gathering with strong multiplicity detection. Theor. Comput. Sci., 428:47–57, 2012.

[DPP20] X Défago, M Potop-Butucaru, and P Raipin Parvédy. Self-stabilizing gathering of mobile robots under crash or byzantine faults. Distributed Comput., 33(5):393–421, 2020.

[SY99] I Suzuki and M Yamashita. Distributed anonymous mobile robots : Formation of geometric patterns. SIAM J. Comput., 28(4):1347–1363, 1999.

[Vig13] G Viglietta. Rendezvous of two robots with visible bits. In ALGOSENSORS 2013., volume 8243, pages 291–306, 2013.