Rendez-vous au

Point-Dont-On-Ne-Doit-Pas-Calculer-Les-Coordonnées

Maria-Virginia Aponte, Mathis Bouverot-Dupuis, Quentin Bramas, Pierre

Courtieu, Lionel Rieg, Xavier Urbain

► To cite this version:

Maria-Virginia Aponte, Mathis Bouverot-Dupuis, Quentin Bramas, Pierre Courtieu, Lionel Rieg, et al.. Rendez-vous au Point-Dont-On-Ne-Doit-Pas-Calculer-Les-Coordonnées. ALGOTEL 2025 – 27èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications, Jun 2025, Saint Valery-sur-Somme, France. hal-05002157

HAL Id: hal-05002157

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

Submitted on 13 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
# Rendez-vous au Point-Dont-On-Ne-Doit-Pas-Calculer-Les-Coordonnées

Virginia Aponte¹, Mathis Bouverot-Dupuis¹,⁴, Quentin Bramas²,³, Pierre Courtieu¹, Lionel Rieg⁵, et Xavier Urbain⁶

¹CÉDRIC, Conservatoire des arts et métiers ²ICUBE, Université de Strasbourg, CNRS ³LIP6, Sorbonne Université, CNRS ⁴ENS, École normale supérieure Paris ⁵VERIMAG, Grenoble-INP – UGA, CNRS ⁶LIRIS, Université Lyon 1, CNRS

Le point Weber, aussi appelé médian géométrique, a toujours eu mauvaise réputation dans les travaux sur les robots mobiles. La raison invoquée est qu'il n'est pas constructible, mais tout le monde sait que la vraie raison est qu'il offre une solution triviale au problème du regroupement, supprimant ainsi la possibilité de publier des protocoles compliqués dans des journaux réputés. Est-ce cependant vraiment le cas ? Maintenant que les protocoles compliqués sont publiés, nous montrons qu'en fait, le point Weber, bien que non constructible par un robot muni d'un compas et d'une règle, n'est pas une solution triviale (une destination inconditionnelle).

Dans cet article, nous présentons un protocole non trivial utilisant le point Weber pour regrouper dans le plan euclidien un nombre quelconque de robots ne se trouvant pas initialement dans une configuration impossible à résoudre (bivalente) pour un modèle d'exécution asynchrone (sans hypothèses d'ordonnancement des cycles ni sur l'achèvement des déplacements) et non rigide (les déplacements peuvent être interrompus). Le point Weber et ses propriétés, ainsi que la correction de notre protocole sont prouvés en Coq, grâce à la bibliothèque PACTOLE.

**Mots-clefs** : Robots mobiles, Point Weber, Problème du rassemblement, Ordonnancement Asynchrone

## 1 Introduction

Le problème du rassemblement dans le plan 2D est une question centrale du domaine des essais de robots autonomes, avec des applications en robotique collective et en algorithmique distribuée. Dans le modèle Look/Compute/Move (LCM) [SY99], les robots observent leur environnement, effectuent un calcul fondé sur ces observations, puis se déplacent en conséquence. L'un des défis majeurs réside dans la prise en compte d'un cadre asynchrone et non rigide, où les robots peuvent être interrompus en plein mouvement et doivent s'adapter à des observations potentiellement absolues.

Le point Weber, qui minimise la somme des distances aux positions des robots, semble une solution naturelle pour le rassemblement car il présente des propriétés géométriques favorables. Il est cependant généralement écarté avec deux arguments principaux : « le point Weber n'est pas calculable dans le cas général » [Cie+12] et « son utilisation rend le problème de rassemblement trivial » [FW24].

Le problème de la calculabilité du point Weber peut facilement être mis de côté car les robots effectuent déjà des opérations non calculables sur les nombres réels, pour se déplacer et pour calculer des destinations (pour viser le milieu par exemple), certains protocoles se permettant également de trisecter les angles...

