Automatic Verification of Multi-Agent Systems in Parameterised Grid-Environments

We present a framework for modeling and analysing multiple mobile agents on grid-environments such as finite mazes and labyrinths. Agents are modeled as automata, and the grid-environments are parameterised by their size and the relative positions of the obstacles. We study the verification problem, i.e., whether given agents complete a given task on a given (possibly infinite) set of grid-environments. We identify restrictions on the agents and on the environments for which the verification problem is decidable (and in pspace). These assumptions are: i) there are a bounded number of obstacles, and ii) the agents are not allowed to issue commands like "increase my x-coordinate by 1" but can only issue commands that change their relative positions, e.g., "increase my x-coordinate until I go past this wall". We prove pspace-hardness already for the verification problem of a single agent on singleton parameterised environments with no obstacles. It is therefore remarkable that the pspace-upper bound also holds for the verification problem with multiple agents, parameterised environments and multiple obstacles. We prove that weakening either of restrictions i) or ii) results in undecidability. The importance of this work is that it is the first to give a sound and complete decision procedure for the verification problem on parameterised grid-like environments. Previous work either involved only a single grid, restricted the scheduling of the agents, or excluded grids altogether.