article

Synchronous Gathering without Multiplicity Detection: a Certified Algorithm

Authors:

Thibaut Balabonski,

Sébastien Tixeuil,

Xavier UrbainAuthors Info & Claims

Theory of Computing Systems, Volume 63, Issue 2

Pages 200 - 218

https://doi.org/10.1007/s00224-017-9828-z

Published: 01 February 2019 Publication History

Abstract

In mobile robotic swarms, the gathering problem consists in coordinating all the robots so that in finite time they occupy the same location, not known beforehand. Multiplicity detection refers to the ability to detect that more than one robot can occupy a given position. When the robotic swarm operates synchronously, a well-known result by Cohen and Peleg permits to achieve gathering, provided robots are capable of multiplicity detection. We present a new algorithm for synchronous gathering, that does not assume that robots are capable of multiplicity detection, nor make any other extra assumption. Unlike previous approaches, the correctness of our proof is certified in the model where the protocol is defined, using the Coq proof assistant.

References

[1]

Altisen, K., Corbineau, P., Devismes, S.: A framework for certified self-stabilization. In: Albert, E, Lanese, I (eds.) Formal Techniques for Distributed Objects, Components, and Systems - 36th IFIP WG 6.1 International Conference, FORTE 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June 6-9, 2016, Proceedings, volume 9688 of Lecture Notes in Computer Science, pp. 36---51. Springer (2016)

Digital Library

[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.) Stabilization, Safety, and Security of Distributed Systems - 15th International Symposium (SSS 2013), volume 8255 of Lecture Notes in Computer Science, pp. 178---186. Springer, Osaka (2013)

[3]

Balabonski, T., Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: 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 - Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems - and - 17th International Workshop on Automated Verification of Critical Systems, (FMICS-AVoCS 2017), volume 10471 of Lecture Notes in Computer Science, pp. 165---181. Springer, Turin (2017)

[4]

Balabonski, T., Pelle, R., Rieg, L., Tixeuil, S.: A foundational framework for certified impossibility results with mobile robots on graphs. In: Proceedings of International Conference on Distributed Computing and Networking. Varanasi (2018)

Digital Library

[5]

Bérard, B., Lafourcade, P., Millet, L., Potop-Butucaru, M., Thierry-Mieg, Y., Tixeuil, S.: Formal verification of mobile robot protocols. Distrib. Comput. 29(6), 459---487 (2016)

Digital Library

[6]

Bertot, Y., Castéran, P.: Interactive theorem proving and program development. Coq'Art: The calculus of inductive constructions. Texts in Theoretical Computer Science. Springer (2004)

Digital Library

[7]

Bonnet, F., Dă?fago, X., Petit, F., Potop-Butucaru, M., Tixeuil, S.: Discovering and assessing fine-grained metrics in robot networks protocols. In: 33rd IEEE International Symposium on Reliable Distributed Systems Workshops, SRDS Workshops 2014, pp. 50---59. IEEE, Nara (2014)

Digital Library

[8]

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. Inf. Soc. 7(3), 101---114 (2015). Invited Paper

[9]

Castă?ran, P., Filou, V.: Tasks, types and tactics for local computation systems. Studia Informatica Universalis 9(1), 39---86 (2011)

[10]

Cohen, R., Peleg, D.: Robot convergence via center-of-gravity algorithms. In: Kralovic, R, S?kora, O (eds.) Structural Information and Communication Complexity - 11th International Colloquium (SIROCCO 2004), volume 3104 of Lecture Notes in Computer Science, pp. 79---88. Springer, Smolenice Castle (2004)

[11]

Cohen, R., Peleg, D.: Convergence properties of the gravitational algorithm in asynchronous robot systems. SIAM J. Comput. 34(6), 1516---1528 (2005)

Digital Library

[12]

