Towards Scalable Parallel Verification of Multi-Robot Systems In ROS 2 Using Reduced Distributed State Space

Abstract

One of the persistent challenges in formally verifying distributed and concurrent systems is the combinatorial growth of the state space, a phenomenon known as the state explosion problem. The number of potential configurations for these systems increases significantly with scale and interconnection, rendering exhaustive analysis computationally costly or even infeasible. To address this problem, researchers have been resorting to modular design approaches that divide an intricate system into smaller, independently verifiable components. Based on an in-depth examination of the strengths and limitations of current works in the literature, we suggest parallelizing the construction of the Reduced Distributed State Space (RDSS), which is an abstract and condensed representation that leverages the subdivision of the system into separate modules. To this end, we propose a generalized distributed architecture that defines the roles of a central coordinator and multiple worker modules, along with their communication points for synchronizing the RDSS building. This architecture is then concretely implemented using the Robot Operating System (ROS 2) framework, which provides robust primitives such as topics and services for inter-process communication, making the distributed execution both scalable and maintainable. Our method ensures stuttering equivalence with the global system and enables the scalable verification of local LTL\X properties using each module’s metagraph, without the need to explore the full RDSS. This implementation lays the foundation for modular model checking in distributed environments. Its effectiveness is demonstrated through a cooperative patrolling case study, which serves not only to validate the correctness of the proposed algorithm but also to observe its distributed behavior through simulated executions.