Du discrètement continu au continûment discret

National audience; Les robots mobiles oublieux ont été étudiés à la fois dans des espaces euclidiens continus et dans des espaces discrets (c'est-à-dire des graphes). Cependant, l'état de l'art actuel forme des ensembles de résultats distincts pour les deux modèles. À notre avis, le modèle continu reflète bien la physicalité des robots fonctionnant dans un environnement réel, tandis que le modèle discret reflète bien la nature numérique des robots autonomes, dont les capteurs et les capacités de calcul sont intrinsèquement finis. Nous explorons la possibilité de faire le pont entre les deux modèles. Notre approche est certifiée à l'aide de l'assistant de preuve Coq et du framework Pactole, que nous étendons au modèle asynchrone (le plus général) sans compromettre sa généricité. Notre cadre étendu est ensuite utilisé pour prouver formellement l'équivalence entre les mouvements atomiques dans un espace discret (le modèle classique des «robots sur les graphes») et les mouvements non atomiques dans un espace unidimensionnel continu lorsque les capteurs de vision du robot sont discrets (les robots se déplacent en ligne droite entre les positions, mais leurs observations ne se traduisent que par les positions de départ ou d'arrivée), quel que soit le problème résolu. Notre effort consolide l'intégration entre le modèle, la spécification du problème et sa preuve prônée par le framework Pactole.