Title
A Foundational Framework for Certified Impossibility Results with Mobile Robots on Graphs.
Abstract
Swarms of mobile robots recently attracted the focus of the Distributed Computing community. One of the fundamental problems in this context is that of exploration: the robots must coordinate to visit all locations that are reachable from their initial positions. Despite its apparent simplicity, this problem proved quite hard to characterise fully, due to many model variants, leading to informal error-prone reasoning. Over the past few years, a significant effort permitted to set up a formal framework, relying on the Coq proof assistant, which was used to provide certified results when robots evolve in a continuous bi-dimensional Euclidean space. However, the most challenging issues with exploration arise in the discrete setting (a.k.a. graph), where locations are modeled as vertices and where edges between vertices denote the ability for a robot to move from one location to the next. We present a formal model to tackle problems and reason about robot algorithms arising in the discrete setting. Our approach extends and generalises previous research efforts focusing on the continuous model. As case studies, we consider fundamental impossibility results for exploration with stop in the discrete model. To our knowledge, those are the first certified results in this context. This framework paves the way for a general certification workflow dedicated to mobile robots on graphs.
Year
DOI
Venue
2018
10.1145/3154273.3154321
ICDCN'18: PROCEEDINGS OF THE 19TH INTERNATIONAL CONFERENCE ON DISTRIBUTED COMPUTING AND NETWORKING
Keywords
Field
DocType
Mobile Robots,Proof Assistant,Exploration,Impossibility results
Continuous modelling,Vertex (geometry),Computer science,Impossibility,Euclidean space,Theoretical computer science,Robot,Workflow,Mobile robot,Distributed computing,Proof assistant
Conference
Citations 
PageRank 
References 
1
0.35
19
Authors
4
Name
Order
Citations
PageRank
Thibaut Balabonski1206.56
Robin Pelle210.69
Lionel Rieg3456.91
Sébastien Tixeuil497893.01