{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T17:01:33Z","timestamp":1780074093689,"version":"3.54.0"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2019,7,30]],"date-time":"2019-07-30T00:00:00Z","timestamp":1564444800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,7,30]],"date-time":"2019-07-30T00:00:00Z","timestamp":1564444800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-14-CE28- 0002"],"award-info":[{"award-number":["ANR-14-CE28- 0002"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2020,12]]},"DOI":"10.1007\/s10703-019-00335-y","type":"journal-article","created":{"date-parts":[[2019,7,31]],"date-time":"2019-07-31T07:02:37Z","timestamp":1564556557000},"page":"55-89","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Parameterized verification of algorithms for oblivious robots on a ring"],"prefix":"10.1007","volume":"56","author":[{"given":"Arnaud","family":"Sangnier","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nathalie","family":"Sznajder","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Maria","family":"Potop-Butucaru","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"S\u00e9bastien","family":"Tixeuil","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,7,30]]},"reference":[{"key":"335_CR1","doi-asserted-by":"crossref","unstructured":"Auger C, Bouzid Z, Courtieu P, Tixeuil S, Urbain X (2013) Certified impossibility results for byzantine-tolerant mobile robots. In: Proceedings\u00a0of SSS\u201913, volume 8255 of LNCS. Springer, Berlin, pp 178\u2013186","DOI":"10.1007\/978-3-319-03089-0_13"},{"key":"335_CR2","doi-asserted-by":"crossref","unstructured":"Balabonski T, Delga A, Rieg L, Tixeuil S, Urbain X (2016) Synchronous gathering without multiplicity detection: a certified algorithm. In: Proceedings of SSS\u201916, volume 10083 of LNCS. Springer, Berlin, pp 7\u201319","DOI":"10.1007\/978-3-319-49259-9_2"},{"issue":"3","key":"335_CR3","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 (2015) Formal methods for mobile robots: current results and open problems. Int J Inf Soc 7(3):101\u2013114","journal-title":"Int J Inf Soc"},{"key":"335_CR4","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 (2016) Formal verification of mobile robot protocols. Distrib Comput 29:459\u2013587","journal-title":"Distrib Comput"},{"key":"335_CR5","doi-asserted-by":"crossref","unstructured":"Blin L, Milani A, Potop-Butucaru M, Tixeuil S (2010) Exclusive perpetual ring exploration without chirality. In: Proceedings\u00a0of DISC\u201910, volume 6343 of LNCS. Springer, Berlin, pp 312\u2013327","DOI":"10.1007\/978-3-642-15763-9_29"},{"key":"335_CR6","doi-asserted-by":"crossref","unstructured":"Bonnet F, D\u00e9fago X, Petit F, Potop-Butucaru M, Tixeuil S (2014) Discovering and assessing fine-grained metrics in robot networks protocols. In: Proceedings\u00a0of SRDS\u201914. IEEE Press, pp 50\u201359","DOI":"10.1109\/SRDSW.2014.34"},{"key":"335_CR7","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1090\/S0002-9939-1976-0396605-3","volume":"55","author":"I Borosh","year":"1976","unstructured":"Borosh I, Treybig L (1976) Bounds on positive integral solutions of linear Diophantine equations. Am Math Soc 55:299\u2013304","journal-title":"Am Math Soc"},{"key":"335_CR8","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 (2015) Impossibility of gathering, a certification. Inf Process Lett 115:447\u2013452","journal-title":"Inf Process Lett"},{"key":"335_CR9","doi-asserted-by":"crossref","unstructured":"Courtieu P, Rieg L, Tixeuil S, Urbain X (2016) Certified universal gathering in $$\\mathbb{R}^{2}$$ for oblivious mobile robots. In: Proceedings\u00a0of DISC\u201916, volume 9888 of LNCS. Springer, Berlin, pp 187\u2013200","DOI":"10.1007\/978-3-662-53426-7_14"},{"key":"335_CR10","doi-asserted-by":"crossref","unstructured":"D\u2019Angelo G, Stefano GD, Navarra A, Nisse N, Suchan K (2013) A unified approach for different tasks on rings in robot-based computing systems. In Proceedings of IPDPSW\u201913. IEEE Press, pp 667\u2013676","DOI":"10.1109\/IPDPSW.2013.89"},{"key":"335_CR11","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura LM, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: TACAS\u201908, volume 4963 of LNCS. Springer, Berlin, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"335_CR12","doi-asserted-by":"crossref","unstructured":"Devismes S, Lamani A, Petit F, Raymond P, Tixeuil S (2012) Optimal grid exploration by asynchronous oblivious robots. In: Proceedings\u00a0of SSS\u201912, volume 7596 of LNCS. Springer, Berlin, pp 64\u201376","DOI":"10.1007\/978-3-642-33536-5_7"},{"key":"335_CR13","unstructured":"Doan HTT, Bonnet F, Ogata K (2016) Model checking of a mobile robots perpetual exploration algorithm. In Proceedings\u00a0of SOFL+MSVL, Revised Selected Papers, volume 10189 of LNCS, pp 201\u2013219"},{"issue":"3","key":"335_CR14","doi-asserted-by":"publisher","first-page":"562","DOI":"10.1007\/s00453-011-9611-5","volume":"65","author":"P Flocchini","year":"2013","unstructured":"Flocchini P, Ilcinkas D, Pelc A, Santoro N (2013) Computing without communicating: ring exploration by asynchronous oblivious robots. Algorithmica 65(3):562\u2013583","journal-title":"Algorithmica"},{"key":"335_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-02008-7","volume-title":"Distributed computing by oblivious mobile robots. Synt. Lect. Distr. Comp. Th","author":"P Flocchini","year":"2012","unstructured":"Flocchini P, Prencipe G, Santoro N (2012) Distributed computing by oblivious mobile robots. Synt. Lect. Distr. Comp. Th. Morgan & Claypool Publishers, San Rafael"},{"key":"335_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-01999-9","volume-title":"The mobile agent rendezvous problem in the ring. Synt. Lect. Distr. Comp. Th.","author":"E Kranakis","year":"2010","unstructured":"Kranakis E, Krizanc D, Markou E (2010) The mobile agent rendezvous problem in the ring. Synt. Lect. Distr. Comp. Th. Morgan & Claypool Publishers, San Rafael"},{"issue":"1\u20133","key":"335_CR17","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/S0304-3975(02)00646-1","volume":"297","author":"R Mayr","year":"2003","unstructured":"Mayr R (2003) Undecidable problems in unreliable computations. Theor Comput Sci 297(1\u20133):337\u2013354","journal-title":"Theor Comput Sci"},{"key":"335_CR18","doi-asserted-by":"crossref","unstructured":"Millet L, Potop-Butucaru M, Sznajder N, Tixeuil S (2014) On the synthesis of mobile robots algorithms: the case of ring gathering. In: Proceedings\u00a0of SSS\u201914, volume 8756 of LNCS. Springer, Berlin, pp 237\u2013251","DOI":"10.1007\/978-3-319-11764-5_17"},{"key":"335_CR19","volume-title":"Computation: finite and infinite machines","author":"ML Minsky","year":"1967","unstructured":"Minsky ML (1967) Computation: finite and infinite machines. Prentice-Hall Inc, Upper Saddle River"},{"key":"335_CR20","unstructured":"Rubin S, Zuleger F, Murano A, Aminof B (2015) Verification of asynchronous mobile-robots in partially-known environments. In: Proceedings\u00a0of PRIMA\u201915, volume 9387 of LNCS. Springer, Berlin, pp 185\u2013200"},{"key":"335_CR21","doi-asserted-by":"crossref","unstructured":"Sangnier A, Sznajder N, Potop-Butucaru M, Tixeuil S (2017) Parameterized verification of algorithms for oblivious robots on a ring. In: FMCAD\u201917. IEEE, pp 212\u2013219","DOI":"10.23919\/FMCAD.2017.8102262"},{"key":"335_CR22","unstructured":"SMT-LIB: The satisfiability modulo theory library. http:\/\/smtlib.cs.uiowa.edu\/"},{"issue":"4","key":"335_CR23","doi-asserted-by":"publisher","first-page":"1347","DOI":"10.1137\/S009753979628292X","volume":"28","author":"I Suzuki","year":"1999","unstructured":"Suzuki I, Yamashita M (1999) Distributed anonymous mobile robots: formation of geometric patterns. SIAM J Comput 28(4):1347\u20131363","journal-title":"SIAM J Comput"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-019-00335-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-019-00335-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-019-00335-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,24]],"date-time":"2022-09-24T22:16:49Z","timestamp":1664057809000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-019-00335-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,30]]},"references-count":23,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["335"],"URL":"https:\/\/doi.org\/10.1007\/s10703-019-00335-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,30]]},"assertion":[{"value":"30 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}