Parameterised Verification of Autonomous Mobile-Agents in Static But Unknown Environments

Automata walking on graphs are a mathematical formalisation of autonomous mobile agents with limited memory operating in discrete environments. This paper establishes a framework in which to model and automatically verify that autonomous mobile agents correctly perform their tasks. The framework consists of a logical language tailored for expressing agent tasks, and an algorithm solving the parameterised verification problem, where the graphs are treated as the parameter. We reduce the parameterised verification problem to classic questions in automata theory and monadic second order logic, i.e., universality and validity problems. We illustrate the framework by instantiating it to a popular model of robot from the distributed computing literature. This work clarifies the border between classes of mobileagent systems that have decidable parameterised verification problem, and those that do not.