UNIVERSITE DE LUBUMBASHI

ECOLE SUPERIEURE DES INGENIEURS INDUSTRIELS

Département de Génie Electrique
BP.1825

Travail Pratique de Robotique

Contribution à la modélisation formelle d’essaims de
robots mobiles

Diriger par Msc TUNDA

Master 2 ELECTRICITE INDUSTRIELLE

2024
Présenter par :

MUTOMBO MUKIMBA MARDOCHEE

KABIOLA MBIDI JUNIAS
KAPEND NAWEJ RAPHAEL
NTUMBA MUYOMBO RAPHAEL
Contents
Introduction..........................................................................................................................................4

Un modèle pour l’étude des essaims de robots....................................................................................6

2.1 L’espace.....................................................................................................................................7

2.2 Les robots..................................................................................................................................7

2.2.2 Le comportement..................................................................................................................9

2.4 Accomplir une tâche, principaux problèmes étudiés.................................................................9

2.4.3 Puissances de quelques variantes..........................................................................................9

Méthodes formelles............................................................................................................................10

3.1 Model-checking.......................................................................................................................11

Pactole................................................................................................................................................12

4.1 L’espace...................................................................................................................................12

4.2 Les robots................................................................................................................................13

4.2.1 Capteurs, perceptions..........................................................................................................13

Graphes comme espaces dans............................................................................................................15

5.1 Modèle général des graphes....................................................................................................15

5.2 Exemples de graphes particuliers............................................................................................15

5.3 Graphes en action : une preuve d’impossibilité.......................................................................17

5.3.3 Formalisation de l’impossibilité de l’exploration avec stop.................................................19

Exécutions ASYNC dans PACTOLE........................................................................................................20

6.1 Rappels sur ASYNC...................................................................................................................20

6.2 Implémentation.......................................................................................................................20

6.3 ASYNC en action : une preuve d’équivalence..........................................................................21

Étude de cas : maintien de connexion dans un réseau dynamique.....................................................22

7.1 Protocoles de poursuite et connexion.....................................................................................23

7.1.1 Définitions............................................................................................................................23

7.1.2 Le choix de la cible...............................................................................................................24

7.2 Preuve formelle.......................................................................................................................26

7.2.1 Définitions COQ...................................................................................................................26

Conclusion...........................................................................................................................................28

Introduction
La robotique mobile a révolutionné la réalisation de tâches en environnement hostile : recherche,
assistance et exploration ou encore démantèlement ne représentent que quelques exemples parmi
les nombreuses missions où on peut de plus en plus éviter de risquer des vies.
L’expérience a toutefois montré les limites d’un aspect de l’approche robotique : l’envoi d’une
unité de matériel très sophistiqué (et donc cher) peut ne pas s’avérer pertinent. Le désastre de la
centrale Fukushima Daiichi l’a illustré récemment avec la panne définitive, au bout de deux heures
seulement, du robot unique chargé d’inspecter et nettoyer une partie du site dévasté, détruit par
les radiations1.
La perte de matériel coûteux2 et l’avortement de missions importantes sinon critiques (au sens
où des vies sont en jeu) invitent à peser les alternatives. Les essaims de robots mobiles s’inscrivent
dans cette réflexion.
Dans ce cadre, c’est une flotte de robots qui est à l’œuvre. Ses éléments, simples, autonomes,
doivent coopérer à la réalisation de la tâche considérée, complexe, et se réorganiser face aux
évolutions de l’environnement. Une fois déployé, l’essaim peut permettre, en parallélisant les actions
et en partageant les risques, l’établissement de réseaux dynamiques, les patrouilles, les explorations
de zones de catastrophes, l’assistance aux équipes de secours, etc.
L’emploi d’un essaim de petits robots simples à la place d’un agent unique sophistiqué répond à
l’hostilité de l’environnement et en particulier à la quasi-certitude qu’on va perdre des éléments.
D’une part, en utilisant des robots en essaim, plus simples et bien meilleur marché qu’un robot spécialisé,
l’opérateur, peut donc se permettre d’en perdre.
D’autre part, par le développement de protocoles distribués robustes, la tâche elle-même peut
supporter la perte de participants : elle n’est plus forcément mise en péril par une défaillance. On
peut ainsi caractériser deux aspects :

• Des capacités faibles pour chaque agent,

• Des propriétés fortes sur le protocole (l’algorithme, unique, embarqué et exécuté par tous les
agents), qui vont s’articuler dans cette approche versatile.

Certains des quelques scénarios que nous avons proposé ici ne tolèrent pas d’échec : des vies
peuvent être en jeu. Les solutions à base de flottes de robots qui répondent à des missions
critiques doivent donc être soumises à des étapes de vérification intransigeantes.
Du point de vue informatique, les essaims s’inscrivent dans les thématiques de l’algorithmique
distribuée et ils en partagent les difficultés. La certification de ces systèmes, en particulier est notoirement
ardue. Dès 1982 Lamport, Shostak et Pease soulignent dans un célèbre article [58] qu’ils ne connaissent «
aucun autre domaine de l’informatique ou des mathématiques dans lequel un raisonnement informel est
plus susceptible d’être erroné ». Dans la pratique, la diversité de variantes, le manque de réutilisabilité des
preuves même entre nuances très proches des hypothèses de travail handicapent le processus de
validation des protocoles typiquement écrits dans un langage informel. Malgré tout le soin apporté par
leurs auteurs on trouve encore dans la littérature des algorithmes ne respectant pas les propriétés qu’ils
sont censés vérifier [1, 39].
Sans s’appuyer sur une certification formelle, on risque l’introduction d’erreurs subtiles dont les
conséquences peuvent s’avérer catastrophiques une fois le système déployé. Ce risque est d’autant plus
prégnant que le domaine est émergent, à l’instar de la robotique en essaim.
C’est un des grands objectifs des méthodes formelles que de pouvoir garantir la sûreté de fonctionnement
dans ce type de situation. Sans surprise, on trouve donc des tentatives d’application aux essaims de robots.

1
2
 Le Model-Checking, également à l’œuvre dans la synthèse automatique de protocoles, a par exemple
été utilisé avec succès. Très automatisé et présentant l’avantage de produire systématiquement un
contremodèle dans les cas incorrects, il a permis de découvrir des erreurs dans différents travaux publiés,
dans un contexte toutefois relativement simple où les robots évoluent dans un espace discret. Il
s’applique cependant sur des instances de problèmes et ne permet pas de raisonner en toute généralité.
Typiquement, montrer qu’il n’existe aucun protocole capable de remplir une tâche donnée sous certaines
hypothèses n’est pas à sa portée.
Une autre méthode, la preuve formelle, peut être vue comme son complémentaire. Cette approche fait
l’usage d’assistants à la preuve : des outils logiciels qui ne trouvent pas seuls une preuve en complète
automatisation mais vérifient qu’une preuve qu’on leur fournit est bien correcte. C OQ est l’un de ces
assistants ; muni d’une logique d’ordre supérieur, il bénéficie d’un grand pouvoir d’expression et permet de
manipuler dans un même contexte données, calculs, propriétés et preuves de ces propriétés. L’automatisation
est faible, on sera en revanche capable d’énoncer, établir et finalement certifier corrects des résultats très
généraux, comme ceux d’impossibilité cités plus haut, y compris dans des espaces continus.

Les travaux de cette thèse abordent la preuve formelle de propriétés d’essaims de robots. Ils visent à
permettre la vérification, de protocoles ou de résultats théoriques plus abstraits, sous des hypothèses de
travail présentant un caractère plus réaliste que l’existant.

Le parti pris est délibérément informatique. Nous nous intéressons en particulier à la description d’un
modèle pour les essaims de robots proposée par Suzuki & Yamashita [74]. Le modèle original décrit des
robots se déplaçant dans un espace en fonction de leur perception de l’environnement, selon un cycle de
trois phases :

1. Look durant laquelle les robots observent un instantané de leur environnement ;

2. Compute durant laquelle la destination est calculée à l’aide du programme embarqué, le protocole
;

3. Move durant laquelle le robot se déplace vers la destination calculée.

Le modèle de Suzuki & Yamashita est remarquable par la diversités de ses variantes ; les principales
questions qui s’y rapportent concernent la détermination de bornes : quelles sont les hypothèses les plus
faibles sous lesquelles une tâche reste réalisable ?
Très succinct, épuré, dans sa définition initiale, il laisse en effet une grande liberté dans le choix des
hypothèses : sur l’espace bien sûr et sa topologie, sur la nature et les capacités des robots, en particulier
de leurs capteurs et de leurs actuateurs, enfin sur l’environnement : en quelque sorte l’adversaire.
Les variantes rencontrées sont autant de réponses à un besoin de réalisme. La possibilité d’une
réinitialisation « sauvage » dans un milieu fortement radioactif pourra justifier par exemple qu’on ne
souhaite pas, dans certains cas, assujettir le succès d’une tâche à une mémorisation des états
précédents. Il n’y a à l’origine pas d’hypothèse particulière sur la façon dont l’univers est perçu : les
performances des capteurs à modéliser pourront motiver différents modes ou des portées de visibilité
plus ou moins importantes. On voudra éventuellement prendre en compte des vitesses de
déplacement, etc.

