Top

Theory of Computing Systems

Published in:

02-01-2018

Synchronous Gathering without Multiplicity Detection: a Certified Algorithm

Authors: Thibaut Balabonski, Amélie Delga, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain

Published in: Theory of Computing Systems | Issue 2/2019

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

previous article Self-Stabilizing Metric Graphs

next article Wait-free Solvability of Colorless Tasks in Anonymous Shared-memory Model

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Available only for authorised users

The 2016 SIROCCO Prize for Innovation in Distributed Computing was awarded to Masafumi Yamashita for this line of work.

http://pactole.lri.fr/pub/cffg2d_v86/html/Pactole.Gathering.InR.Impossibility.html.

http://coq.inria.fr.

http://pactole.lri.fr.

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)

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)

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)

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)

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)MathSciNetCrossRefMATH

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)

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)

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

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)MathSciNetCrossRefMATH

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)

13.

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

14.

Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: Certified universal gathering algorithm in \(\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)

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)

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)MathSciNetCrossRefMATH

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)

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)

23.

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

Title: Synchronous Gathering without Multiplicity Detection: a Certified Algorithm
Authors: Thibaut Balabonski
Amélie Delga
Lionel Rieg
Sébastien Tixeuil
Xavier Urbain
Publication date: 02-01-2018
Publisher: Springer US
Published in: Theory of Computing Systems / Issue 2/2019
Print ISSN: 1432-4350
Electronic ISSN: 1433-0490
DOI: https://doi.org/10.1007/s00224-017-9828-z

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 2/2019

Self-Stabilizing Byzantine Clock Synchronization with Optimal Precision

Self-Stabilizing Metric Graphs

Editor’s Note: Special Issue on Stabilization, Safety, and Security of Distributed Systems

Packet Efficient Implementation of the Omega Failure Detector

On-Line Path Computation and Function Placement in SDNs

Wait-free Solvability of Colorless Tasks in Anonymous Shared-memory Model

Premium Partner