Encadrant : Lionel Rieg
Les réseaux de robots autonomes permettent d’utiliser des comportements émergeant de protocoles distribués simples, tout en garantissant une grande résilience et flexibilité dans la taille de l’essaim. Lorsqu’un essaim de robots mobiles est utilisés dans un cadre critique, par exemple lorsque des vies sont en jeu, il est impératif d’avoir les plus fortes garanties de correction possibles sur les protocoles, c’est-à-dire sur le comportement de l’essaim par rapport à ce qu’on en attend. On s’intéresse donc à la preuve formelle dans le cadre des robots mobiles, en particulier avec l’assistant de preuve Coq et la bibliothèque Pactole.
Le but de ce travail est de proposer un mécanisme de dispersion, sans collision, de robots à vision limitée afin d’obtenir une couverture d’une zone prédéfinie, dans un cadre de perception imparfaite (par masquage ou imprécisions des capteurs). On s’attachera à modéliser voire prouver formellement la correction du nouveau protocole obtenu.
Pour plus de détails, voir la description pdf.
