Séminaire APRRSS

Un cadre formel adapté aux réseaux de robots mobiles.


http://www.ensiie.fr/~urbain/
10/04/2015
Intervenant(s) : Xavier Urbain
Les réseaux de robots mobiles reçoivent depuis quelques années une attention croissante de la part de la communauté de l'algorithmique distribuée. Si l'utilisation d'essaims de robots coopérant dans l'exécution de diverses tâches est une perspective séduisante, l'analyse de la faisabilité de certaines tâches dans ce cadre émergent est extrêmement ardue, en particulier si certains robots présentent des comportements dits byzantins, c'est-à-dire arbitraires voire hostiles.
Pour obtenir des garanties formelles dans ce contexte, nous proposons un cadre mécanique formel fondé sur l'assistant à la preuve Coq et adapté aux réseaux de robots. Nous nous intéressons principalement dans cet exposé aux résultats d'impossibilité, fondamentaux en ce qu'ils établissent ce qui peut ou ne peut pas être réalisé et permettent de définir des bornes et, par là, l'optimalité de certaines solutions.
Utiliser un assistant comme Coq travaillant à l'ordre supérieur nous permet d'exprimer aisément des quantifications sur les algorithmes, ceux-ci étant considérés comme des objets abstraits. Nous illustrons les possibilités offertes par notre développement en présentant les premières preuves formelles (et donc certifications) de certains résultats comme l'impossibilité de la convergence de robots amnésiques lorsqu'un tiers d'entre eux sont byzantins, ou encore l'impossibilité du rassemblement pour un nombre pair de robots évoluant dans R.
Plus d'informations ici
 Mentions légales
Carte du site |