Certified Gathering of Oblivious Mobile Robots: Survey of Recent Results and Open Problems

  • Thibaut Balabonski
  • Pierre Courtieu
  • Lionel Rieg
  • Sébastien Tixeuil
  • Xavier UrbainEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10471)


Swarms of mobile robots have recently attracted the focus of the Distributed Computing community. One of the fundamental problems in this context is that of gathering the robots: the robots must meet at a common location, not known beforehand. 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 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.


  1. 1.
    Agmon, N., Peleg, D.: Fault-tolerant gathering algorithms for autonomous mobile robots. SIAM J. Comput. 36(1), 56–82 (2006)CrossRefzbMATHMathSciNetGoogle Scholar
  2. 2.
    Auger, C., Bouzid, Z., Courtieu, P., Tixeuil, S., Urbain, X.: Certified impossibility results for byzantine-tolerant mobile robots. In: Higashino, T., Katayama, Y., Masuzawa, T., Potop-Butucaru, M., Yamashita, M. (eds.) SSS 2013. LNCS, vol. 8255, pp. 178–190. Springer, Cham (2013). doi: 10.1007/978-3-319-03089-0_13 CrossRefGoogle Scholar
  3. 3.
    Balabonski, T., Delga, A., Rieg, L., Tixeuil, S., Urbain, X.: Synchronous gathering without multiplicity detection: a certified algorithm. In: Bonakdarpour, B., Petit, F. (eds.) SSS 2016. LNCS, vol. 10083, pp. 7–19. Springer, Cham (2016). doi: 10.1007/978-3-319-49259-9_2 CrossRefGoogle Scholar
  4. 4.
    Bérard, B., Lafourcade, P., Millet, L., Potop-Butucaru, M., Thierry-Mieg, Y., Tixeuil, S.: Formal verification of mobile robot protocols. Dis. Comput. 29(6), 459–487 (2016)CrossRefzbMATHMathSciNetGoogle Scholar
  5. 5.
    Bonnet, F., Défago, X., Petit, F., Potop-Butucaru, M., Tixeuil, S.: Discovering and assessing fine-grained metrics in robot networks protocols. In: SRDS Workshops 2014, pp. 50–59. IEEE (2014)Google Scholar
  6. 6.
    Bouzid, Z., Das, S., Tixeuil, S.: Gathering of mobile robots tolerating multiple crash faults. In: ICDCS, pp. 337–346. IEEE Computer Society (2013)Google Scholar
  7. 7.
    Bouzid, Z., Dolev, S., Potop-Butucaru, M., Tixeuil, S.: Robocast: asynchronous communication in robot networks. In: Lu, C., Masuzawa, T., Mosbah, M. (eds.) OPODIS 2010. LNCS, vol. 6490, pp. 16–31. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-17653-1_2 CrossRefGoogle Scholar
  8. 8.
    Bramas, Q., Tixeuil, S.: Wait-free gathering without chirality. In: Scheideler, C. (ed.) Structural Information and Communication Complexity. LNCS, vol. 9439, pp. 313–327. Springer, Cham (2015). doi: 10.1007/978-3-319-25258-2_22 CrossRefGoogle Scholar
  9. 9.
    Bérard, B., Courtieu, P., Millet, L., Potop-Butucaru, M., Rieg, L., Sznajder, N., Tixeuil, S., Urbain, X.: Formal methods for mobile robots: current results and open problems. Int. J. Inform. Soc. 7(3), 101–114 (2015). Invited PaperGoogle Scholar
  10. 10.
    Cieliebak, M., Flocchini, P., Prencipe, G., Santoro, N.: Distributed computing by mobile robots: Gathering. SIAM J. Comput. 41(4), 829–879 (2012)CrossRefzbMATHMathSciNetGoogle Scholar
  11. 11.
    Cohen, R., Peleg, D.: Convergence properties of the gravitational algorithm in asynchronous robot systems. SIAM J. Comput. 34(6), 1516–1528 (2005)CrossRefzbMATHMathSciNetGoogle Scholar
  12. 12.
    Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: A certified universal gathering algorithm for oblivious mobile robots. CoRR, abs/1506.01603 (2015)Google Scholar
  13. 13.
    Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: Impossibility of gathering, a Certification. Inf. Process. Lett. 115, 447–452 (2015)CrossRefzbMATHMathSciNetGoogle Scholar
  14. 14.
    Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: Certified universal gathering in \({\mathbb{R}}^2\) for oblivious mobile robots. In: Gavoille, C., Ilcinkas, D. (eds.) DISC 2016. LNCS, vol. 9888, pp. 187–200. Springer, Heidelberg (2016). doi: 10.1007/978-3-662-53426-7_14 CrossRefGoogle Scholar
  15. 15.
    Devismes, S., Lamani, A., Petit, F., Raymond, P., Tixeuil, S.: Optimal grid exploration by asynchronous oblivious robots. In: Richa, A.W., Scheideler, C. (eds.) SSS 2012. LNCS, vol. 7596, pp. 64–76. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-33536-5_7 CrossRefGoogle Scholar
  16. 16.
    Dieudonné, Y., Petit, F.: Self-stabilizing gathering with strong multiplicity detection. Theoret. Comput. Sci. 428, 47–57 (2012)CrossRefzbMATHMathSciNetGoogle Scholar
  17. 17.
    Doan, H.T.T., Bonnet, F., Ogata, K.: Model checking of a mobile robots perpetual exploration algorithm. In: Liu, S., Duan, Z., Tian, C., Nagoya, F. (eds.) SOFL+MSVL 2016. LNCS, vol. 10189, pp. 201–219. Springer, Cham (2017). doi: 10.1007/978-3-319-57708-1_12 CrossRefGoogle Scholar
  18. 18.
    Flocchini, P., Prencipe, G., Santoro, N.: Distributed Computing by Oblivious Mobile Robots. Synthesis lectures on distributed computing theory. Morgan & Claypool Publishers, San Rafael (2012)zbMATHGoogle Scholar
  19. 19.
    Flocchini, P., Prencipe, G., Santoro, N., Widmayer, P.: Arbitrary pattern formation by asynchronous, anonymous, oblivious robots. Theor. Comput. Sci. 407(1–3), 412–447 (2008)CrossRefzbMATHMathSciNetGoogle Scholar
  20. 20.
    Fujinaga, N., Yamauchi, Y., Kijima, S., Yamashita, M.: Asynchronous pattern formation by anonymous oblivious mobile robots. In: Aguilera, M.K. (ed.) DISC 2012. LNCS, vol. 7611, pp. 312–325. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-33651-5_22 CrossRefGoogle Scholar
  21. 21.
    Millet, L., Potop-Butucaru, M., Sznajder, N., Tixeuil, S.: On the synthesis of mobile robots algorithms: the case of ring gathering. In: Felber, P., Garg, V. (eds.) SSS 2014. LNCS, vol. 8756, pp. 237–251. Springer, Cham (2014). doi: 10.1007/978-3-319-11764-5_17 Google Scholar
  22. 22.
    Prencipe, G.: Impossibility of gathering by a set of autonomous mobile robots. Theoret. Comput. Sci. 384(2–3), 222–231 (2007)CrossRefzbMATHMathSciNetGoogle Scholar
  23. 23.
    Aminof, B., Murano, A., Rubin, S., Zuleger, F.: Verification of asynchronous mobile-robots in partially-known environments. In: Chen, Q., Torroni, P., Villata, S., Hsu, J., Omicini, A. (eds.) PRIMA 2015. LNCS (LNAI), vol. 9387, pp. 185–200. Springer, Cham (2015). doi: 10.1007/978-3-319-25524-8_12 CrossRefGoogle Scholar
  24. 24.
    Suzuki, I., Yamashita, M.: Distributed anonymous mobile robots: formation of geometric patterns. SIAM J. Comput. 28(4), 1347–1363 (1999)CrossRefzbMATHMathSciNetGoogle Scholar
  25. 25.
    Yamashita, M., Suzuki, I.: Characterizing geometric patterns formable by oblivious anonymous mobile robots. Theor. Comput. Sci. 411(26–28), 2433–2453 (2010)CrossRefzbMATHMathSciNetGoogle Scholar
  26. 26.
    Yamauchi, Y., Yamashita, M.: Pattern formation by mobile robots with limited visibility. In: Moscibroda, T., Rescigno, A.A. (eds.) SIROCCO 2013. LNCS, vol. 8179, pp. 201–212. Springer, Cham (2013). doi: 10.1007/978-3-319-03578-9_17 CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Thibaut Balabonski
    • 6
  • Pierre Courtieu
    • 1
  • Lionel Rieg
    • 2
  • Sébastien Tixeuil
    • 4
    • 5
  • Xavier Urbain
    • 3
    Email author
  1. 1.CÉDRIC, Conservatoire National des Arts et MétiersParisFrance
  2. 2.Yale UniversityNew HavenUSA
  3. 3.Université de Lyon, Université Claude Bernard Lyon 1, CNRS, LIRIS UMR 5205LyonFrance
  4. 4.UPMC Sorbonne Universités, LIP6-CNRS 7606ParisFrance
  5. 5.Institut Universitaire de FranceParisFrance
  6. 6.Université Paris-Sud, LRI, CNRS UMR 8623, Université Paris-SaclayParisFrance

Personalised recommendations