À l’étude des possibilités offertes par différentes hypothèses, nous ajouterons quant à nous la
préoccupation : ce résultat est-il sûr ?

Notre approche de vérification s’appuie sur le cadre formel P ACTOLE3 développé pour l’assistant à la
preuve COQ. PACTOLE est constitué d’une vaste bibliothèque formelle pour l’expression et la preuve de
protocoles et de propriétés sur le modèle de Suzuki & Yamashita. Initié en 2009, ce cadre formel a
montré la faisabilité d’une approche par preuve dans le contexte des robots mobiles. Il a permis de
certifier non seulement des résultats de correction de protocole [32, 11] mais aussi d’impossibilité [31]
y compris en présence de fautes byzantines (c’est-à-dire comportement arbitraires voire hostiles de
certains robots défaillants) [6]. Le prototype au commencement de nos travaux considérait toutefois

3
des hypothèses assez simples : espace Euclidien, robots ponctuels, sans volume, ordonnancement
totalement ou semisynchrone, etc.
Nos contributions étendent ce cadre formel. Par des facilités de spécification, par un
enrichissement du cœur du modèle à une plus grande variété de domaines, elles introduisent des
hypothèses toujours plus réalistes et s’inscrivent donc dans une volonté de rendre accessible au plus
grand nombre de développeurs des techniques de vérification formelle fondées sur la preuve. Nous
proposons en particulier un cadre d’expression des espaces discrets, c’est-à-dire ici de graphes,
domaine très étudié en pratique. Nous ajoutons aux synchronisations en place la possibilité de
modéliser des exécutions totalement asynchrones et donc bien plus réalistes. Nous permettons enfin
de travailler sur des robots qui ne sont plus simplement des points sans épaisseur mais qui présentent
un volume et des risques de collisions.
Au delà de l’exercice technique, nous illustrons systématiquement l’utilisabilité pratique de nos
formalisations à travers différentes mises en œuvre : preuve d’impossibilité d’exploration dans les anneaux,
preuve d’équivalence entre deux représentations des déplacements dans des graphes, conservation
d’invariant pour un protocole distribué de poursuite et maintien de connexion avec une cible mobile.

Ce document présente nos travaux, il est organisé comme suit : le chapitre 2 détaille le modèle
proposé par Suzuki & Yamashita [74]. Nous y détaillons le cœur du modèle, les particularités des
robots, ainsi que différents degrés de liberté définissant des variantes. Nous exposons également
certains des principaux problèmes étudiés dans ce contexte.
Pour maîtriser les erreurs malheureusement encore rencontrées dans des travaux pourtant très
soigneux, nous nous intéressons aux méthodes formelles dont nous donnons un aperçu au chapitre 3.
Le spectre des méthodes formelles est large ; on rencontre principalement en algorithmique distribuées
des approches de spécifications outillées par des assistants mécaniques, du model-checking, et depuis
peu de la preuve formelle sur laquelle se concentrent nos travaux, au travers de l’approche PACTOLE.
Le chapitre 4 donne un bref exposé de l’assistant à la preuve C OQ et décrit le cœur de PACTOLE. Il
présente comment le modèle de Suzuki & Yamashita est fidèlement reproduit dans le cadre formel.
PACTOLE a connu plusieurs phases de développement, nous faisons dans ce document, par souci de
cohérence, le choix de décrire sa version la plus récente utilisant les « typeclasses » de C OQ et dans
laquelle ont été portées nos contributions initialement développées pour une architecture de modules.
Le chapitre 5 présente la première de nos contributions avec l’extension de P ACTOLE aux graphes, nous
illustrons une première fois la validité de cette extension avec une preuve d’impossibilité en certifiant
formellement qu’on ne peut réaliser l’exploration avec stop d’un anneau lorsque le nombre de robots (sous
certaines hypothèses de capacités) divise le nombre de nœuds de l’anneau. Un article présentant ces
travaux a été publié dans les actes de la conférence internationale ICDCN2018 [12].
Le chapitre 6 quant à lui explique notre extension du noyau de P ACTOLE au cas de séquencement
totalement asynchrone. Nous montrons la pertinence de notre modélisation en la mettant en œuvre dans une
preuve d’équivalence entre deux modèles de nouveau sur les graphes : un modèle purement discret où les
agents sautent de nœud en nœud et un modèle plus réaliste où les robots se déplacent continuement le long
des arêtes

Un modèle pour l’étude des essaims de

robots
Nous présentons le modèle introduit par Suzuki & Yamashita [74]. Simple dans sa description, conçu pour une
analyse des essaims des points de vue informatique et algorithmique, ce modèle s’est enrichi de nombreuses
variantes. On peut en résumer le principe fondamental en énonçant que des robots se déplacent dans un
espace vers une destination calculée en fonction de leur perception de l’environnement. Nous allons donc
décrire dans un premier temps les espaces considérés, les caractéristiques et capacités usuellement
rencontrées pour les robots et en particulier celles de leur mode de perception. Nous présenterons enfin les
différents aléas et modes de synchronisation qui peuvent décrire les évolutions du système.
 Nous détaillerons ensuite quelques-uns des principaux problèmes, fondamentaux ou plus appliqués,
étudiés dans ce cadre.

2.1 L’espace
On distingue principalement deux grandes familles d’espaces dans la littérature sur les robots mobiles, les
espaces continus d’une part, et les espaces discrets d’autre part.

Les espaces continus. Dans la plupart des travaux sur les espaces continus, ces derniers sont euclidiens 4
; les positions des robots sont simplement des points ou des voisinages quelconques. La trajectoire des
robots peut être spécifiée, ou définie par le programme embarqué dans chaque agent. Sauf mention
contraire, on considère cependant des trajets rectilignes.
Nous travaillerons plus particulièrement avec ces espaces au long du chapitre 7.

Les espaces discrets. Les positions privilégiées (destinations) possibles des robots dans ces espaces sont
discrètes et distinguées, leurs liaisons spécifiées. On est essentiellement dans le cas de graphes (où les
positions privilégiées sont les nœuds). Le chemin entre deux positions dans le graphe est classiquement
dans ce cas la liste des sommets séparant les deux positions.

Un cas hybride. On peut toutefois, par souci de réalisme, considérer certains espaces exhibant des
caractéristiques de ces deux grandes familles, par exemple en considérant des arêtes de graphes continues
de dimension 1 dont les points sont des positions possibles (c’est-à-dire traversables au cours d’un
déplacement) mais non privilégiées des agents qui visent les nœuds. La description d’un chemin comprend
alors également la liste des arêtes empruntées.
Nous nous intéresserons aux graphes discrets et hybrides au cours des chapitres 5 et 6.

2.2 Les robots

La diversité des situations auxquelles les robots peuvent être confrontés dans des applications pratiques, en
particulier du fait de l’adversité supposée de l’environnement, invite à la prudence quant aux hypothèses sur
lesquelles se reposer : peut-on faire confiance à d’éventuelles communications ? les agents vont-ils se
réinitialiser du fait de radiations, par exemple et peut-on alors faire confiance à leur mémoire ? etc. Les
capacités et caractéristiques des robots à modéliser varient donc en fonction de la résilience désirée.
Dans sa version fondamentale et initiale, le modèle de Suzuki & Yamashita pose cependant un cadre
commun.

Les robots sont homogènes. Ils présentent les mêmes caractéristiques internes et externes au sens où ils
sont construits sur le même modèle.

Les robots sont autonomes. Ils constituent un système distribué décentralisé : chacun des robots prend lui-
même ses décisions, elles ne lui sont pas dictées par une quelconque unité centrale.

Les robots suivent le même algorithme. La prise de décision dépend d’un algorithme commun à tous les
robots : le protocole. Ce protocole peut être suivant les modèles déterministe ou non déterministe.

Il n’y a pas de canal de communication explicite. Les robots sont dit silencieux. Les seuls échanges
d’informations se font via l’observation de l’état perceptible des autres robots, par exemple leurs positions
relatives et éventuellement d’autres modalités visibles comme l’affichage de signaux colorés.

4
 Ce silence des robots peut être motivé par les applications ou les environnements hostiles dans lesquels les
perturbations de communications sont possibles.

