Model checking of emergent behaviour properties of robot swarms

Abstract

This paper presents a case study on scalability of explicit state model checking. Three state space reduction methods - state vector compression, bit state hashing, and symmetry reduction - were applied on an exercise with the objective of verifying a distributed coordination algorithm for robot swarms. Based on the analysis results, the feasibility of using explicit state model checking to prove properties of large multi-agent systems is questioned and the limitations faced in verifying a dynamic cleaning algorithm are outlined.