{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T16:54:51Z","timestamp":1780073691489,"version":"3.54.0"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2018,1,2]],"date-time":"2018-01-02T00:00:00Z","timestamp":1514851200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2019,2]]},"DOI":"10.1007\/s00224-017-9828-z","type":"journal-article","created":{"date-parts":[[2018,1,2]],"date-time":"2018-01-02T05:58:58Z","timestamp":1514872738000},"page":"200-218","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Synchronous Gathering without Multiplicity Detection: a Certified Algorithm"],"prefix":"10.1007","volume":"63","author":[{"given":"Thibaut","family":"Balabonski","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Am\u00e9lie","family":"Delga","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lionel","family":"Rieg","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0948-7172","authenticated-orcid":false,"given":"S\u00e9bastien","family":"Tixeuil","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xavier","family":"Urbain","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,1,2]]},"reference":[{"key":"9828_CR1","doi-asserted-by":"crossref","unstructured":"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\u201351. Springer (2016)","DOI":"10.1007\/978-3-319-39570-8_3"},{"key":"9828_CR2","doi-asserted-by":"crossref","unstructured":"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\u2013186. Springer, Osaka (2013)","DOI":"10.1007\/978-3-319-03089-0_13"},{"key":"9828_CR3","doi-asserted-by":"crossref","unstructured":"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\u2013181. Springer, Turin (2017)","DOI":"10.1007\/978-3-319-67113-0_15"},{"key":"9828_CR4","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1145\/3154273.3154321"},{"issue":"6","key":"9828_CR5","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/s00446-016-0271-1","volume":"29","author":"B B\u00e9rard","year":"2016","unstructured":"B\u00e9rard, B., Lafourcade, P., Millet, L., Potop-Butucaru, M., Thierry-Mieg, Y., Tixeuil, S.: Formal verification of mobile robot protocols. Distrib. Comput. 29(6), 459\u2013487 (2016)","journal-title":"Distrib. Comput."},{"key":"9828_CR6","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development. Coq\u2019Art: The calculus of inductive constructions. Texts in Theoretical Computer Science. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"9828_CR7","doi-asserted-by":"crossref","unstructured":"Bonnet, F., D\u0117fago, 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\u201359. IEEE, Nara (2014)","DOI":"10.1109\/SRDSW.2014.34"},{"issue":"3","key":"9828_CR8","first-page":"101","volume":"7","author":"B B\u00e9rard","year":"2015","unstructured":"B\u00e9rard, 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\u2013114 (2015). Invited Paper","journal-title":"Int. J. Inf. Soc."},{"issue":"1","key":"9828_CR9","first-page":"39","volume":"9","author":"P Cast\u0117ran","year":"2011","unstructured":"Cast\u0117ran, P., Filou, V.: Tasks, types and tactics for local computation systems. Studia Informatica Universalis 9(1), 39\u201386 (2011)","journal-title":"Studia Informatica Universalis"},{"key":"9828_CR10","doi-asserted-by":"crossref","unstructured":"Cohen, R., Peleg, D.: Robot convergence via center-of-gravity algorithms. In: Kralovic, R, S\u00fdkora, O (eds.) Structural Information and Communication Complexity - 11th International Colloquium (SIROCCO 2004), volume 3104 of Lecture Notes in Computer Science, pp. 79\u201388. Springer, Smolenice Castle (2004)","DOI":"10.1007\/978-3-540-27796-5_8"},{"issue":"6","key":"9828_CR11","doi-asserted-by":"publisher","first-page":"1516","DOI":"10.1137\/S0097539704446475","volume":"34","author":"R Cohen","year":"2005","unstructured":"Cohen, R., Peleg, D.: Convergence properties of the gravitational algorithm in asynchronous robot systems. SIAM J. Comput. 34(6), 1516\u20131528 (2005)","journal-title":"SIAM J. Comput."},{"key":"9828_CR12","doi-asserted-by":"crossref","unstructured":"Coquand, T., Paulin-Mohring, C.: Inductively defined types. In: Martin-L\u00f6f, P, Mints, G (eds.) International Conference on Computer Logic (Colog\u201988), volume 417 of Lecture Notes in Computer Science, pp. 50\u201366. Springer (1990)","DOI":"10.1007\/3-540-52335-9_47"},{"key":"9828_CR13","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1016\/j.ipl.2014.11.001","volume":"115","author":"P Courtieu","year":"2015","unstructured":"Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: Impossibility of gathering, a certification. Inf. Process. Lett. 115, 447\u2013452 (2015)","journal-title":"Inf. Process. Lett."},{"key":"9828_CR14","doi-asserted-by":"crossref","unstructured":"Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: Certified universal gathering algorithm in \u211d 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)","DOI":"10.1007\/978-3-662-53426-7_14"},{"key":"9828_CR15","doi-asserted-by":"crossref","unstructured":"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\u201376. Springer, Toronto (2012)","DOI":"10.1007\/978-3-642-33536-5_7"},{"key":"9828_CR16","unstructured":"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\u2013Leibniz-Zentrum fuer Informatik, Lisbon (2017)"},{"key":"9828_CR17","doi-asserted-by":"crossref","unstructured":"Flocchini, P., Prencipe, G., Santoro, N.: Distributed Computing by Oblivious Mobile Robots. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers (2012)","DOI":"10.2200\/S00440ED1V01Y201208DCT010"},{"key":"9828_CR18","doi-asserted-by":"crossref","unstructured":"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\u2013251. Springer, Paderborn (2014)","DOI":"10.1007\/978-3-319-11764-5_17"},{"issue":"2-3","key":"9828_CR19","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1016\/j.tcs.2007.04.023","volume":"384","author":"G Prencipe","year":"2007","unstructured":"Prencipe, G.: Impossibility of gathering by a set of autonomous mobile robots. Theor. Comput. Sci. 384(2-3), 222\u2013231 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"9828_CR20","doi-asserted-by":"crossref","unstructured":"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\u2013200. Springer (2015)","DOI":"10.1007\/978-3-319-25524-8_12"},{"key":"9828_CR21","doi-asserted-by":"crossref","unstructured":"Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press (2012)","DOI":"10.1017\/CBO9780511777110"},{"key":"9828_CR22","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.23919\/FMCAD.2017.8102262"},{"issue":"4","key":"9828_CR23","doi-asserted-by":"publisher","first-page":"1347","DOI":"10.1137\/S009753979628292X","volume":"28","author":"I Suzuki","year":"1999","unstructured":"Suzuki, I., Yamashita, M.: Distributed Anonymous Mobile Robots: Formation of Geometric Patterns. SIAM J. Comput. 28(4), 1347\u20131363 (1999)","journal-title":"SIAM J. Comput."}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-017-9828-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00224-017-9828-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-017-9828-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,11]],"date-time":"2022-08-11T17:17:51Z","timestamp":1660238271000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00224-017-9828-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,2]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,2]]}},"alternative-id":["9828"],"URL":"https:\/\/doi.org\/10.1007\/s00224-017-9828-z","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"value":"1432-4350","type":"print"},{"value":"1433-0490","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,1,2]]},"assertion":[{"value":"2 January 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}