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.

Verification of asynchronous mobile-robots in partially-known environments (Best Paper Award) / Rubin, Sasha; Florian, Zuleger; Murano, Aniello; Benjamin, Aminof. - 9387:(2015), pp. 185-200. (Intervento presentato al convegno 18th International Conference on Principles and Practice of Multi-Agent Systems, PRIMA 2015 tenutosi a Bertinoro, Italia nel Ottobre 26–30, 2015) [10.1007/978-3-319-25524-8_12].

Verification of asynchronous mobile-robots in partially-known environments (Best Paper Award)

Sasha Rubin
Membro del Collaboration Group
;
Murano Aniello
Membro del Collaboration Group
;
2015

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.
2015
978-3-319-25523-1
Verification of asynchronous mobile-robots in partially-known environments (Best Paper Award) / Rubin, Sasha; Florian, Zuleger; Murano, Aniello; Benjamin, Aminof. - 9387:(2015), pp. 185-200. (Intervento presentato al convegno 18th International Conference on Principles and Practice of Multi-Agent Systems, PRIMA 2015 tenutosi a Bertinoro, Italia nel Ottobre 26–30, 2015) [10.1007/978-3-319-25524-8_12].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11588/618924
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 55
  • ???jsp.display-item.citation.isi??? 24
social impact