|
 
|
[CT17] Certified Gathering of Oblivious Mobile Robots: Survey of Recent Results and Open Problems
Conférence Internationale avec comité de lecture : FMICS-AVoCS 2017, September 2017, Vol. 10471, pp.165-181, Series LNCS, Turin, Italy, (DOI: 10.1007/978-3-319-67113-0_11)Mots clés: swarm of robots, verification, proof assistant
Résumé:
Over the past few years, a significant effort has resulted in the set up of a formal framework, relying on the Coq proof assistant, that was used to provide certified results related to the gathering problem. We survey the main abstractions that permit to reason about oblivious mobile robots that evolve in a bidimensional Euclidean space, the distributed executions they can perform, and the variants of the gathering problem they can solve, while certifying all obtained results. We also describe the remaining steps to obtain a certified full characterisation of the problem.
Collaboration:
LIP6
BibTeX
| @inproceedings { | |||
| CT17, | |||
| title | = | "{Certified Gathering of Oblivious Mobile Robots: Survey of Recent Results and Open Problems}", | |
| author | = | " P. Courtieu and S. Tixeuil ", | |
| booktitle | = | "{FMICS-AVoCS 2017}", | |
| year | = | 2017, | |
| month | = | "September", | |
| series | = | "LNCS", | |
| volume | = | 10471, | |
| pages | = | "165-181", | |
| address | = | "Turin, Italy", | |
| doi | = | "10.1007/978-3-319-67113-0_11", | |
| } | |||
