Verification of visibility-based properties on multiple moving robots in an environment with obstacles

A multi-robot system consists of a number of autonomous robots moving within an environment to achieve a common goal. Each robot decides to move based on information obtained from various sensors and gathered data received through communicating with other robots. In order to prove the system satisfies certain properties, one can provide an analytical proof or use a verification method. This article presents a new notion to prove visibility-related properties of a multirobot system by introducing an automated verification method. Precisely, we propose a method to automatically generate a discrete state space of a given multi-robot system and verify the correctness of the desired properties by means of model-checking tools and algorithms. We construct the state space of a number of robots, each moves freely inside a bounded polygonal area with obstacles. The generated state space is then used to verify visibility properties (e.g. if the communication graph of robots is connected) by means of the construction and analysis of distributed processes model checker. Using our method, there is no need to analytically prove that the properties are preserved with every change in the motion strategy of the robots. We have implemented a tool to automatically generate the state space and verified some properties to demonstrate the applicability of our method in various environments.