Abstract
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.
This work was partially funded by the CNRS PEPS OCAAA 2017 project CYBORG and the Université Claude Bernard Lyon 1 BQR 2017 project PREFER.
The original version of this chapter was revised. The author corrections were updated. The erratum to this chapter is available at https://doi.org/10.1007/978-3-319-67113-0_15
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
- 3.
A demon is k -fair when any robot is activated within k consecutive activations of any other robot.
References
Agmon, N., Peleg, D.: Fault-tolerant gathering algorithms for autonomous mobile robots. SIAM J. Comput. 36(1), 56–82 (2006)
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
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
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)
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)
Bouzid, Z., Das, S., Tixeuil, S.: Gathering of mobile robots tolerating multiple crash faults. In: ICDCS, pp. 337–346. IEEE Computer Society (2013)
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
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
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 Paper
Cieliebak, M., Flocchini, P., Prencipe, G., Santoro, N.: Distributed computing by mobile robots: Gathering. SIAM J. Comput. 41(4), 829–879 (2012)
Cohen, R., Peleg, D.: Convergence properties of the gravitational algorithm in asynchronous robot systems. SIAM J. Comput. 34(6), 1516–1528 (2005)
Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: A certified universal gathering algorithm for oblivious mobile robots. CoRR, abs/1506.01603 (2015)
Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: Impossibility of gathering, a Certification. Inf. Process. Lett. 115, 447–452 (2015)
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
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
Dieudonné, Y., Petit, F.: Self-stabilizing gathering with strong multiplicity detection. Theoret. Comput. Sci. 428, 47–57 (2012)
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
Flocchini, P., Prencipe, G., Santoro, N.: Distributed Computing by Oblivious Mobile Robots. Synthesis lectures on distributed computing theory. Morgan & Claypool Publishers, San Rafael (2012)
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)
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
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
Prencipe, G.: Impossibility of gathering by a set of autonomous mobile robots. Theoret. Comput. Sci. 384(2–3), 222–231 (2007)
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
Suzuki, I., Yamashita, M.: Distributed anonymous mobile robots: formation of geometric patterns. SIAM J. Comput. 28(4), 1347–1363 (1999)
Yamashita, M., Suzuki, I.: Characterizing geometric patterns formable by oblivious anonymous mobile robots. Theor. Comput. Sci. 411(26–28), 2433–2453 (2010)
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
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Balabonski, T., Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X. (2017). Certified Gathering of Oblivious Mobile Robots: Survey of Recent Results and Open Problems. In: Petrucci, L., Seceleanu, C., Cavalcanti, A. (eds) Critical Systems: Formal Methods and Automated Verification. AVoCS FMICS 2017 2017. Lecture Notes in Computer Science(), vol 10471. Springer, Cham. https://doi.org/10.1007/978-3-319-67113-0_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-67113-0_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-67112-3
Online ISBN: 978-3-319-67113-0
eBook Packages: Computer ScienceComputer Science (R0)