Coquand, T., Paulin-Mohring, C.: Inductively defined types. In: Martin-Löf, P, Mints, G (eds.) International Conference on Computer Logic (Colog'88), volume 417 of Lecture Notes in Computer Science, pp. 50---66. Springer (1990)

Digital Library

[13]

Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: Impossibility of gathering, a certification. Inf. Process. Lett. 115, 447---452 (2015)

[14]

Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: Certified universal gathering algorithm in ?2$\mathbb {R}^{2}$ for oblivious mobile robots. In: Gavoille, C, Ilcinkas, D (eds.) Distributed Computing - 30th International Symposium, (DISC 2016), volume 9888 of Lecture Notes in Computer Science. Springer, Paris (2016)

[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.) Stabilization, Safety, and Security of Distributed Systems - 14th International Symposium (SSS 2012), volume 7596 of Lecture Notes in Computer Science, pp. 64---76. Springer, Toronto (2012)

Digital Library

[16]

Doan, HTT., Bonnet, F., Ogata, K.: Model checking of robot gathering. In: Aspnes, J., Felber, P. (eds.) Principles of Distributed Systems - 21th International Conference (OPODIS 2017), Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl---Leibniz-Zentrum fuer Informatik, Lisbon (2017)

[17]

Flocchini, P., Prencipe, G., Santoro, N.: Distributed Computing by Oblivious Mobile Robots. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers (2012)

Digital Library

[18]

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.K. (eds.) Stabilization, Safety, and Security of Distributed Systems - 16th International Symposium, (SSS 2014), volume 8756 of Lecture Notes in Computer Science, pp. 237---251. Springer, Paderborn (2014)

[19]

Prencipe, G.: Impossibility of gathering by a set of autonomous mobile robots. Theor. Comput. Sci. 384(2-3), 222---231 (2007)

Digital Library

[20]

Rubin, S., Zuleger, F., Murano, A., Aminof, B.: Verification of asynchronous mobile-robots in partially-known environments. In: Chen, Q., Torroni, P., Villata, S., Hsu, J.Y.-j., Omicini, A. (eds.) PRIMA 2015: Principles and Practice of Multi-Agent Systems - 18th International Conference, Bertinoro, Italy, October 26-30, 2015, Proceedings, volume 9387 of Lecture Notes in Computer Science, pp. 185---200. Springer (2015)

[21]

Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press (2012)

Digital Library

[22]

Sangnier, A., Sznajder, N., Potop-Butucaru, M., Tixeuil, S.: Parameterized verification of algorithms for oblivious robots on a ring. In: Formal Methods in Computer Aided Design. Vienna (2017)

Digital Library

[23]

Suzuki, I., Yamashita, M.: Distributed Anonymous Mobile Robots: Formation of Geometric Patterns. SIAM J. Comput. 28(4), 1347---1363 (1999)

Digital Library

Cited By

Balabonski TCourtieu PPelle RRieg LTixeuil SUrbain X(2021)Computer Aided Formal Design of Swarm Robotics AlgorithmsStabilization, Safety, and Security of Distributed Systems10.1007/978-3-030-91081-5_31(469-473)Online publication date: 17-Nov-2021
https://dl.acm.org/doi/10.1007/978-3-030-91081-5_31
Bramas QLamani ATixeuil S(2021)Stand up Indulgent GatheringAlgorithms for Sensor Systems10.1007/978-3-030-89240-1_2(17-28)Online publication date: 9-Sep-2021
https://dl.acm.org/doi/10.1007/978-3-030-89240-1_2
Bramas QLamani ATixeuil S(2020)Stand Up Indulgent RendezvousStabilization, Safety, and Security of Distributed Systems10.1007/978-3-030-64348-5_4(45-59)Online publication date: 18-Nov-2020
https://dl.acm.org/doi/10.1007/978-3-030-64348-5_4
Show More Cited By

Synchronous Gathering without Multiplicity Detection: a Certified Algorithm

Recommendations

Fault-Tolerant Gathering of Mobile Robots with Weak Multiplicity Detection
ICDCN '17: Proceedings of the 18th International Conference on Distributed Computing and Networking

There has been a wide interest in designing distributed algorithms for tiny robots. In particular, it has been shown that the robots can complete certain tasks even in the presence of faulty robots. In this paper, we focus on gathering of all non-faulty ...
Stand up indulgent gathering
Abstract
We consider a swarm of mobile robots evolving in a bidimensional Euclidean space. We study a variant of the crash-tolerant gathering problem: if no robot crashes, robots have to meet at the same arbitrary location, not known beforehand,...
Fault-tolerant Gathering of Semi-synchronous Robots
ICDCN '17: Proceedings of the 18th International Conference on Distributed Computing and Networking

This paper addresses the Gathering problem which asks robots to gather at a single point which is not fixed in advance, for a set of small, autonomous, mobile robots. The problem is studied for a set of semi-synchronous robots under SSY NC model when ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Theory of Computing Systems

Theory of Computing Systems Volume 63, Issue 2

February 2019

191 pages

ISSN:1432-4350

Issue’s Table of Contents

Copyright © Copyright © 2019 Springer Science+Business Media, LLC, part of Springer Nature.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 February 2019

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Balabonski TCourtieu PPelle RRieg LTixeuil SUrbain X(2021)Computer Aided Formal Design of Swarm Robotics AlgorithmsStabilization, Safety, and Security of Distributed Systems10.1007/978-3-030-91081-5_31(469-473)Online publication date: 17-Nov-2021
https://dl.acm.org/doi/10.1007/978-3-030-91081-5_31
Bramas QLamani ATixeuil S(2021)Stand up Indulgent GatheringAlgorithms for Sensor Systems10.1007/978-3-030-89240-1_2(17-28)Online publication date: 9-Sep-2021
https://dl.acm.org/doi/10.1007/978-3-030-89240-1_2
Bramas QLamani ATixeuil S(2020)Stand Up Indulgent RendezvousStabilization, Safety, and Security of Distributed Systems10.1007/978-3-030-64348-5_4(45-59)Online publication date: 18-Nov-2020
https://dl.acm.org/doi/10.1007/978-3-030-64348-5_4
Shibata MTixeuil S(2020)Partial Gathering of Mobile Robots from Multiplicity-Allowed Configurations in RingsStabilization, Safety, and Security of Distributed Systems10.1007/978-3-030-64348-5_21(264-279)Online publication date: 18-Nov-2020
https://dl.acm.org/doi/10.1007/978-3-030-64348-5_21

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents