Soutenance mémoire
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 radiations . La perte de matériel coûteux 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.
Un modèle pour l’étude des essaims de robots
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 ; 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.
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.
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. 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.
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. Certains travaux supposent toutefois des quantités de mémoire persistante et étudient la réalisabilité de certaines tâches en fonction de ces quantités .
Volume, collisions. Les hypothèses les plus faibles considèrent les robots comme
• Ponctuels (ils n’ont pas d’épaisseur),
• Transparents (ils ne masquent pas la perception),
• Sans collision (deux robots peuvent se trouver au même endroit exact, se croiser sans problème).
Le souci de réalisme a bien sûr amené à revisiter ces propriétés et proposer des robots volumiques. Deux robots volumiques peuvent se toucher mais pas se superposer. Si jamais lors d’un mouvement deux robots venaient à rentrer en collision, ils seraient considérés comme devenant fautifs. La perception de ce volume entraîne le partage d’une unité de distance commune ; ces robots peuvent être vus comme des boules d’un diamètre donné. Notons que la notion de volume n’entraîne pas forcément l’opacité des robots et il existe des études sur des robots volumiques mais transparents [29, 34, 47].
|
Table des matières
1 Introduction
2 Un modèle pour l’étude des essaims de robots
2.1 L’espace
2.2 Les robots
2.2.1 Capteurs, perception
2.2.2 Le comportement
2.3 Caractéristiques de synchronisation
2.4 Accomplir une tâche, principaux problèmes étudiés
2.4.1 Formation de figures
2.4.2 Exploration, le cas des graphes
2.4.3 Puissances de quelques variantes
3 Méthodes formelles
3.1 Model-checking
3.2 Preuve formelle
3.3 COQ
4 Pactole
4.1 L’espace
4.2 Les robots
4.2.1 Capteurs, perceptions
4.2.2 Le comportement
4.3 Caractéristiques de synchronisation
4.3.1 Round
4.3.2 Propriétés des démons
4.4 Quelques résultats
5 Graphes comme espaces dans PACTOLE
5.1 Modèle général des graphes
5.2 Exemples de graphes particuliers
5.3 Graphes en action : une preuve d’impossibilité
5.3.1 Exploration avec stop
5.3.2 Argument de preuve
5.3.3 Formalisation de l’impossibilité de l’exploration avec stop
6 Exécutions ASYNC dans PACTOLE
6.1 Rappels sur ASYNC
6.2 Implémentation
6.3 ASYNC en action : une preuve d’équivalence
6.3.1 Modélisation des deux types de graphes
6.3.2 Traductions entre les modèles
6.3.3 Équivalence des modèles
7 Étude de cas : maintien de connexion dans un réseau dynamique
7.1 Protocoles de poursuite et connexion
7.1.1 Définitions
7.1.2 Le choix de la cible
7.2 Preuve formelle
7.2.1 Définitions COQ
7.2.2 Prédicats
7.2.3 no_collision
7.2.4 executed_means_light_on
7.2.5 executioner_means_light_off
7.2.6 exists_at_less_that_Dp
7.2.7 path_conf
7.3 Une base fixe à relier à la cible
7.3.1 Ajouts dans les définitions
7.3.2 Les prédicats ajoutés
7.4 Des robots avec un volume
8 Conclusion
