{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T17:05:57Z","timestamp":1780074357668,"version":"3.54.0"},"publisher-location":"Cham","reference-count":11,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319577074","type":"print"},{"value":"9783319577081","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-57708-1_12","type":"book-chapter","created":{"date-parts":[[2017,4,20]],"date-time":"2017-04-20T12:03:37Z","timestamp":1492689817000},"page":"201-219","source":"Crossref","is-referenced-by-count":13,"title":["Model Checking of a Mobile Robots Perpetual Exploration Algorithm"],"prefix":"10.1007","author":[{"given":"Ha Thi Thu","family":"Doan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fran\u00e7ois","family":"Bonnet","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,4,21]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1016\/j.scico.2014.02.006","volume":"99","author":"K Bae","year":"2015","unstructured":"Bae, K., Meseguer, J.: Model checking linear temporal logic of rewriting formulas under localized fairness. Sci. Comput. Program. 99, 193\u2013234 (2015)","journal-title":"Sci. Comput. Program."},{"key":"12_CR2","doi-asserted-by":"publisher","first-page":"1","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, 1\u201329 (2016). (to appear, published online)","journal-title":"Distrib. Comput."},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-642-15763-9_29","volume-title":"Distributed Computing","author":"L Blin","year":"2010","unstructured":"Blin, L., Milani, A., Potop-Butucaru, M., Tixeuil, S.: Exclusive perpetual ring exploration without chirality. In: Lynch, N.A., Shvartsman, A.A. (eds.) DISC 2010. LNCS, vol. 6343, pp. 312\u2013327. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15763-9_29"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-319-40509-4_22","volume-title":"Ad-hoc, Mobile, and Wireless Networks","author":"F Bonnet","year":"2016","unstructured":"Bonnet, F., Potop-Butucaru, M., Tixeuil, S.: Asynchronous gathering in rings with 4 robots. In: Mitton, N., Loscri, V., Mouradian, A. (eds.) ADHOC-NOW 2016. LNCS, vol. 9724, pp. 311\u2013324. Springer, Cham (2016). doi: 10.1007\/978-3-319-40509-4_22"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)"},{"issue":"4","key":"12_CR6","doi-asserted-by":"publisher","first-page":"1055","DOI":"10.1007\/s00453-014-9892-6","volume":"72","author":"G D\u2019Angelo","year":"2015","unstructured":"D\u2019Angelo, G., Di Stefano, G., Navarra, A., Nisse, N., Suchan, K.: Computing on rings by oblivious robots: a unified approach for different tasks. Algorithmica 72(4), 1055\u20131096 (2015)","journal-title":"Algorithmica"},{"key":"12_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-02008-7","volume-title":"Distributed Computing by Oblivious Mobile Robots","author":"P Flocchini","year":"2012","unstructured":"Flocchini, P., Prencipe, G., Santoro, N.: Distributed Computing by Oblivious Mobile Robots. Morgan & Claypool Publishers, San Rafael (2012)"},{"key":"12_CR8","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science: Modelling and Reasoning about Systems","author":"M Huth","year":"2004","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, Cambridge (2004)"},{"issue":"2","key":"12_CR9","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/s00446-014-0226-3","volume":"28","author":"A Kawamura","year":"2015","unstructured":"Kawamura, A., Kobayashi, Y.: Fence patrolling by mobile agents with distinct speeds. Distrib. Comput. 28(2), 147\u2013154 (2015)","journal-title":"Distrib. Comput."},{"issue":"4","key":"12_CR10","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."},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-662-48653-5_7","volume-title":"Distributed Computing","author":"Y Yamauchi","year":"2015","unstructured":"Yamauchi, Y., Uehara, T., Kijima, S., Yamashita, M.: Plane formation by synchronous mobile robots in the three dimensional Euclidean space. In: Moses, Y. (ed.) DISC 2015. LNCS, vol. 9363, pp. 93\u2013106. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-48653-5_7"}],"container-title":["Lecture Notes in Computer Science","Structured Object-Oriented Formal Language and Method"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-57708-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,27]],"date-time":"2022-07-27T18:36:37Z","timestamp":1658946997000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-57708-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319577074","9783319577081"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-57708-1_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}