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.