{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T10:41:08Z","timestamp":1760784068185},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319255231"},{"type":"electronic","value":"9783319255248"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-25524-8_12","type":"book-chapter","created":{"date-parts":[[2015,10,21]],"date-time":"2015-10-21T22:57:56Z","timestamp":1445468276000},"page":"185-200","source":"Crossref","is-referenced-by-count":12,"title":["Verification of Asynchronous Mobile-Robots in Partially-Known Environments"],"prefix":"10.1007","author":[{"given":"Benjamin","family":"Aminof","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aniello","family":"Murano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sasha","family":"Rubin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,28]]},"reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-54013-4_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Aminof","year":"2014","unstructured":"Aminof, B., Jacobs, S., Khalimov, A., Rubin, S.: Parameterized model checking of token-passing systems. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 262\u2013281. Springer, Heidelberg (2014)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/978-3-662-44584-6_9","volume-title":"CONCUR 2014 \u2013 Concurrency Theory","author":"B Aminof","year":"2014","unstructured":"Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith, H.: Parameterized model checking of rendezvous systems. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 109\u2013124. Springer, Heidelberg (2014)"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-662-47666-6_30","volume-title":"Automata, Languages, and Programming","author":"B Aminof","year":"2015","unstructured":"Aminof, B., Rubin, S., Zuleger, F., Spegni, F.: Liveness of parameterized timed networks. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 375\u2013387. Springer, Heidelberg (2015)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-319-03089-0_13","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"C Auger","year":"2013","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.) SSS 2013. LNCS, vol. 8255, pp. 178\u2013190. Springer, Heidelberg (2013)"},{"key":"12_CR5","unstructured":"Bender, M.A., Slonim, D.K.: The power of team exploration: Two robots can learn unlabeled directed graphs. Technical report, MIT (1995)"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Blum, M., Hewitt, C.: Automata on a 2-dimensional tape. In: SWAT (FOCS), pp. 155\u2013160 (1967)","DOI":"10.1109\/FOCS.1967.6"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"525","DOI":"10.1007\/978-3-319-08867-9_34","volume-title":"Computer Aided Verification","author":"P \u010cerm\u00e1k","year":"2014","unstructured":"\u010cerm\u00e1k, P., Lomuscio, A., Mogavero, F., Murano, A.: MCMAS-SLK: a model checker for the verification of strategy logic specifications. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 525\u2013532. Springer, Heidelberg (2014)"},{"issue":"4","key":"12_CR8","first-page":"42","volume":"4","author":"R Cohen","year":"2008","unstructured":"Cohen, R., Fraigniaud, P., Ilcinkas, D., Korman, A., Peleg, D.: Label-guided graph exploration by a finite automaton. T. Algorithms (TALG) 4(4), 42 (2008)","journal-title":"T. Algorithms (TALG)"},{"key":"12_CR9","first-page":"179","volume":"108","author":"B Courcelle","year":"2012","unstructured":"Courcelle, B., Engelfriet, J.: Book: Graph structure and monadic second-order logic. a language-theoretic approach. Bull. EATCS 108, 179 (2012)","journal-title":"Bull. EATCS"},{"key":"12_CR10","first-page":"54","volume":"109","author":"S Das","year":"2013","unstructured":"Das, S.: Mobile agents in distributed computing: Network exploration. Bull. EATCS 109, 54\u201369 (2013)","journal-title":"Bull. EATCS"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"De Giacomo, G., Felli, P., Patrizi, F., Sardi\u00f1a, S.: Two-player game structures for generalized planning and agent composition. In: Fox, M., Poole, D., (eds.) AAAI, pp. 297\u2013302 (2010)","DOI":"10.1609\/aaai.v24i1.7597"},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Graph Transformation","author":"G Delzanno","year":"2014","unstructured":"Delzanno, G.: Parameterized verification and model checking for distributed broadcast protocols. In: Giese, H., K\u00f6nig, B. (eds.) ICGT 2014. LNCS, vol. 8571, pp. 1\u201316. Springer, Heidelberg (2014)"},{"issue":"1","key":"12_CR13","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1016\/j.jalgor.2003.10.002","volume":"51","author":"K Diks","year":"2004","unstructured":"Diks, K., Fraigniaud, P., Kranakis, E., Pelc, A.: Tree exploration with little memory. Journal of Algorithms 51(1), 38\u201363 (2004)","journal-title":"Journal of Algorithms"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Flocchini, P., Prencipe, G., Santoro, N.: Computing by mobile robotic sensors. In: Nikoletseas, S., Rolim, J.D., (eds.) Theoretical Aspects of Distributed Computing in Sensor Networks, EATCS, pp. 655\u2013693. Springer (2011)","DOI":"10.1007\/978-3-642-14849-1_21"},{"key":"12_CR15","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 (2012)","DOI":"10.2200\/S00440ED1V01Y201208DCT010"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/3-540-46632-0_10","volume-title":"Algorithms and Computations","author":"P Flocchini","year":"1999","unstructured":"Flocchini, P., Prencipe, G., Santoro, N., Widmayer, P.: Hard tasks for weak robots: the role of common knowledge in pattern formation by autonomous mobile robots. In: Aggarwal, A.K., Pandu Rangan, C. (eds.) ISAAC 1999. LNCS, vol. 1741, p. 93. Springer, Heidelberg (1999)"},{"key":"12_CR17","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1016\/j.tcs.2005.07.014","volume":"345","author":"P Fraigniaud","year":"2005","unstructured":"Fraigniaud, P., Ilcinkas, D., Peer, G., Pelc, A., Peleg, D.: Graph exploration by a finite automaton. Theoretical Computer Science 345, 331\u2013344 (2005)","journal-title":"Theoretical Computer Science"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/978-3-540-92248-3_2","volume-title":"Graph-Theoretic Concepts in Computer Science","author":"L Gasieniec","year":"2008","unstructured":"Gasieniec, L., Radzik, T.: Memory efficient anonymous graph exploration. In: Broersma, H., Erlebach, T., Friedetzky, T., Paulusma, D. (eds.) WG 2008. LNCS, vol. 5344, pp. 14\u201329. Springer, Heidelberg (2008)"},{"key":"12_CR19","unstructured":"Hu, Y., De Giacomo, G.: Generalized planning: synthesizing plans that work for multiple environments. In: Walsh, T., (ed.) IJCAI, pp. 918\u2013923. AAAI (2011)"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"928","DOI":"10.1007\/978-3-642-39799-8_66","volume-title":"Computer Aided Verification","author":"A Khalimov","year":"2013","unstructured":"Khalimov, A., Jacobs, S., Bloem, R.: PARTY parameterized synthesis of token rings. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 928\u2013933. Springer, Heidelberg (2013)"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-642-35873-9_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Khalimov","year":"2013","unstructured":"Khalimov, A., Jacobs, S., Bloem, R.: Towards efficient parameterized synthesis. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 108\u2013127. Springer, Heidelberg (2013)"},{"key":"12_CR22","unstructured":"Kouvaros, P., Lomuscio, A.: Automatic verification of parameterised multi-agent systems. In: Gini, M.L., Shehory, O., Ito, T., Jonker, C.M., (eds.) AAMAS, pp. 861\u2013868 (2013)"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Kouvaros, P., Lomuscio, A.: A counter abstraction technique for the verification of robot swarms. In: Bonet, B., Koenig, S., (eds.) AAAI, pp. 2081\u20132088 (2015)","DOI":"10.1609\/aaai.v29i1.9442"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11780823_1","volume-title":"Structural Information and Communication Complexity","author":"H-C An","year":"2006","unstructured":"An, H.-C., Krizanc, D., Rajsbaum, S.: Mobile agent rendezvous: a survey. In: Flocchini, P., Gkasieniec, L. (eds.) SIROCCO 2006. LNCS, vol. 4056, pp. 1\u20139. Springer, Heidelberg (2006)"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Kranakis, E., Krizanc, D., Rajsbaum, S.: Computing with mobile agents in distributed networks. In: Rajasekaran, S., Reif, J., (eds.) Handbook of Parallel Computing: Models, Algorithms, and Applications, CRC Computer and Information Science Series, pp. 8\u20131 \u2013 8\u201320. Chapman Hall (2007)","DOI":"10.1201\/9781420011296.ch8"},{"key":"12_CR26","unstructured":"Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann (1996)"},{"key":"12_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/978-3-319-11764-5_17","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"L Millet","year":"2014","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. (eds.) SSS 2014. LNCS, vol. 8756, pp. 237\u2013251. Springer, Heidelberg (2014)"},{"key":"12_CR28","unstructured":"Minsky, M.L.: Computation: finite and infinite machines. Prentice-Hall Inc (1967)"},{"key":"12_CR29","unstructured":"Murano, A., Sorrentino, L.: A game-based model for human-robots interaction. In: Workshop \u201cFrom Objects to Agents\u201d (WOA), CEUR Workshop Proceedings, vol. 1382, pp. 146\u2013150. CEUR-WS.org (2015)"},{"key":"12_CR30","unstructured":"Rubin, S.: Parameterised verification of autonomous mobile-agents in static but unknown environments. In: Weiss, G., Yolum, P., Bordini, R.H., Elkind, E., (eds.) AAMAS, pp. 199\u2013208 (2015)"},{"issue":"4","key":"12_CR31","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/0020-0190(88)90211-6","volume":"28","author":"I Suzuki","year":"1988","unstructured":"Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28(4), 213\u2013214 (1988)","journal-title":"Inf. Process. Lett."}],"container-title":["Lecture Notes in Computer Science","PRIMA 2015: Principles and Practice of Multi-Agent Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25524-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,15]],"date-time":"2023-08-15T14:53:47Z","timestamp":1692111227000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25524-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319255231","9783319255248"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25524-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}