Quant à la trivialité des solutions, rappelons qu'un point Weber d'un multi-ensemble $\mathcal{P}$ de points de $\mathbb{R}^2$ (multi-ensemble car plusieurs robots peuvent occuper la même position) est défini comme le point, ou l'ensemble des points, minimisant la somme des distances à tous les points de $\mathcal{P}$. Une propriété importante est que le point Weber est invariant lorsque les points de $\mathcal{P}$ se déplacent vers lui en ligne droite, ce qui en fait un excellent choix pour un point de rassemblement. De ce fait, chaque robot à une position de $\mathcal{P}$ peut s'activer et se déplacer de manière indépendante (et asynchrone) vers le point Weber sans impacter les mouvements des autres robots. Cette approche, largement évoquée dans la littérature et acceptée comme une évidence algorithmique [FW24], n'est pourtant pas correcte, car le point Weber n'est pas toujours unique
**protocole 1:** Rassemblement utilisant le point Weber

si unique point Weber w alors retourner w ;

sinon l'ensemble des points Weber est un segment, soient $w_1, w_2 \in \mathcal{P}$ ses extrémités;

les points de $\mathcal{P}$ sont alignés, soient $s_1, s_2 \in \mathcal{P}$ les extrémités de ce segment et M son milieu;

si une position m contient la moitié des points et ] (0,0), m[ non occupé alors retourner m ;

si $(0,0) \notin \{w_1, w_2\}$ alors retourner $(0,0)$ ;

si $M \in [w_1, w_2]$ alors retourner $M$ ;

Sans perte de généralité, on peut supposer que $w_1$ est situé entre $M$ et $w_2$;

si $(0,0) = w_2$ alors retourner $w_1$ ;

retourner (0,0);

<caption>**FIGURE 1 :** Description informelle du protocole</caption>

(cf. paragraphe 2). Ainsi, si les robots ne choisissent pas le même point Weber, cette stratégie algorithmique échoue !

**Contributions.** Nous proposons un protocole formel de rassemblement dans le plan 2D sans obstacle dans un cadre asynchrone avec déplacements non rigides, où chaque robot exécute son cycle LCM indépendamment et peut être interrompu avant d'atteindre sa destination. Ce protocole est entièrement spécifié et prouvé dans l'assistant de preuve Coq [Tea24]†, à l'aide du framework Pactole [CUR25; Bér+15]. À notre connaissance, il s'agit de la première preuve *formelle mécanisée* d'un protocole dans un cadre asynchrone non rigide, avec ou sans l'utilisation du point Weber.

**Travaux dans le domaine.** Fondamental, le problème du rassemblement a été largement étudié. La preuve d'impossibilité du rassemblement dans le cas semi-synchrone (et donc a fortiori en asynchrone) pour deux robots oublieux est donnée par Suzuki et Yamashita [SY99]. Plus précisément, il est démontré [Cou+15] que si la position initiale est *bivalente* (exactement deux positions occupées par le même nombre de robots) alors il n'existe pas de protocole résolvant le rassemblement en semi-synchrone. Ciceron et al. [CSN18] étudient les propriétés du point Weber dans le cadre du rassemblement sur un ensemble fini prédéterminé de points. Cieliebak et al. [Cie+12] résolvent le rassemblement en ASYNC non rigide : (1) pour les configurations initiales *distinctes* (pas de point de multiplicité > 1), (2) pour strictement plus de deux robots, (3) en n'utilisant pas le point Weber. En comparaison, notre travail présente une solution au rassemblement à partir de configurations quelconques (non bivalentes) avec utilisation du point Weber. En outre, notre solution est formellement prouvée correcte.

## 2 Description informelle de notre protocole

Notre protocole de rassemblement est donné Figure 1 et certains cas illustrés Figure 2.

**Modèle.** Soit $\mathcal{R}$ un ensemble de robots dans le plan. À chaque instant $t$, chaque robot $r$ a une position $p_r^t \in \mathbb{R}^2$, notons $\mathcal{P}^t$ le multi-ensemble des positions des robots à l'instant $t$. Les robots effectuent des cycles LCM infiniment souvent de manière asynchrone. Un robot activé à l'instant $t$ pour démarrer un cycle reçoit une *observation* : le multi-ensemble $\mathcal{P}^t$ dans un système de coordonnées quelconque autocentré et décide, uniquement sur la base de ce multi-ensemble, d'une destination dans $\mathbb{R}^2$. Le déplacement du robot vers sa destination prend ensuite un temps fini mais indéterminé, durant lequel d'autres robots peuvent être activés. Un robot peut être réactivé avant d'avoir atteint sa destination (il est interrompu dans son mouvement) mais uniquement s'il a parcouru une distance plus grande qu'un certain $\delta > 0$ fixé au début de l'exécution. Un protocole $A$ est une fonction qui associe à chaque observation $\mathcal{P}^t$ une destination $A(\mathcal{P}^t)$. Un protocole résout le rassemblement à partir d'une configuration initiale donnée si, quels que soient les instants où sont

<footnote>†. Coq version 8.20.</footnote>

<footnote>‡. Le protocole utilise les centres de rotation, lesquels partagent les bonnes propriétés du point Weber sans les inconvénients pré-cités.</footnote>
<figure><img src="image_2.png" /></figure>

(A) Les trois points dans $\mathcal{P}$ sont A, B, et C. Le point W est l'unique point Weber et c'est la destination de tous les robots.

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

(B) Les cinq points de $\mathcal{P}$ sont alignés mais W est l'unique point Weber et c'est la destination de tous les robots.

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

(C) Il y a une infinité de points Weber formant un segment $[w_1, w_2]$. Le milieu M du segment $[s_1, s_2]$ est un point Weber. Seuls les robots sur $w_1$ et $w_2$ se déplacent vers M.

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

(D) Il y a une infinité de points Weber formant un segment $[w_1, w_2]$. Le milieu M du segment $[s_1, s_2]$ n'est pas un point Weber. Seuls les robots sur $w_1$ se déplacent vers $w_2$.

**FIGURE 2** : Exemples d'exécution de notre protocole sur des multi-ensembles $\mathcal{P}$ de points (en noir), ici de multipli-cité 1. Les points Weber de $\mathcal{P}$ sont indiqués en gris et forment parfois un segment (segment Weber). Les flèches (parfois courbées pour faciliter la visualisation) montrent les destinations des robots (si activés à cet instant).

activés les robots, il existe un temps à partir duquel la configuration est, et reste, regroupée en un point. Ici le terme configuration représente un état du système à un instant donné, contenant la position et le mouvement actuel des robots. Dans une configuration initiale, aucun robot n'a encore été activé.

**Idée de la preuve.** La preuve exhibe un ensemble de phases numérotées de 0 à 4, chacune excluant les phases inférieures. Dans les phases 2, 3 et 4 les robots sont alignés. (Phase 0) : les robots sont tous rassemblés; (Phase 1) : il existe un point Weber unique; (Phase 2) : il existe un point regroupant la moitié des robots; (Phase 3) : le milieu de la configuration est à l'intérieur du segment Weber; (Phase 4) : le milieu de la configuration est à l'extérieur du segment Weber. Pour toute exécution depuis une configuration non bivalente, nous montrons que : (1) toutes les configurations sont dans l'une des phases; (2) tout changement de phase diminue le numéro de la phase; (3) aucune exécution ne peut rester indéfiniment dans une même phase, exceptée la phase 0. Nous en concluons que toute exécution depuis une configuration non bivalente finit par être rassemblée. Une propriété fondamentale de notre protocole est que lors d'un changement de phase, les robots encore en déplacement ne changent pas de destination, même s'ils sont réactivés avant de l'atteindre. Ceci est une conséquence de la propriété de contraction définie ci-dessous.

**Propriété de contraction.** La propriété clé du point Weber concernant le rassemblement est la *conservation par contraction* : si les robots se déplacent vers un point Weber, alors ce point reste un point Weber (cf. Figure 3). Nous précisons cette propriété ci-dessous, notamment au regard de l'unicité du point Weber. Notons que si les points sont alignés il peut y avoir plusieurs points de contraction distincts.

**Définition 1 (Contraction)** Soient $X = (x_i)_{i \in I}$ et $Y = (y_i)_{i \in I}$ deux multi-ensembles de points. On dit que $X$ se contracte sur $Y$ en $p$ si : $\forall i \in I, y_i \in [x_i, p]$. On appelle $p$ un point de contraction de $X$ sur $Y$.

**Lemme 1 (Contraction, [Bou13])** Soient $X$ et $Y$ deux multi-ensembles de points tels que $X$ se contracte sur $Y$ en un point Weber de $X$. Alors tout point $p$ est un point Weber de $Y$ si et seulement s'il est un point Weber de $X$ et un point de contraction de $X$ sur $Y$.

Deux résultats importants en découlent : sont conservés par contraction vers le point Weber, non seulement le point lui-même mais également son unicité. Notre protocole peut donc s'appuyer sur cette propriété pour déplacer sans risque les robots vers le point Weber lorsque celui-ci est unique.

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

**FIGURE 3** : Un nuage $X$ de points (en noir) se contracte sur un nuage $Y$ (en blanc) vers $W$, l'unique point Weber pour $X$. Par le lemme de contraction, $W$ est aussi l'unique point Weber pour $Y$.
**Caractérisation du cas aligné.** Quand les points de $X$ sont alignés sur une droite $D$ (et uniquement dans ce cas) il peut exister plusieurs points Weber distincts (en fait, une infinité). L'ensemble des points Weber d'un multi-ensemble de points alignés peut être caractérisé de la manière suivante [Bou13] :

**Définition 2 (on left, right)** Soit $D$ une droite et une direction (arbitraire) sur $D$. Soit $X$ un multi-ensemble de points de $D$ et $p \in D$. On note $\text{left}(p)$ (respectivement $\text{on}(p)$ et $\text{right}(p)$) le sous-ensemble des points de $X$ situés strictement à gauche de (respectivement exactement sur et strictement à droite de) $p$.

**Lemme 2** Pour tout multi-ensemble $X$ de points alignés, $p$ est un point Weber de $X$ si et seulement si : $|\#\text{left}(p) - \#\text{right}(p)| \le \#\text{on}(p)$, où $\#E$ dénote le cardinal du multi-ensemble $E$. De plus, $p$ est l'unique point Weber de $X$ si et seulement si : $|\#\text{left}(p) - \#\text{right}(p)| < \#\text{on}(p)$.

Cette caractérisation permet d'énoncer quelques propriétés importantes dans le cas aligné : (1) Les points Weber sont un segment dont *seuils* les extrémités sont dans $X$ (tout autre point exclu). (2) Lorsque $\#X$ est impair, chaque point Weber appartient à $X$ et donc le point Weber est unique. (3) Si un point $a$ une multiplicité d'au moins $\lfloor \frac{\#X+1}{2} \rfloor$, alors ce point est un point Weber. Si sa multiplicité est supérieure à $\lfloor \frac{\#X+1}{2} \rfloor$, alors c'est l'unique point Weber.

## 3 Modélisation et preuve dans le langage Coq

La bibliothèque PACTOLE est conçue pour formaliser et prouver des protocoles pour des systèmes de robots mobiles dans le modèle LCM. Dans PACTOLE, une configuration est définie comme une fonction associant à chaque robot son état : la position de sa dernière activation, sa destination et la fraction de la distance accomplie. Une exécution est une suite infinie de configurations, déterminée par l'interaction entre un *robogram* (programme exécuté par chaque robot) et un démon (séquence de décisions adversariales). Chaque robot perçoit son environnement à travers une observation, obtenue à partir de la configuration globale et d'un référentiel local. La fonction *round* est au cœur du modèle et simule un cycle LCM en mettant à jour la configuration en fonction du *robogram* et des actions du démon. Dans le modèle ASYNC non rigide, les robots peuvent être activés même en cours de mouvement. L'évolution d'un robot inactif est contrôlée par le démon qui ajuste son ratio de progression. Enfin, une propriété d'équité du démon garantit que les robots finissent par avancer, évitant ainsi une exécution figée.

Le théorème qui établit la correction de notre protocole et la première partie du lemme 2 sont donnés ci-dessous. Toutes ces propriétés sont formellement établies dans notre développement COQ.

**Theorem** gather correct config demon : 
Fair demon -> (* Pour chaque adversaire équitable *) 
(* Les référentiels locaux étant cohérents avec le configuration globale *) 
(stream.forever (Streaminstan t similarity_da prop)) demon -> 
(* Les mouvement pouvant être interrompus *) 
(stream.forever (Stream .instant flex_da prop)) demon -> 
~invalid config -> (* partant d'une configuration non-bivalente *) 
config_stay config -> (* où initialement aucun robot n'est en mouvement. *) 
WillGather (execute gatherW demon config). (* Les robots se rassemblent *)

**Lemma** weber Aligned spec weak right L ps p : 
line_dir L /= 0 -> (* la droite doit être munie d'une direction *) 
ps <> nil -> (* le multi-ensemble de points doit être non vide *) 
aligned_on L ps -> (* ...et aligné sur la droite *) 
Weber ps p -> (* p est un point Weber de ps *) 
Rabs (INR(length (L^left p ps)) - INR(length (L^right p ps))) 
<= INR (length (L^on p ps)). (* alors |#left(p) - #right(p)| ≤ #on(p) *)

où INR est l'injection canonique de $\mathbb{N}$ dans $\mathbb{R}$.

## 4 Conclusion

Notre travail présente une solution au rassemblement et sa preuve mécanisée à partir de configurations quelconques non prouvées impossibles, avec utilisation du point Weber. Contrairement au folklore large- ment accepté cette solution n'est pas triviale. L'existence d'une solution dans ces mêmes conditions mais sans utilisation du point Weber reste ouverte.
Références

[Bér+15] Béatrice BÉRARD et al. « Formal Methods for Mobile Robots : Current Results and Open Problems ». In : *International Journal of Informatics Society* 7.3 (2015). Invited Paper, p. 101-114. URL: http://www.infsoc.org/journal/vol07/IJIS_07_3_101-114.pdf.

[Bou13] Zohir BOUZID. « Modèles et algorithmes pour les systèmes émergents ». Thèse de doct. Paris, France : Université Pierre et Marie Curie, juin 2013.

[Cie+12] Mark CIELIEBAK et al. « Distributed Computing by Mobile Robots : Gathering ». In : *SIAM J. Comput.* 41.4 (2012), p. 829-879. DOI: 10.1137/100796534. URL: http://dx.doi.org/10.1137/100796534.

[Cou+15] Pierre COURTIEU et al. « Impossibility of Gathering, a Certification ». In : *Information Processing Letters* 115 (2015), p. 447-452. DOI: 10.1016/j.ipl.2014.11.001.

[CSN18] Serafino CICERONE, Gabriele Di STEFANO et Alfredo NAVARRA. « Gathering of robots on meeting-points : feasibility and optimal resolution algorithms ». In : *Distributed Computing* 31 (2018), p. 1-50. URL : https://api.semanticscholar.org/CorpusID:861053.

[CUR25] [Log.] Pierre COURTIEU, Xavier URBAIN et Lionel RIEG, *Pactole* jan. 2025. LIC : LGPL-3.0. HAL : hal-04911413v1, URL : https://gitlab.liris.cnrs.fr/pactole/coq-pactole,

[FW24] Fabian FREI et Koichi WADA. « Invited Paper : Gathering Oblivious Robots in the Plane ». In : *Stabilization, Safety, and Security of Distributed Systems : 26th International Symposium, SSS 2024, Nagoya, Japan, October 20–22, 2024. Proceedings*. Nagoya, Japan : Springer-Verlag, 2024, p. 39-54. ISBN : 978-3-031-74497-6. URL : https://doi.org/10.1007/978-3-031-74498-3_3.

[SY99] Ichiro SUZUKI et Masafumi YAMASHITA. « Distributed Anonymous Mobile Robots : Formation of Geometric Patterns ». In : *SIAM Journal of Computing* 28.4 (1999), p. 1347-1363.

[Tea24] [Log.] The Coq Development TEAM, *The Coq Proof Assistant* version 8.20, sept. 2024. DOI : 10.5281/zenodo.14542673.

A Reproductibilité de la compilation Coq

Le développement est intégré à la bibliothèque PACTOLE [CUR25].
et doit être compilée avec la version 8.20 de COQ. Plus précisément avec la séquence suivante :

```
coq_makefile -f _CoqProject -o Makefile
make CaseStudies/Gathering/InR2/Weber/Gather_flex_async_Assumptions.v
```

Les deux derniers fichiers compilés sont :

```
COQC CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v
COQC CaseStudies/Gathering/InR2/Weber/Gather_flex_async_Assumptions.v
```

Le premier contient la preuve du théorème final, et le deuxième imprime sur la console les axiomes utilisés directement ou indirectement par cette preuve. Cette liste doit être la suivante :

— les axiomes postulant l'existence d'une fonction retournant les extrémités du segment Weber : *weber_CALCobject*, *weber_CALCobject_complement* et *weber_CALCobject*.

— des axiomes concernant les réels de la bibliothèque standard de COQ : *R2similarity_in_R2*, *ClassicalDedekindReals*, *sig_not_dec* et *ClassicalDedekindReals*, *sig_forall_dec*.

— des axiomes de la logique classique : *Eqdep*, *EqRect*, *Eq*, *EqRectEq*, *ClassicalProp*, *Classic* et *FunctionalExtensionality*, *functional_extensions*, *dep*.