La perception de l’environnement est un instantané. Les états perceptibles reçus sont ceux à un instant
donné.
La prise de décision, le résultat de l’algorithme ne dépend que de la perception des robots. En particulier si
deux robots ont des perceptions équivalentes (pour une certaine définition) les ensembles de réponses sont
équivalents. Par exemple deux robots au protocole déterministe, situés à la même position et recevant la
même perception de l’environnement, calculeront le même état résultat (comprenant la même destination).

Les principales variantes du modèle portent sur les caractéristiques des robots et de leurs capteurs.

Anonymat. Les robots sont tous construits sur le même modèle mais cela n’empêche pas une forme
d’identification. Le modèle original [74] considère des robots indistinguables au sens où leur propre perception
ne sait les différencier et anonymes. C’est le cadre où nous nous placerons dans la majeure partie de nos
travaux. Nous modéliserons et utiliserons cependant des robots avec identifiant lors de notre étude de cas
complète du chapitre 7.
Persistance de la mémoire. On peut considérer que les robots ont une certaine quantité de mémoire pour
l’exécution du protocole. Cela ne signifie pas qu’ils sont capables de retenir des informations (perceptions,
états) de leur actions passées.
On parle de robots oublieux lorsque leurs prises de décision et changements d’état ne peuvent pas
dépendre des actions passées (en plus de la perception actuelle). C’est le cas des robots du modèle initial ; la
contrainte est lourde mais légitimée par les cas pratiques où des réinitialisations sont à craindre.
2 X
1 X

5 5

3 X
(c) Multiplicité globale forte. (d) Multiplicité locale forte.

Figure 2.3: La configuration en (a) est un graphe avec le robot

observant et les autres robots. En (b) et en (c) nous avons des exemples de détection de la multiplicité globale
dans ce graphe. Enfin en (d) nous avons un exemple de multiplicité locale.

A B C

Figure 2.4: Le robot A ne voit pas le robot C car le robot B bloque la vision dans la. zone à fond bleu
 2.2.2 Le comportement
Au cœur de leur modèle, Suzuki & Yamashita décrivent la façon dont les robots agissent et interagissent
comme suit : 1) un robot est soit actif soit inactif, 2) quand il est actif, le robot effectue un cycle de trois
phases:

1. Look Le robot fait un snapshot de l’espace observé recevant la position des autres robots (plus
précisément leur état perceptible) relativement à sa propre position.

2. Compute En utilisant le snapshot fait dans la phase Look, le robot calcule grâce à son programme la
position de sa prochaine destination (plus précisément son prochain état).

2.4 Accomplir une tâche, principaux problèmes étudiés

La littérature dans la thématique des robots mobiles est principalement dirigée par les problèmes : on y fixe
un problème et on étudie sous quelles hypothèses (sous quelles variantes du modèle) ce problème est, ou
non, résoluble.
Un protocole résout un problème si dans toutes les configurations initiales acceptables, ce protocole
résout le problème quels que soient les choix du démon5. L’important ici c’est qu’il ne peut pas y avoir de cas
où le protocole ne résout pas le problème : si un protocole ne fonctionne que pour certaines configurations
initiales par exemple, ou certains choix, il ne résout pas le problème.
Similairement, un problème n’est pas résoluble si pour tout protocole il existe une configuration de départ
et une suite de décisions du démon faisant échouer le problème.
On peut caractériser les conditions pour lesquelles une tâche est réalisable de deux façons : les résultats
positifs identifient des conditions suffisantes à la réalisation de la tâche en fournissant des protocoles qui
résolvent cette tâche suivant certaines conditions. Inversement, les résultats négatifs cherchent à identifier
des conditions nécessaires, en démontrant qu’en deçà aucun protocole ne peut résoudre la tâche.
Lors des résultats négatifs, la hiérarchie précédemment établie sur les démons peut être vu comme
inversée. Un contre-exemple utilisant un démon F SYNC sera plus puissant qu’un contre-exemple utilisant S SYNC,
car le contre-exemple FSYNC est également SSYNC. De même, un contre-exemple S SYNC est plus puissant qu’un
contre-exemple ASYNC.
Les problèmes principalement étudiés sont fondamentaux ou plus appliqués, ils se rangent en deux
grandes familles : d’abord la création de figures particulières (pattern formation), incluant notamment le cas
fondamental particulier du rassemblement (gathering) en un seul point, ensuite les problèmes d’exploration,

2.4.3 Puissances de quelques variantes

Robots lumineux
Les modèles de robots lumineux utilisent pour la plupart un nombre de couleurs fini et leur puissance peut
varier selon ce nombre. Un modèle ASYNC avec des couleurs peut ainsi gagner en puissance. Avec seulement
5 couleurs, Das et al. montrent [35] que leur modèle ASYNC est au moins aussi puissant qu’un modèle S SYNC
sans couleur, c’est-à-dire qu’il peut résoudre les même problèmes, et potentiellement d’autres. Ces mêmes
travaux établissent en outre que si jamais ces robots colorés pouvaient se souvenir d’une seule
configuration, ils seraient strictement plus puissant que des robots FSYNC oublieux et sans lumières.

Robots volumiques opaques

Les robots volumiques opaques ont en particulier été étudiés dans le contexte du rassemblement. Toutefois,
étant volumiques, ils ne peuvent pas être exactement au même endroit. La définition du rassemblement est
donc adaptée à ce cadre et le rassemblement pour des robots volumiques devient la formation d’une figure
géométrique dont tous les robots doivent être conscients de la fin de formation.
L’opacité de ces robots ajoute une difficulté : il est impossible pour un robot de savoir si un autre est
caché par un des robots visibles (comme illustré par la figure 2.9). Le démon peut en particulier faire bouger
les robots de telle sorte à en cacher certains à d’autres.

5
 Il n’existe pas à notre connaissance dans la littérature de solution pour le rassemblement de plus de 4
robots volumiques opaques. Czyzowicz, Ga˛sieniec et Pelc proposent un protocole pour le cas où n = 3, et un
autre pour le cas où n = 4 [34].

A B C

Figure 2.9: Le robot A ne voit pas le robot C car qu’importe où sont placés les capteurs de A, le robot
bloque la vision, dans la .

Méthodes formelles
Le chapitre précédent a fait état de de travaux démontrant des résultats. Ces démonstrations sont
cependant bien souvent faites « à la main », avec grand soin mais possiblement victimes d’erreurs
humaines. De possibles variations subtiles entre le contexte et là où est justifié/appliqué un résultat
invalident en effet ce dernier. On trouve malheureusement toujours des résultats incorrects dans la
littérature [39] ; la plupart du temps ces erreurs sont découvertes grâce à l’apport des méthodes
formelles.
Les méthodes formelles (il en existe plusieurs types) permettent d’énoncer formellement (sans aucune
ambiguïté) les résultats et lemmes mais ont aussi pour but de permettre la vérification de la validité d’énoncés
et de programmes. Cette vérification a lieu grâce d’une part, à des langages mathématiques non ambigus et
d’autre part à des outils permettant cette vérification. Ces méthodes ont été utilisées avec succès dans
différents domaines: mathématiques [49, 62], preuve de programmes [60], compilateurs certifiés[60], Système
d’exploitation [55]. Les preuves formelles ont aussi eu un rôle dans l’industrie, avec la certification de la ligne
du métro 14 à paris [59], ou encore la vérification de protocole d’atterrissage[64].
La grande variété dans les modèles de robots mobiles et la considérable difficulté à garantir la
correction d’un algorithme distribué rendent leur utilisation nécessaire, en particulier dans les cas
d’applications critiques.
L’algorithmique distribuée a bien sûr fait appel à ces méthodes, pour ne citer que quelques approches
: au niveau des spécifications et raisonnement (possiblement outillés) avec la Temporal Logic of Actions
de Lamport : TLA/TLA+Proofs [57, 33], au niveau de la vérification avec le model-checking et au niveau de
l’algèbre des processus avec le π-calcul [63].
Le contexte des robots mobiles n’est pas parfaitement adapté à la modélisation TLA, plutôt pensée
pour un modèle de processus avec partage de mémoire et envoi de messages. Les algèbres de processus
ne sont pas non plus idéales pour notre modèle, car il n’y existe pas de notion de positions. Il a en
revanche été fait largement usage du model-checking et de sa puissante automatisation, y compris pour
la synthèse automatique de protocoles ; nous en donnons un aperçu au prochain paragraphe. Nous nous
intéresserons pour notre part à une autre approche : la preuve formelle mécanisée. Pour plus de détail, il
existe plusieurs études concernant les méthodes formelles appliquées aux robots mobiles[16, 68]
3.1 Model-checking
Parmi les différentes méthodes formelles, le model checking est une méthode très utilisée dans la
vérification sur les robots mobiles grâce à son automatisation et sa relative facilité de prise en main. Le
principe de cette méthode est le suivant:

