MILLET Laure
Supervision : Béatrice BÉRARD
Co-supervision : POTOP-BUTUCARU Maria, SZNAJDER Nathalie
Verification and synthesis of robot protocols
The topic of autonomous mobile robots continues to generate a lot of interest in the algorithmic community, both from a purely theoretical perspective and from a more applicative one. The model is now well understood, and the problems under investigation are becoming more and more complex. Correctness proofs are usually very intricate and elaborate, often leaving margin of doubts.
This thesis focuses on a new approach to formally study correctness in robots systems and to automatically generate algorithmic solutions.
In fact, we propose a general framework to express robot models, and where automated technics like model checking and algorithm synthesis can be used, moreover we show their applicability in robots models under all possible synchronicity levels (from fully synchronous to fully asynchronous).
Defence : 12/01/2015
Jury members :
Paola Flocchini, Professeur, Ottawa University, Canada [Rapporteur]
Stephan Merz, Professeur, INRIA Nancy & LORIA [Rapporteur]
Béatrice,Bérard, Professeur, LIP6,UPMC
Amal El Fallah Seghrouchni, Professeur, LIP6, UPMC
Laure Petrucci,Professeur, LIPN, Paris 13
Maria Potop-Butucaru, Professeur, LIP6, UPMC
Nathalie Sznajder, Maitre de Conférences LIP6, UPMC
Xavier Urbain, Maitre de Conférences, LRI
Josef Widder, Professeur, TU, Wien, Austria
2012-2016 Publications
-
2016
- B. Bérard, P. Lafourcade, L. Millet, M. Potop‑Butucaru, Y. Thierry‑Mieg, S. Tixeuil : “Formal verification of mobile robot protocols”, Distributed Computing, vol. 29 (6), pp. 459-487, (Springer Verlag) (2016)
-
2015
- L. Millet : “Verification and synthesis of robot protocols”, thesis, phd defence 12/01/2015, supervision Bérard, Béatrice, co-supervision : Potop-butucaru, Maria, Sznajder, Nathalie (2015)
- L. Millet, M. Potop‑Butucaru, N. Sznajder, S. Tixeuil : “Synthèse d’algorithmes pour robots mobiles : le cas du regroupement sur un anneau”, ALGOTEL 2015 — 17es Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications, Beaune, France (2015)
- B. Bérard, P. Courtieu, L. Millet, M. Potop‑Butucaru, L. Rieg, N. Sznajder, S. Tixeuil, X. Urbain : “[Invited Paper] Formal Methods for Mobile Robots: Current Results and Open Problems”, International Journal of Informatics Society, vol. 7 (3), pp. 101-114, (Japan Informatics Society) (2015)
-
2014
- L. Millet, M. Potop‑Butucaru, N. Sznajder, S. Tixeuil : “On the Synthesis of Mobile Robots Algorithms: the Case of Ring Gathering”, SSS 2014 - 16th International Symposium on Stabilization, Safety and Security of Distributed Systems, vol. 8756, Lecture Notes in Computer Science, Paderborn, Germany, pp. 237-251, (Springer) (2014)
-
2013
- B. Bérard, L. Millet, M. Gradinariu Potop‑Butucaru, Y. Thierry‑Mieg, S. Tixeuil : “Vérification formelle et robots mobiles”, 15es Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications (AlgoTel), Pornic, France, pp. 1-4, (Nisse, Nicolas et Rousseau, Franck et Busnel, Yann) (2013)
- B. Bérard, L. Millet, M. Potop‑Butucaru, Y. Thierry‑Mieg, S. Tixeuil : “Formal verification of Mobile Robot Protocols”, (2013)
-
2012
- L. Millet, M. Lorrillere, L. Arantes, S. Gançarski, H. Naacke, J. Sopena : “Facing peak loads in a P2P transaction system”, Proceedings of the First Workshop on P2P and Dependability (P2PDEP'12), P2P-Dep '12, Sibiu, Romania, pp. 1-7, (ACM) (2012)