{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T16:55:40Z","timestamp":1780073740241,"version":"3.54.0"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031917356","type":"print"},{"value":"9783031917363","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-91736-3_8","type":"book-chapter","created":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T22:03:49Z","timestamp":1747865029000},"page":"127-143","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Deterministic Color-Optimal Self-stabilizing Semi-synchronous Gathering: A Certified Algorithm"],"prefix":"10.1007","author":[{"given":"Fran\u00e7ois","family":"Bonnet","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Quentin","family":"Bramas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pierre","family":"Courtieu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xavier","family":"D\u00e9fago","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lionel","family":"Rieg","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"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":[[2025,5,22]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","unstructured":"Asahiro, Y., Yamashita, M.: Minimum algorithm sizes for self-stabilizing gathering and related problems of autonomous mobile robots (extended abstract). In: Dolev, S., Schieber, B. (eds.) Stabilization, Safety, and Security of Distributed Systems - SSS 2023. Lecture Notes in Computer Science, vol. 14310, pp. 312\u2013327. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-44274-2_23","DOI":"10.1007\/978-3-031-44274-2_23"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-030-31277-0_7","volume-title":"Networked Systems","author":"T Balabonski","year":"2019","unstructured":"Balabonski, T., Courtieu, P., Pelle, R., Rieg, L., Tixeuil, S., Urbain, X.: Continuous vs. discrete asynchronous moves: a certified approach for mobile robots. In: Atig, M.F., Schwarzmann, A.A. (eds.) NETYS 2019. LNCS, vol. 11704, pp. 93\u2013109. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31277-0_7"},{"issue":"2","key":"8_CR3","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/S00224-017-9828-Z","volume":"63","author":"T Balabonski","year":"2019","unstructured":"Balabonski, T., Delga, A., Rieg, L., Tixeuil, S., Urbain, X.: Synchronous gathering without multiplicity detection: a certified algorithm. Theory Comput. Syst. 63(2), 200\u2013218 (2019). https:\/\/doi.org\/10.1007\/S00224-017-9828-Z","journal-title":"Theory Comput. Syst."},{"key":"8_CR4","unstructured":"Bauer, A.: How to review formalized mathematics. Blog post (2013). http:\/\/math.andrej.com\/2013\/08\/19\/how-to-review-formalized-mathematics\/"},{"issue":"6","key":"8_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. Distributed Comput. 29(6), 459\u2013487 (2016). https:\/\/doi.org\/10.1007\/S00446-016-0271-1","journal-title":"Distributed Comput."},{"key":"8_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). http:\/\/www.labri.fr\/publications\/l3a\/2004\/BC04","DOI":"10.1007\/978-3-662-07964-5"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-319-25258-2_22","volume-title":"Structural Information and Communication Complexity","author":"Q Bramas","year":"2015","unstructured":"Bramas, Q., Tixeuil, S.: Wait-free gathering without chirality. In: Scheideler, C. (ed.) SIROCCO 2014. LNCS, vol. 9439, pp. 313\u2013327. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25258-2_22"},{"issue":"4","key":"8_CR8","doi-asserted-by":"publisher","first-page":"829","DOI":"10.1137\/100796534","volume":"41","author":"M Cieliebak","year":"2012","unstructured":"Cieliebak, M., Flocchini, P., Prencipe, G., Santoro, N.: Distributed computing by mobile robots: gathering. SIAM J. Comput. 41(4), 829\u2013879 (2012). https:\/\/doi.org\/10.1137\/100796534","journal-title":"SIAM J. Comput."},{"issue":"3","key":"8_CR9","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(3), 447\u2013452 (2015). https:\/\/doi.org\/10.1016\/J.IPL.2014.11.001","journal-title":"Inf. Process. Lett."},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-662-53426-7_14","volume-title":"Distributed Computing","author":"P Courtieu","year":"2016","unstructured":"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\u2013200. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53426-7_14"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: Swarms of mobile robots: towards versatility with safety. Leibniz Trans. Embed. Syst. 8(2), 02:1\u201302:36 (2022). https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LITES.8.2.2. https:\/\/doi.org\/10.4230\/LITES.8.2.2","DOI":"10.4230\/LITES.8.2.2"},{"key":"8_CR12","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/J.TCS.2015.09.018","volume":"609","author":"S Das","year":"2016","unstructured":"Das, S., Flocchini, P., Prencipe, G., Santoro, N., Yamashita, M.: Autonomous mobile robots with lights. Theor. Comput. Sci. 609, 171\u2013184 (2016). https:\/\/doi.org\/10.1016\/J.TCS.2015.09.018","journal-title":"Theor. Comput. Sci."},{"key":"8_CR13","doi-asserted-by":"publisher","DOI":"10.1016\/J.ROBOT.2023.104378","volume":"163","author":"X D\u00e9fago","year":"2023","unstructured":"D\u00e9fago, X., Heriban, A., Tixeuil, S., Wada, K.: Using model checking to formally verify rendezvous algorithms for robots with lights in euclidean space. Robotics Auton. Syst. 163, 104378 (2023). https:\/\/doi.org\/10.1016\/J.ROBOT.2023.104378","journal-title":"Robotics Auton. Syst."},{"issue":"5","key":"8_CR14","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/S00446-019-00359-X","volume":"33","author":"X D\u00e9fago","year":"2020","unstructured":"D\u00e9fago, X., Potop-Butucaru, M., Parv\u00e9dy, P.R.: Self-stabilizing gathering of mobile robots under crash or byzantine faults. Distrib. Comput. 33(5), 393\u2013421 (2020). https:\/\/doi.org\/10.1007\/S00446-019-00359-X","journal-title":"Distrib. Comput."},{"key":"8_CR15","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/J.TCS.2011.12.010","volume":"428","author":"Y Dieudonn\u00e9","year":"2012","unstructured":"Dieudonn\u00e9, Y., Petit, F.: Self-stabilizing gathering with strong multiplicity detection. Theor. Comput. Sci. 428, 47\u201357 (2012). https:\/\/doi.org\/10.1016\/J.TCS.2011.12.010","journal-title":"Theor. Comput. Sci."},{"issue":"11","key":"8_CR16","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1145\/361179.361202","volume":"17","author":"EW Dijkstra","year":"1974","unstructured":"Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17(11), 643\u2013644 (1974). https:\/\/doi.org\/10.1145\/361179.361202","journal-title":"Commun. ACM"},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Doan, H.T.T., Bonnet, F., Ogata, K.: Model checking of robot gathering. In: Aspnes, J., Bessani, A., Felber, P., Leit\u00e3o, J. (eds.) 21st International Conference on Principles of Distributed Systems, OPODIS 2017, Lisbon, Portugal, 18\u201320 December 2017. LIPIcs, vol.\u00a095, pp. 12:1\u201312:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017). https:\/\/doi.org\/10.4230\/LIPICS.OPODIS.2017.12","DOI":"10.4230\/LIPICS.OPODIS.2017.12"},{"key":"8_CR18","doi-asserted-by":"publisher","unstructured":"Flocchini, P.: Gathering. In: Flocchini, P., Prencipe, G., Santoro, N. (eds.) Distributed Computing by Mobile Entities, Current Research in Moving and Computing. Lecture Notes in Computer Science, vol. 11340, pp. 63\u201382. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-11072-7_4","DOI":"10.1007\/978-3-030-11072-7_4"},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"Nakajima, K., Takase, K., Wada, K.: Efficient self-stabilizing simulations of energy-restricted mobile robots by asynchronous luminous mobile robots. In: Emek, Y. (ed.) Structural Information and Communication Complexity - SIROCCO 2024. Lecture Notes in Computer Science, vol. 14662, pp. 494\u2013500. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-60603-8_28","DOI":"10.1007\/978-3-031-60603-8_28"},{"key":"8_CR20","unstructured":"Pierce, B.C., et al.: Logical Foundations. Software Foundations series, volume 1. Electronic textbook (2025). https:\/\/softwarefoundations.cis.upenn.edu\/lf-current\/index.html"},{"issue":"2\u20133","key":"8_CR21","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\u20133), 222\u2013231 (2007). https:\/\/doi.org\/10.1016\/J.TCS.2007.04.023","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"8_CR22","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/S10703-019-00335-Y","volume":"56","author":"A Sangnier","year":"2020","unstructured":"Sangnier, A., Sznajder, N., Potop-Butucaru, M., Tixeuil, S.: Parameterized verification of algorithms for oblivious robots on a ring. Formal Methods Syst. Des. 56(1), 55\u201389 (2020). https:\/\/doi.org\/10.1007\/S10703-019-00335-Y","journal-title":"Formal Methods Syst. Des."},{"issue":"4","key":"8_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). https:\/\/doi.org\/10.1137\/S009753979628292X","journal-title":"SIAM J. Comput."},{"key":"8_CR24","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/j.tcs.2022.11.018","volume":"941","author":"S Terai","year":"2023","unstructured":"Terai, S., Wada, K., Katayama, Y.: Gathering problems for autonomous mobile robots with lights. Theor. Comput. Sci. 941, 241\u2013261 (2023). https:\/\/doi.org\/10.1016\/j.tcs.2022.11.018","journal-title":"Theor. Comput. Sci."},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-642-45346-5_21","volume-title":"Algorithms for Sensor Systems","author":"G Viglietta","year":"2014","unstructured":"Viglietta, G.: Rendezvous of two robots with visible bits. In: Flocchini, P., Gao, J., Kranakis, E., Meyer auf der Heide, F. (eds.) ALGOSENSORS 2013. LNCS, vol. 8243, pp. 291\u2013306. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-45346-5_21"}],"container-title":["Lecture Notes in Computer Science","Structural Information and Communication Complexity"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-91736-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T22:03:53Z","timestamp":1747865033000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-91736-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031917356","9783031917363"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-91736-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"22 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SIROCCO","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Structural Information and Communication Complexity","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Delphi","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 June 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 June 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sirocco2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.torontomu.ca\/sirocco-2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}