1. Représenter le système sous forme de système de transition. Cela amène donc une abstraction et
une sur-approximation du modèle de base. Cette sur-approximation contient cependant tout les
états du système de base, ainsi les propriétés de sûreté sur le modèle de transition restent valables
sur le système original.

2. Analyser tous les cas possibles lors de l’évolution du système de transition.

Ensuite il faut définir la propriété qui doit être vérifiée grâce à, par exemple, de la logique temporelle: la
propriété S en langage naturel pour toute la durée de l’exécution, il n’existe pas deux robot à la même
position peut se traduire en logique temporelle en GF(∀xy,x 6= y => pos(x) 6= pos(y)). Cette propriété φ
est une abstraction de S qui est créée sur mesure pour être vérifié de manière exhaustive et automatique
par le model-checker.
φ doit ensuite rester valable. Si cette validité de φ est bien là, la propriété S est vraie car φ est une
propriété de sûreté. De plus, si φ n’est pas vérifiée, alors le model-checker retournera un contre-modèle.
Ce contre-modèle n’est pas à proprement parler un contre-exemple de S, car il se peut que l’abstraction de
φ soit trop forte, et donc que le résultat ne corresponde pas exactement au problème S.
Cette méthode de vérification a pour avantage de n’avoir qu’à exprimer le modèle et le problème en
système de transition d’états, et le logiciel donne une réponse automatiquement. Cela permet à des
personnes non spécialisées dans le domaine des méthodes formelles de faire de la vérification formelle sur
les modèles.
Cette méthode de vérification formelle a permis de prouver de nombreux résultats dans le cadre des
robots mobiles utilisant des instances de problème. Pour citer quelques exemples : Bérard et al. proposent
des preuves concernant la correction d’algorithmes pour résoudre l’exploration avec stop [17], ainsi que
l’exhibition de contre-exemple pour le modèle perpétuel ; Défago donne et prouve correct un protocole
pour le rassemblement entre deux robots lumineux [41].
Les outils utilisés sont extrêmement efficaces pour résoudre certains types de problèmes, notamment
sur des instances particulières. Il est cependant plus difficile d’aborder par cette approche des problèmes
généraux. En effet, comme il est nécessaire de modéliser toutes les possibilités, il existe une tension entre
la précision de l’abstraction du problème et la taille à maintenir raisonnable des modèles à vérifier. Cette
méthode est très susceptible à l’explosion combinatoire et donc peut devenir impraticable. Il est de même
difficile de faire des vérifications sur l’impossibilité de résoudre un problème pour tout programme 6. En

Preuve formelle
Modèles de
Autres Modeles Problème P Protocole p
Calculs

preuve assistée preuve assistée preuve assistée

Inclusion Impossibilité Correction Instance I

preuve automatisée abstraction

Contre-exemples LTL φ?
génération

6 C’est-à-dire qu’un problème ne peut être résolu qu’importe l’algorithme utilisé, voir paragraphe 2.4.
 Model-checking Figure 3.1: Les

utilisations de la preuve formelle et du model checking.

Pactole
Dans ce chapitre, nous présentons comment P ACTOLE7 implémente les différentes notions communément
présentes pour les algorithmes distribués sur les robots mobiles. Nous allons donc dans un premier temps
décrire la représentation des espaces dans PACTOLE. Puis nous présenterons les définitions des robots, ainsi que
les façons dont sont décrites leurs limitations. Nous détaillerons ensuite comment sont modélisées les
différentes caractéristiques des synchronisations dans PACTOLE. 8

4.1 L’espace
PACTOLE a pour but de représenter fidèlement mais aussi de manière abstraite les espaces utilisés dans
l’algorithmique des robots mobiles.
Dans sa version original, c’est-à-dire avant nos travaux, P ACTOLE permet essentiellement la définition
d’espaces continus.
On y demande en général de pouvoir décider si deux positions sont égales. Dans le cas des espaces réels,
R, R2, etc., on utilisera les réel axiomatiques de C OQ. La plupart des études de cas de P ACTOLE utilisent en fait
des espaces vectoriels.
Pour construire un espace vectoriel, il faut un type de départ, représenté par T. Ce type possède une
origine, les opérations usuelles que sont l’addition, la multiplication et l’inversion.
Afin de pouvoir travailler sur cet espace, il faut aussi une notion d’équivalence sur le type T et la preuve de
la décidabilité de cette équivalence, représentées respectivement par S et par H. Avec S et H, il est possible
maintenant de définir les propriétés de compatibilité d’une fonction avec l’équivalence S. Nous pouvons donc
définir les propriétés d’associativité et de commutativité de l’addition, ou encore de distributivité de l’addition
par la multiplication.
Chacune de ces opérations nécessite aussi une propriété de compatibilité: ces propriétés spécifient que si,
lors de deux applications d’une fonction, tous les arguments de chaque applications sont équivalents deux à
deux, alors les deux résultats seront équivalents 4.1.
Enfin, pour avoir un espace non dégénéré, l’existence d’une valeur autre que l’origine ( one) et d’une
propriété assurant leur inégalité (non_trivial) sont requises.
(* A | B | C | D | E *) add_compat : Proper
(equiv ≡> equiv ≡> equiv) add;

Figure 4.1: Exemple d’une déclaration de propriété de compatibilité:

A : Le nom de cette propriété.

B : La relation sur première variable de la fonction dont on veut établir la compatibilité.

C : La relation sur la seconde variable de la fonction.

7 [Link]
8 ces notions sont résumé dans [10]
4.2 Les robots
Dans PACTOLE, les robots mobiles sont représentés par un identifiant unique à chaque robot, mais
invisible par les robots9. Cet identifiant sert uniquement aux preuves.
Nous avons vu qu’il peut exister des robots fautifs, nous séparons donc les robots en
deux catégories, les robot fautifs, qui sont appelés byzantins ou Byz, et les robots
normaux, appelés Good. Un robot a ainsi le type identifier:

Inductive identifier {G} {B} : Type :=

| Good : G→
identifier | Byz : B→
identifier.

Ici, G et B sont les ensembles de robots de chaque catégorie qui existe dans le modèle
et restent abstraits pour plus de liberté. B et G sont définis par deux nombres entiers
naturels, nB et nG respectivement, à la création de l’instance des robots:
Notation "’fin’N" := {n : nat | n < N}

(*...*)

G := fin nG;
B := fin nB;

Cette définition permet d’avoir des propriétés prédéfinies pour les robots comme
l’unicité des robots ou la décidabilité de l’égalité. Cela permet aussi de faire de l’induction
sur le nombre de robots. Pour extraire cet entier du type par intention, nous utilisons la
fonction proj1_sig.
proj1_sig =
fun (A : Type) (P : A→ Prop) (e : {x : A | P x}) ⇒ let (a, _) := e in a : ∀ (A : Type) (P : A→ Prop), {x :
A | P x} → A

Il faut cependant noter que cela ne représente pas les caractéristiques des robots, cela
représente juste l’ensemble des identifiants des robots.
4.2.1 Capteurs, perceptions
Dans PACTOLE, une configuration est définie comme une fonction qui étant donné un identifiant de
robot, qu’il soit byzantin ou non, renvoie toutes les informations concernant ce robot et en particulier
sa position. Ces informations sont stockées dans un type info, abstrait.
Definition configuration ‘{State} ‘{Names} := ident→ info.

Cela permet de représenter le système à un moment donné. Le système évoluant dans le temps,
potentiellement indéfiniment, les exécutions sont simplement des suites infinies de configurations comme
dans le paragraphe
2.3.
Cette suite infinie est représentée par un Stream. Un Stream dans PACTOLE est un objet d’un ensemble
défini par coinduction. Il est défini par un ajout ( cons) en tête, la projection de cet élément de tête ( hd)
et la projection du reste (tl) du Stream.

9 Cela n’empêche pas d’ajouter une forme d’identification perceptible dans l’état visible d’un robot si jamais les
hypothèses ne requièrent pas l’anonymat des robots.
Graphes comme espaces dans
PACTOLE
Les espaces discrets sont largement présents dans la littérature concernant les robots autonomes. Le
prototype original de PACTOLE ne permettant pas de travailler sur ce genre d’espace, il était important d’y
intégrer les moyens d’exprimer ces espaces discrets de la façon la plus simple possible.
Nous proposons une interface générale pour définir des graphes en adéquation avec le cadre formel. Nous
n’avons pas la prétention de réaliser une bibliothèque du calibre de loco [25], une bibliothèque permettant de
manipuler des graphes arbitraires. Nous donnons davantage les moyens de définir des espaces se comportant
comme des graphes plutôt que des graphes pour eux-mêmes. De plus, un des buts de P ACTOLE étant de faciliter
la specification à des utilisateurs extérieurs au milieu de la preuve formelle nous veillons autant que faire se
peut à la simplicité de création de ces espaces, y compris pour les non-experts.

