Abstract
This paper establishes a framework based on logic and automata theory in which to model and automatically verify that multiple mobile robots, with sensing abilities, moving asynchronously, correctly perform their tasks. The motivation is from practical scenarios in which the environment is not completely know to the robots, e.g., physical robots exploring a maze, or software agents exploring a hostile network. The framework shows how to express tasks in a logical language, and exhibits an algorithm solving the parameterised verification problem, where the graphs are treated as the parameter. The main assumption that yields decidability is that the robots take a bounded number of turns. We prove that dropping this assumption results in undecidability, even for robots with very limited (“local”) sensing abilities.
Benjamin Aminof and Florian Zuleger were supported by the Austrian National Research Network S11403-N23 (RiSE) of the Austrian Science Fund (FWF) and by the Vienna Science and Technology Fund (WWTF) through grant ICT12-059. Aniello Murano was supported by FP7 EU project 600958-SHERPA. Sasha Rubin is a Marie Curie fellow of the Istituto Nazionale di Alta Matematica.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
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–281. Springer, Heidelberg (2014)
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–124. Springer, Heidelberg (2014)
Aminof, B., Rubin, S., Zuleger, F., Spegni, F.: Liveness of parameterized timed networks. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 375–387. Springer, Heidelberg (2015)
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–190. Springer, Heidelberg (2013)
Bender, M.A., Slonim, D.K.: The power of team exploration: Two robots can learn unlabeled directed graphs. Technical report, MIT (1995)
Blum, M., Hewitt, C.: Automata on a 2-dimensional tape. In: SWAT (FOCS), pp. 155–160 (1967)
Čermák, 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–532. Springer, Heidelberg (2014)
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)
Courcelle, B., Engelfriet, J.: Book: Graph structure and monadic second-order logic. a language-theoretic approach. Bull. EATCS 108, 179 (2012)
Das, S.: Mobile agents in distributed computing: Network exploration. Bull. EATCS 109, 54–69 (2013)
De Giacomo, G., Felli, P., Patrizi, F., Sardiña, S.: Two-player game structures for generalized planning and agent composition. In: Fox, M., Poole, D., (eds.) AAAI, pp. 297–302 (2010)
Delzanno, G.: Parameterized verification and model checking for distributed broadcast protocols. In: Giese, H., König, B. (eds.) ICGT 2014. LNCS, vol. 8571, pp. 1–16. Springer, Heidelberg (2014)
Diks, K., Fraigniaud, P., Kranakis, E., Pelc, A.: Tree exploration with little memory. Journal of Algorithms 51(1), 38–63 (2004)
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–693. Springer (2011)
Flocchini, P., Prencipe, G., Santoro, N.: Distributed Computing by Oblivious Mobile Robots. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool (2012)
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)
Fraigniaud, P., Ilcinkas, D., Peer, G., Pelc, A., Peleg, D.: Graph exploration by a finite automaton. Theoretical Computer Science 345, 331–344 (2005)
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–29. Springer, Heidelberg (2008)
Hu, Y., De Giacomo, G.: Generalized planning: synthesizing plans that work for multiple environments. In: Walsh, T., (ed.) IJCAI, pp. 918–923. AAAI (2011)
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–933. Springer, Heidelberg (2013)
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–127. Springer, Heidelberg (2013)
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–868 (2013)
Kouvaros, P., Lomuscio, A.: A counter abstraction technique for the verification of robot swarms. In: Bonet, B., Koenig, S., (eds.) AAAI, pp. 2081–2088 (2015)
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–9. Springer, Heidelberg (2006)
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–1 – 8–20. Chapman Hall (2007)
Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann (1996)
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–251. Springer, Heidelberg (2014)
Minsky, M.L.: Computation: finite and infinite machines. Prentice-Hall Inc (1967)
Murano, A., Sorrentino, L.: A game-based model for human-robots interaction. In: Workshop “From Objects to Agents” (WOA), CEUR Workshop Proceedings, vol. 1382, pp. 146–150. CEUR-WS.org (2015)
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–208 (2015)
Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28(4), 213–214 (1988)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Aminof, B., Murano, A., Rubin, S., Zuleger, F. (2015). Verification of Asynchronous Mobile-Robots in Partially-Known Environments. In: Chen, Q., Torroni, P., Villata, S., Hsu, J., Omicini, A. (eds) PRIMA 2015: Principles and Practice of Multi-Agent Systems. PRIMA 2015. Lecture Notes in Computer Science(), vol 9387. Springer, Cham. https://doi.org/10.1007/978-3-319-25524-8_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-25524-8_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-25523-1
Online ISBN: 978-3-319-25524-8
eBook Packages: Computer ScienceComputer Science (R0)