|
 
|
[CRT15a] Impossibility of Gathering, a Certification
Revue Internationale avec comité de lecture : Journal Information Processing Letters, vol. 115, pp. 447-452, 2015, (doi:10.1016/j.ipl.2014.11.001)Mots clés: Analysis of algorithms Automatic theorem proving Computational geometry Distributed computing Theory of computation
Résumé:
Recent advances in Distributed Computing highlight models and algorithms for autonomous
swarms of mobile robots that self-organise and cooperate to solve global objectives. The
overwhelming majority of works so far considers handmade algorithms and proofs of
correctness.
This paper builds upon a previously proposed formal framework to certify the correctness
of impossibility results regarding distributed algorithms that are dedicated to autonomous
mobile robots evolving in a continuous space. As a case study, we consider the problem
of gathering all robots at a particular location, not known beforehand. A fundamental (but
not yet formally certified) result, due to Suzuki and Yamashita, states that this simple task
is impossible for two robots executing deterministic code and initially located at distinct
positions. Not only do we obtain a certified proof of the original impossibility result, we
also get the more general impossibility of gathering with an even number of robots, when
any two robots are possibly initially at the same exact location.
Equipe:
sys
Collaboration:
LIP6
BibTeX
| @article { | |||
| CRT15a, | |||
| title | = | "{Impossibility of Gathering, a Certification}", | |
| author | = | "P. Courtieu and L. Rieg and S. Tixeuil and X. Urbain", | |
| journal | = | "Information Processing Letters", | |
| year | = | 2015, | |
| volume | = | 115, | |
| pages | = | "447-452", | |
| doi | = | "10.1016/j.ipl.2014.11.001", | |
| } | |||