5.1 Modèle général des graphes

Pour construire un espace, il nous faut un ensemble décidable de positions. Pour cela, nous définissons une
classe Graph qui représente les graphes en général. Prenons le principe de base de la création de graphes: deux
ensembles, un pour les sommets ( V) et un pour les arêtes ( E). Comme nous voulons que ces deux types
puissent être utilisés comme positions des robots, ces types possèdent une notion d’équivalence et de
décidabilité.
Les arêtes allant toujours d’un sommet vers un autre, et comme nous voulons garder le type des arêtes
abstrait, nous rajoutons 2 fonctions : source (src) et target (tgt), servant à relier le type E au type V et
retournant respectivement le point de départ et le point d’arrivée d’une arête.
Nous avons des fonctions de l’ensemble des arêtes vers l’ensemble des sommets. Il nous faut aussi une
fonction dans l’autre sens: la fonction find_edge est une fonction qui, étant donnés deux sommets, renvoie un
type option (None/Some x) pour indiquer s’il existe une arête entre les deux sommets. 10
La cohérence entre les fonctions src et tgt, d’une part, et la fonction find_edge, d’autre part, est garantie par
la propriété find2st. Cette fonction vérifie que s’il existe une arête entre deux sommets, alors les fonctions src
et tgt rendent bien ces sommets.
Toutes ces fonctions représentent la topologie dans laquelle évoluent les robots, mais ces robots ne
perçoivent pas forcément exactement cet espace. Comme il a été vu précédemment dans la section 4, notre
modèle nécessite aussi une possibilité de changer de référentiel. Nous avons donc ajouter un type de bijection
pour les graphes, les isomorphismes de graphes, contenant une bijection pour chaque type, sommet et arête,
ainsi que des propriétés s’assurant que l’organisation du graphe ne change pas. Par exemple dans un anneau,
un isomorphisme est une rotation de l’anneau, ou une symétrie axiale.

