Synchronous gathering without multiplicity detection: a certified algorithm. (English) Zbl 1423.68522
Summary: 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.
MSC:
| 68T40 | Artificial intelligence for robotics |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 68W15 | Distributed algorithms |
Software:
CoqReferences:
| [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) · Zbl 1347.68358 |
| [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) |
| [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) · Zbl 1410.68217 · doi:10.1007/s00446-016-0271-1 |
| [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) · Zbl 1069.68095 |
| [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) |
| [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) · Zbl 1085.68697 |
| [11] | Cohen, R., Peleg, D.: Convergence properties of the gravitational algorithm in asynchronous robot systems. SIAM J. Comput. 34(6), 1516-1528 (2005) · Zbl 1081.68110 · doi:10.1137/S0097539704446475 |
| [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) · Zbl 0722.03006 |
| [13] | Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: Impossibility of gathering, a certification. Inf. Process. Lett. 115, 447-452 (2015) · Zbl 1317.68264 · doi:10.1016/j.ipl.2014.11.001 |
| [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) · Zbl 1393.68163 |
| [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) · Zbl 1487.68041 |
| [17] | Flocchini, P., Prencipe, G., Santoro, N.: Distributed Computing by Oblivious Mobile Robots. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers (2012) · Zbl 1286.68484 |
| [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) · Zbl 1125.68124 · doi:10.1016/j.tcs.2007.04.023 |
| [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) · Zbl 1252.68008 |
| [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) · Zbl 1506.68058 |
| [23] | Suzuki, I., Yamashita, M.: Distributed Anonymous Mobile Robots: Formation of Geometric Patterns. SIAM J. Comput. 28(4), 1347-1363 (1999) · Zbl 0940.68145 · doi:10.1137/S009753979628292X |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