Record isomorphism := { iso_V :> bijection V; iso_E : bijection E;

iso_morphism : ∀ e, iso_V (src e) ≡ src (iso_E e) ∧ iso_V (tgt e) ≡
tgt (iso_E e

5.2 Exemples de graphes particuliers

Pour montrer l’expressivité et les possibilités de ce modèle de graphe, nous avons aussi décrit dans
PACTOLE un modèle de graphe plus particulier: l’anneau (au sens graphe du terme). Un anneau
est un graphe connexe où chaque sommet est relié à deux et seulement deux autres sommets.

10
1 dist x ≤z add (dist x y) (dist y z)

≤ x) z)
[Link] (add (opp z) x) (add (opp
2 add ([Link] (add (opp y) x) (add (opp x) y))
([Link] (add (opp z) y) (add (opp
)) y) z

[Link] ((x - z) mod n) ((z - x) ≤mod n)

3 (([Link] ((y - x) mod n) ((x - y)))mod n
+ ([Link] ((y - z) mod n) ((z - y) mod n))) mod n

Cas 1 Cas 1’ ... Cas 2 Cas 2’

Figure 5.3: Pour prouver cette inégalité en C OQ, nous allons commencer par développer les définitions de dist,
pour pouvoir voir tous les différents cas auxquels nous allons devoir faire face (1).
Puis nous allons déplier les définitions des opérations modulo n, pour pouvoir plus facilement travailler avec le
scope Z de COQ, un scope étant un environnement de C OQ pour que les opérations soient en priorité regardées
sur des valeurs de type voulu, ici Z (2).
Nous allons ensuite différentier toutes les possibilités des termes de la forme
[Link] ((a - b) mod n) ((b - a) mod n) en distinguant trois cas : le cas où les deux parties sont égales et chacun des
cas où une des partie est strictement plus petite que l’autre (3).

∀ x y z , X
(x - z ) m o d n = ( z - x ) m→ o d n
0 < ( x -z) mod n → Cas 1
(x - y ) m o d n < ( y - x ) m→ o d n
(z - y ) m o d n < ( y - z ) m→ o d Zn
False

Figure 5.4: Le premier des cas non triviaux concernant la preuve de l’inégalité triangulaire dans les graphes
∀ x y z , X
(x - z ) m o d n = ( z - x ) m→ o d n
0 < ( x -z) mod n → Cas 1’
(y - x ) m o d n < ( x - y ) m→ o d n
(y - z ) m o d n < ( z - y ) m→ o d Zn
False

Figure 5.5: Un cas similaire au premier cas de la preuve.

 ∀ x y z , Z X
(x - z ) m o d n < ( z - x ) m→ o d n
0 < ( x -z) mod n → Y Cas 2
(x - y ) m o d n < ( y - x ) m→ o d n
(z - y ) m o d n < ( y - z ) m→o d n
(x - z ) m o d≤ n((x - y ) m o d n + ( z - y ) m o d n ) m o d n .

Figure 5.6: Le deuxième cas de la preuve d’inégalité triangulaire dans les graphes, avec la formule en C OQ, et sa
représentation.

Dans le premier cas (5.4), nous sommes dans un des cas où X et Z sont diamétralement opposés sur
l’anneau, ce qui est exprimé par les deux premières lignes. Le reste de l’énoncé nous donnes les
hypothèses permettant de prouver la contradiction car nous sommes dans un cas où Y est plus proche de
la position de X dans un sens que dans l’autre mais est plus proche de Z dans le même sens, ce qui est
impossible.
En dépliant la définition de dist, nous retrouvons la propriété voulue. De là, il reste beaucoup de travail
arithmétique pour enlever les modulos afin que la tactique omega puisse établir l’impossibilité de ces
inégalités. Le cas similaire 5.5 est différent car le robot Y est plus proche dans le sens inverse, c’est-à-dire
que la comparaison des valeurs de (x - y) mod n et (y - x) mod n donne le résultat inverse.
Dans les autres cas non triviaux, regardons en premier le cas 5.6 où il nous faut prouver que le robot Y
est plus proche de X dans un sens, et plus proche de Z dans le même sens, sachant que Z est entre Y et
X. Pour cette preuve nous montrons en premier lieu que les trois valeurs (x-z)mod n, (x-y) mod n et (z-y)mod n
sont toutes inférieures ou égales à n/2, puis nous nous en servons pour retirer le modulo du membre droit de
l’inéquation finale ce qui mène à (x - z) mod n ≤(x - y) mod n + (z - y) mod n.
Nous faisons quelques opérations sur les modulos pour arriver à l’inéquation
(x - z) mod n ≤(x - y) mod n + (z - y) mod n. De là, nous transformons (x-y) mod n en (x - z) mod n + (z - y) mod n, ce
qui résout l’inéquation.
Et ici encore, il y a le cas similaire au cas 2, mais où les valeurs des comparaisons sont inversées. Dans ce
cas, la position de Y est plus proche de X que de Z (5.7).
Ces preuves totalisent un millier de lignes pour prouver l’existence de l’espace associé au graphe.
∀ x y z , Z X
(x - z ) m o d n < ( z - x ) m→ o d n
0 < ( x -z) mod n → Cas 2’ Y
(y - x ) m o d n < ( x - y ) m→ o d n
(y - z ) m o d n < ( z - y ) m→o d n
(x - z ) m o d≤ n((y - x ) m o d n + ( y - z ) m o d n ) m o d n

Figure 5.7: Le cas similaire au cas 2 de la preuve de l’inégalité triangulaire.

5.3 Graphes en action : une preuve d’impossibilité

Pour illustrer l’implantation des graphes dans PACTOLE, nous en présentons une utilisation en établissant
formellement un résultat d’impossibilité concernant l’exploration avec stop dans un anneau.
L’exploration avec stop est satisfaite par un protocole s’il vérifie les deux propriétés suivantes:
1. Chaque sommet du graphe est visité en temps fini par au moins un robot.

2. Une fois tous les nœuds visités, tous les robots sont arrêtés pour toujours.
Nous montrons formellement que si nous avons un anneau de taille n, et un nombre de robots k dans cet
anneau, si k divise n, alors aucun protocole ne résout l’exploration avec stop en FSYNC.
 configurations initiales acceptées correspondent à n’importe laquelle des configurations où il n’existe pas
deux robots qui sont sur un même noeud.
Un protocole résolvant l’exploration avec stop doit arriver à une configuration qui n’est pas acceptée
comme configuration initiale, c’est-à-dire une configuration avec deux robots sur le même sommet.
Une conséquence de cette remarque est qu’il n’existe aucun protocole résolvant l’exploration avec stop
avec un unique robot.

Le nombre de robots divise la taille de l’anneau

S’il y a au moins deux robots, et si le nombre de robots divise la taille de l’anneau, alors il est possible de
créer une configuration initiale symétrique assurant que tous les robots ont exactement le même
comportement.
La configuration globale reste ainsi dans un état où tous les robots ont exactement la même vision de leur
environnement et donc choisissent le même mouvement si ils sont activés. Comme l’exploration avec stop
est résolue seulement par un protocole qui réussi pour tous les démons et toutes les désorientations
possibles, il suffit de trouver un démon qui fait échouer tous les protocoles avec cette configuration initiale.
Nous choisissons le démon qui active tous les robots à chaque round et leur donne tous la même orientation.
Ainsi, tout protocole aura donc un des comportements suivants:

• Soit le protocole ordonne a chaque robot de ne pas bouger, ce qui signifie que le protocole stoppe comme
à la figure 5.8,

Figure 5.8: Dans le cas d’un protocole faisant s’arrêter les robots, nous nous retrouvons ici avec deux sommets
visités, mais les quatre autres ne le sont pas et ne le serons jamais, car on reste dans la même configuration.

les robots bougent

R R

R R

le démon change la perception des robots

Figure 5.9: Si le protocole ordonne à chaque robot de bouger dans la même direction (ici vers la gauche), le
démon changera la perception des robots lors de la prochaine configuration pour qu’elle soit indistinguable de
l’initiale, et donc que les robots seront en mouvement perpétuel.
• Soit les robots bougent indéfiniment et on se retrouve avec une suite d’actions comme à la figure
5.9.

De là, nous déduisons qu’il n’existe pas de protocole pouvant résoudre l’exploration avec stop dans un
anneau si le nombre de robots divise la taille de l’anneau.

5.3.3 Formalisation de l’impossibilité de l’exploration avec stop

Contexte
Avec des robots anonymes, l’observation ne doit contenir aucune information concernant d’éventuels noms.
Avec la détection de la multiplicité, un multi-ensemble contenant les positions occupées est une observation
acceptable (c’est-à-dire un multi-ensemble avec un élément distinct dénotant la position du robot considéré).
Les robots sont oublieux, par conséquent il leur est associé un nouveau référentiel à chaque activation.
Dans le cas d’un espace basé sur un graphe, un isomorphisme (de graphe) est appliqué au graphe avant
d’extraire l’observation pour retirer toute information se reposant sur les identifiants des sommets.
Comme nous utilisons un démon F SYNC, la fonction activate de l’action démoniaque renverra toujours true.
la fonction permettant de calculer l’observation sera quant à elle créée à partir du paramètre change_frame.

Le problème
Le problème de l’exploration avec stop requiert que les robots visitent collectivement tous les sommets du
graphes et s’arrêtent une fois l’exploration complétée. Pour formaliser cette spécification, nous utilisons le
prédicat Will_be_visited tel que, si v est un sommet, et exe est une exécution, la propriété Will_be_visited v exe
est vérifiée si et seulement si au moins un robot visite le sommet v durant au moins un round de exe:
(* Nous utilisons les operations de la logique temporelle classique. on peut lire la definition cidessous comme: ‘‘A
un moment de l’execution, le sommet v sera visite.’’ *)
Definition Will_be_visited v exc :=
[Link] (Visited_now v) exc.
Exécutions ASYNC dans PACTOLE
Nous avons vu précédemment au chapitre 4 que le prototype original de PACTOLE contenait, avant nos
travaux, deux modélisations pour la synchronisation des robots, le mode F SYNC et le mode SSYNC. Nous avons
présenté le modèle ASYNC au paragraphe 2.3. Ce modèle est largement utilisé dans la littérature et afin de
servir davantage de réalisme nous l’avons implémenté dans PACTOLE.
Nous décrivons cette intégration au modèle formel et illustrons son utilisabilité en établissant formellement
une preuve d’équivalence entre deux modèles de graphes utilisant cette synchronisation.

6.1 Rappels sur ASYNC

Pour rappel, le modèle ASYNC a comme principe de ne plus utiliser la séparation du temps en round mais de
rendre indépendants chaque action et chaque robot. Dans ce modèle, chaque robot réalise ses actions Look,
Compute ou Move à son propre tempo, qui peut ne pas être celui des autres robots.

(a) Une exécution de quatre robots dans le (b) La même exécution, mais avec les lignes modèle A SYNC. rouges marquant les
différentes actions.

Figure 6.1

Dans la figure 6.1, les traits rouges représentent chaque instant où il y a un changement pertinent dans la
configuration. Il est important de remarquer que, contrairement aux modes FSYNC et SSYNC, ce mode

Figure 6.2: Un exemple où pendant que le robot dans la ligne supérieure calcule sa prochaine destination, le
robot de la ligne inférieure a bougé : le mouvement du premier robot est décidé en fonction d’informations
périmées.

n’utilise plus la notion de round. De ce fait, il est possible voire même probable qu’un robot prenne une décision
sur des informations périmées.
En effet, si un robot prend un snapshot de son environnement, et que pendant son temps de calcul, l’état du
système est modifié, par exemple par un robot se déplaçant, alors le robot initial bougera vers une nouvelle
position en fonction d’informations qui ne sont plus exactes au commencement de son mouvement (voir figure
6.2).

6.2 Implémentation
Les modèles asynchrones n’utilisent pas dans la littérature la notion de round mais il existe bien des
changements dans l’exécution. Nous avons choisi de regarder l’état de l’exécution à chaque changement d’état
d’un robot. Il faut re-vérifier l’état d’un robot dès que quelque chose change dans tout autre robot. Cela
correspond à chaque trait rouge dans 6.1.
 Le snapshot dans la phase Look est instantané. Il est donc possible de découper la phase Look en une période
d’inactivité pour le robot suivie à la fin du temps défini pour l’action par un snapshot instantané comme
présenté à la figure 6.4.
Il n’y a pas de différence observable entre un calcul qui s’étend entre deux instants t1 et t2 et un calcul
instantané en t1 suivi d’une période d’inactivité jusqu’à t2. Il est
donc possible de découper la phase Compute en un calcul
instantané de la prochaine destination, suivi d’un temps
d’inactivité du robot correspondant à son temps de calcul réel comme présenté à la figure 6.5.
Notre cycle est maintenant constitué de deux actions instantanées, des périodes d’inactivité et le
mouvement. Ces périodes d’inactivité peuvent être considérées comme des moments où le robot est en
mouvement mais où le mouvement est nul, sans perte de généralité. De plus, les deux actions instantanées
étant juste l’une après l’autre, il est possible de les regrouper en une seule action Look-Compute.
Nous avons donc un modèle fonctionnant en alternance de deux états, un état où le robot est activé et fait
l’action Look-Compute, et un état où le robot est inactif, et dans lequel il ne fait que se déplacer (6.3).

Look/Compute

Activé Inactif Move

Move

Figure 6.3: Les deux états du robot en ASYNC, et quelles actions mènent à quels états.

Pour implémenter le fait que l’action Move peut maintenant durer plusieurs activations du robot, nous
ajoutons des informations dans le state des robots pour pouvoir continuer les mouvements en cours.
sembler contredire qu’un robot peut se déplacer durant le calcul de la prochaine destination d’un autre
robot mais ledit premier mouvement peut être nul si le démon représente le robot toujours en train de calculer.

Figure 6.7: Représentation schématique du graphe continu à vision discrète:

représente le robot sur
l’arête, représente un sommet du graphe etreprésente le sommet où est perçu le robot, avec la ...
...
zone de perception. La limite de cette zone de perception est le seuil de l’arête, dès que le robot la dépasse et
arrive dans la zone il n’est plus vu sur le même sommet.

6.3 ASYNC en action : une preuve d’équivalence

Pour illustrer ce fonctionnement de l’asynchrone, nous allons présenter une preuve d’équivalence entre deux
modèles de graphes, le modèle de graphes discret et le modèle de graphe continu avec observation discrète
(voir figure 6.7).
Dans les études du point de vue algorithmique distribuée des agents évoluant dans des graphes, les seuls
déplacements considérés sont « plus » que rigides et on peut quasiment parler de téléportation : le Move est
atomique d’un noeud à l’autre (mais peut survenir n’importe quand). On peut donc objecter que les aspects
ASYNC sont fortement contraints car on ne peut pas voir un robot en train de se déplacer, comme on l’aurait en
ASYNC dans un espace continu11.

11 On a cependant toujours la propriété que l’on peut baser son mouvement sur une observation obsolète.
 round rbg da
c next_c

config_G2V config_V2G config_G2V config_V2G

c’ next_c’
round rbg’ da’

Figure 6.12: Bisimulation: pour tout robogramme rbg, l’action démoniaque da et la configuration c dans le
modèle discret, la traduction de la configuration next_c résultant de la fonction de transition round équivaut au
résultat next_c’ de la fonction de transition appliquée aux traductions de chacun des trois paramètres da’rbg’ et c’
dans le modèle continu. L’inverse est vrai aussi, en traduisant dans l’autre sens chacun des paramètres.

Étude de cas : maintien de connexion dans

un réseau dynamique
Nous illustrons certaines des possibilités offertes par le cadre formel en étudiant un scénario
d’application des essaims de robots : le maintien d’une connexion entre une cible aux déplacements
arbitraires (dans des limites de vitesse acceptables) et une base fixe, à l’aide d’une chaîne de robots
autonomes.
Ce cas d’application peut par exemple servir à suivre une équipe de recherche et secours tout en lui
apportant un réseau ad-hoc de communication avec le centre de ressources.
Notre étude est découpée en deux parties : la poursuite d’une
cible par un groupe de robots, sans collision, puis son enrichissement
avec l’émission possible de
nouveaux robots (volumiques)
par une base fixe.
Dans notre problème, nous
voulons que l’essaim suive une
cible présentant les mêmes
caractéristiques de mouvement
que les robots, en particulier la vitesse de déplacement. Nous la
désignerons en conséquence comme robot libre, non soumis au
protocole. Nous choisissons également cette dénomination pour
éviter les confusions avec les objectifs de déplacements (donc
cibles) des robots qui ne perçoivent pas le robot libre.

Figure 7.1: Le robot libre Figure 7.2: Nous cherchons à toujours avoir tous les est
perçu par le robot car il est dansrobots dans le graphe de visibilité d’un robot percevant le robot libre. Le robot
sa zone de détection . est ainsi lié au robot libre car dans le graphe de visibilité de .
Hypothèses
• L’espace considéré est R2.

• Les robots sont oublieux. Ils ne sont pas opaques. Nous leur ajouterons effectivement un volume dans la
deuxième partie.

• Ils sont identifiés par un numéro strictement positif et équipés d’une lumière à deux états distinguables.

• Le robot libre est perçu comme un robot d’identifiant 0.

• Les capteurs ont tous la même portée limitée ; ils détectent identifiants et couleurs. Les figures 7.1 et 7.2
montrent des exemples de vision des robots.
 • Les robots ont tous la même vitesse maximale de déplacement.

• Le mode de synchronisation est FSYNC12.

• Les robots disposent d’un dispositif d’élimination arbitraire qui leur permet de se retirer de l’espace
considéré. On peut dans le cas d’une application réelle penser à un changement de plan d’altitude, etc.

7.1 Protocoles de poursuite et connexion

7.1.1 Définitions
Les robots pouvant être sujets à des collisions, nous définissons les zones dans lesquelles ils sont respectivement
en quasi-contact et en danger. Nous introduisons les zones de poursuite de cible et de relais.

• Nous nommons D la distance maximale que tout robot peut parcourir en un round.

• Dmax correspond au rayon de visibilité défini au chapitre 2. Cette distance dépend ici de D, car pour
éviter les collisions mais toujours garder en vue d’autres robots, il est nécessaire d’avoir une vision
Dmax ≥ 6 × D. Cette valeur de Dmax nécessaire pourra évoluer suivant les problèmes.

À partir de ces distances, nous définissons quatre zones:

Définition 7.1.1 (Zone de Mort.) La zone de mort est le disque de rayon D autour du robot. Si un autre robot se
trouve dans la zone de mort d’un robot donné, ces deux robots peuvent se percuter et ainsi faire échouer la
tâche.

Définition 7.1.2 (Zone de Danger.) La zone de danger est la zone entre les cercles de rayon D et 2×D. Si un
robot est dans cette zone, il faut y faire attention car il risque de rentrer dans la zone de Mort.

Définition 7.1.3 (Zone de Poursuite.) La zone de poursuite est la zone entre les cercles de rayon Dmax et
Dmax − D. Si un robot est dans la zone de poursuite d’un robot t et ne doit pas être perdu de vue, il faut que
t bouge vers lui car sinon il risque de sortir de son champ de vision. Nous noterons Dp = Dmax − D la
distance de poursuite.

Définition 7.1.4 (Zone de Relais.) La zone de relais correspond à la surface entre les cercles de rayons 2×D et Dp.
Les robots dans cette zone servent de relais : ce sont des nœuds dans le graphe de visibilité.

Ces zones sont schématisées dans la figure 7.3.

12
 D D
D max D max

(a) Zone de mort. (b) Zone de danger.

D D
D max D max

(c) Zone de relais. (d) Zone de poursuite.

Figure 7.3: Les différentes zones du robot (en bleu).

7.1.2 Le choix de la cible

Le problème majeur rencontré dans cette tâche consiste à éviter les collisions. Il n’est pas raisonnable de
prendre en compte les mouvements possibles de tous les robots visibles. Il serait en effet très facile d’arriver
dans des situations de blocage comme présenté à la figure 7.4.
Nous choisissons de ne prendre en compte, dans le calcul de destination d’un robot r, que les robots visibles
d’identifiant r0 < r. Le robot libre est en particulier toujours pris en compte lorsqu’il est visible.
 B

+
C C
A A

Figure 7.4: si le robot A veut se rapprocher du seul robot d’identifiant plus petit visible Bmais
que, sur son chemin, un robot d’identifiant supérieur C menace de rentrer dans la zone de mort, notre
premier robot ne peut pas bouger et risque de perdre de vue le robot d’identifiant inférieur
donc de
casser le chemin entre lui et le robot libre.

Les robots d’identifiants inférieurs à r ne prennent pas r en compte pour leurs déplacements, c’est donc à r
de sortir de leur chemin éventuel.
Pour obtenir un résultat le plus général possible, c’est-à-dire sans fournir de code de protocole mais plutôt
des propriétés à respecter, nous nous interdisons de deviner comment les robots vont bouger. Dès lors, il est
indispensable pour chaque robot de bouger à une position pour laquelle aucun robot d’identifiant inférieur ne
peut se trouver dans la zone de Mort.
Ne connaissant pas le comportement des robots d’identifiants inférieurs, il est possible qu’ils se rapprochent
de la position choisie, et donc il faut rajouter la zone de Danger à celle de Mort dans les zones à éviter. Il faut
également toujours maintenir la connexion avec la cible choisie au départ, et donc rester à une distance
maximale de Dp de la position actuelle de notre cible pour forcément la garder en vue au tour suivant.
Que se passe-t-il s’il n’existe aucune position répondant à ces critères?
Il n’est pas possible de supprimer du réseau tout robot ne trouvant pas de position adéquate pour éviter tout
risque de collision. Une suppression si directe risque de casser la chaîne.
Une solution est apportée ici par les lumières: un robot ne pouvant pas bouger à une position sûre allume
une lumière pour indiquer qu’il est en danger et ne bouge pas. Si lors du calcul des destinations au tour suivant,
un robot se trouve dans sa zone de Mort, alors il se désactive directement et donc nous ne prenons pas le risque
d’avoir des collisions.
Avec l’ajout de cette nouvelle donnée, nous affinons le choix de la cible: la cible choisie par un robot est
prioritairement éteinte, c’est-à-dire qu’elle n’était pas en danger au tour précédent. Si toutefois il n’existe que
des robots allumés dans le champ de vision d’un robot, ce dernier privilégiera comme cible un robot à moins de
Dp de lui.
Nous montrerons lors de la preuve du lemme exists_at_less_round de la section suivante 7.2 que, même s’il
n’existe dans le champ de vision que des robots allumés, il en existe au moins un à moins de Dp.
Un autre cas extrême est à prendre en compte: que ce passe-t-il si le robot ne voit aucun autre robot ? Dans
ce cas là, le robot doit s’éliminer car il ne peut plus aider à la poursuite du robot libre. Ce cas se révélera
toutefois impossible à atteindre en partant d’une configuration correcte.

Pour résumer nous prétendons que tout protocole respectant les étapes suivantes remplit notre objectif
:

1. Le robot fait un snapshot de son environnement en ne prenant que les robots d’identifiants inférieurs.
 2. Pendant la phase Compute, s’il trouve un robot à moins de D ou s’il ne trouve aucun autre robots, il
s’élimine13.

3. Le robot choisit le robot qu’il veut suivre, forcément un robot d’identifiant inférieur.

4. Ayant choisi le robot à suivre pour cible, le robot détermine maintenant une position à moins de Dp de sa
cible, et à moins de D de sa position actuelle.

(a) S’il existe un robot d’identifiant inférieur à moins de 2 × D de cette position choisie, alors le robot ne
bouge pas et allume sa lumière, (b) Sinon le robot bouge vers cette position.

Notre objectif étant d’avoir à chaque point de l’exécution un ensemble de robots pour lequel le robot libre
est dans le graphe de visibilité et chaque robot de cet ensemble se déplace en évitant les collisions.

7.2 Preuve formelle

Nous voulons prouver formellement qu’il existe toujours un chemin dans le graphe de visibilité entre un robot et
le robot libre, mais aussi qu’à aucun moment, deux robots ne rentrent en collision. Pour ce faire, nous utilisons
PACTOLE.

7.2.1 Définitions COQ

Nous commençons avec un nombre n non défini de robots, parmi lesquels il n’existe aucun byzantin:
Parameter n: nat.

(* Il y a n "bons" robots et 0 byzantin *)

Instance Identifiers : Names := Robots n 0.

L’état du système dans PACTOLE

Puis, nous définissons l’espace dans lequel se déplacent les robots comme suit:
Instance Loc : Location := make_Location (R2).

Comme nous l’avons vu en posant nos hypothèses, les robots n’ont pas accès uniquement à leur position
mais aussi à d’autres informations: leur lumière, que nous caractériserons par un booléen, valant true si cette
lumière est allumée, ainsi que l’identifiant de ce robot. Nous ajoutons enfin un deuxième booléen valant true
pour un robot considéré comme vivant, ou false pour un robot éliminé.
Definition identifiants := nat.
(*variable pour savoir si les robots sont allumes ou pas: Si la variable de type [light] est a true, il est
allume*) Definition light := bool.
Definition alive := bool.

Une configuration est la position dans R×R avec en plus les informations concernant l’identifiant, la lumière
et le statut vivant ou non du robot.
Nous avons donc d’une part la position définie dans R2 (notation COQ de R×R) ainsi que d’autre part le reste
des informations nécessaires au bon déroulement du protocole dans un type nommé ILA (pour Identifiant Light
Alive). Ce type est un triplet comprenant un entier naturel représentant l’identifiant du robot et deux booléens
représentants respectivement si la lumière du robot est allumée et si le robot est vivant.
Nous avons donc l’état du système suivant:
(* Notre etat a comme type des positions R2, et comme type d’informations accessibles (R2*ILA) *)
Instance State_ILA : @State (make_Location R2) (R2*ILA) := (* il est cree en creant en premier lieu un
etat ou seul les positions (R2) sont decrites, puis en ajoutant les informations
(ILA) *)
[Link]
Il reste à étudier les cas selon l’état de c:
13
 • Si c est éteint, il ne s’élimine pas grâce à la propriété executed_means_light_on, comme r bouge vers loc(c)
suffisamment pour que la distance soit au plus Dp, la distance entre locr(r) et locr(c) est au plus Dmax.

• Si c est allumé, il risque de s’éliminer. Selon les règles que nous nous sommes imposées dans la partie
7.1.2 pour choisir une cible, si c est allumé, alors tous les robots visibles le sont. De plus, par la propriété
exists_at_less_that_Dp, il en existe au moins un tel que sa position soit à moins de Dp. En utilisant encore les
règles de choix de la cible, c est alors aussi à moins de Dp. Comme tous les robots sont allumés, il ne peut
pas y avoir de robot provoquant l’élimination d’un autre robot, ceux-ci étant forcément éteints par la
propriété executioner_means_light_off. Il n’existe donc pas de bourreau pour c, qui sera vivant au round
suivant, et sera un robot à moins de Dmax de r.

Si r est gêné par g

Il n’est pas possible de se déplacer vers c à cause du robot gênant g, donc loc(g) est à moins de 3 × D de loc(r),
étant à moins de 2 × D d’une position à moins de D de loc(r). Dans ce cas là, loc(r) = locr(r), et nous faisons
attention à l’état de g. Si g ne s’élimine pas, locr(g) est à au plus 3 × D + D de loc(r), donc à moins de Dmax. Si g
s’élimine, il existe donc un robot bourreau b, avec dist loc(b) loc(g) ≤ D. Or, comme b est un bourreau, il doit
avoir sa lumière éteinte en respectant executioner_means_light_off. Ainsi b est éteint et ne s’éliminera pas au tour
prochain, ce qui le rend éligible à être le robot vivant à moins de Dmax de locr(r).
Nous avons donc prouvé que l’existence d’un chemin était préservée si les autres propriétés l’étaient.
Lemma validity:
(* pour tout demon et toute configuration de depart *)
∀(demon : demon_ila_type) conf,
(* si la configuration de depart est une configuration valide *) conf_pred conf→
(* et que le demon est bien defini *) demon_ILA demon→
(* alors il n’y a pas de collision et le chemin entre tout robot et le robot cible est preserve*)
NoCollAndPath (execute rbg_ila demon conf).

Nous avons donc le théorème suivant: en partant d’une configuration initiale correcte, les prédicats
d’existence du chemin et de non collision entre les robots sont préservés.
no_collision no_collision_cont

path_round

path_conf round_target_alive

executioner_means_light_off_round

executioner_means_light_off NoCollisionAndPath

executed_means_light_on_round

executed_means_light_on exists_at_less_round

exists_at_less_that_Dp

Figure 7.9: Représentation des dépendances pour la preuve. Les flèches pointillées représentant les dépendance
des prédicats sur une configuration, alors que les flèches pleines sont les dépendance des fonction entre deux
configuration successives. Les couleurs représente quel prédicat est prouvé.
Conclusion
Nous nous sommes intéressés à l’enrichissement d’une bibliothèque formelle afin d’offrir les moyens de garantir
résultats théoriques et comportements de protocoles distribués dans un modèle émergent : les essaims de
robots mobiles.
En considérant un modèle à l’énoncé simple mais présentant une grande diversité d’ajustements possibles,
nous nous sommes appuyés sur un prototype pour la preuve formelle dans ce cadre : la bibliothèque PACTOLE14.
Le prototype précédant nos travaux reste essentiellement proche de la preuve de concept. Il permet
toutefois d’exprimer des systèmes de robots évoluant dans des espaces continus, de type plan réel R 2, pour des
démons totalement ou semi-synchrones, avec des déplacements rigides ou flexibles.
Ce sont des possibilités suffisantes pour garantir ou établir certains résultats d’impossibilité ou de correction
de protocoles. Ce sont néanmoins des limitations dans l’usage qu’on veut courant et aisé de la vérification, en
particulier dans la perspective d’aborder des cadres et applications réalistes des essaims de robots.
Il fallait donc à ce stade des extensions du cadre formel, d’une part, à des préoccupations non abordées mais
pourtant courantes dans la littérature sur les essaims de robots mobiles, à savoir les problématiques sur les
graphes, et, d’autre part, à des contextes plus réalistes : dans les espaces, dans les caractéristiques des robots,
dans la caractérisation du synchronisme des exécutions.

Contributions
Nous proposons des évolutions majeures du cadre formel correspondant à ces attentes.
Dans un premier temps, nous permettons la prise en compte des graphes : nous définissons classes et
interfaces pour une expression de ces espaces aisée et suffisamment simple pour qu’un non spécialiste de la
preuve formelle puisse les aborder.
Il ne suffit pas de pouvoir exprimer un objet, il faut bien sûr que celui-ci soit effectivement manipulable dans
un développement formel. Nous illustrons l’utilisabilité de notre extension en donnat la première preuve
formelle de l’impossibilité de l’exporation avec stop dans un anneau quand le nombre de robots divise la taille
de l’anneau. Ces premières contributions sont publiées dans les actes de la conférence internationale
ICDCN2018 [12].
Dans un deuxième temps, nous abordons le type de synchronisation le plus complexe et le plus général : le
mode asynchrone. Étendre le cœur du modèle aux exécutions asynchrones entraîne une généralisation de la
plupart des constructions existantes dans la bibliothèque formelle. De nouveau, nous montrons que notre
extension est utilisable. Nous prouvons formellement une équivalence en mode asynchrone entre deux
variantes de graphes, graphes discrets d’une part, graphes continus (c’est-à-dire où les agents se déplacent
continûment le long des arêtes) d’autre part mais avec détection dans le voisinage des sommets. Cette preuve
utilise bien sûr notre modélisation des graphes. Ces travaux sont présentés et publiés sous forme courte dans les
actes de la conférence SSS2018 [7] et sous forme normale dans les actes des conférences N ETYS2019 [8] et
ALGOTEL2020 [9].
Enfin, dans un troisième temps, nous explorons toujours plus de réalisme et travaillons à la représentation
des robots présentant un volume et, donc, des risques de collision. Nous développons et exprimons dans le
cadre formel étendu à dessein un protocole permettant de maintenir, par un essaim de robots mobiles, un
chemin de connexions (à portées limitées) entre une base fixe et une cible mobile. Nous établissons
formellement que notre protocole garantit le maintien de la connexion entre la base et la cible à tout point
d’une exécution synchrone et sans collision.

14