Specification and Verification of the Alpha Swarm Algorithm using NuXMV and GROOVE

摘要

Swarm robotic systems consist of numerous simple robots coordinating in a decentralised manner to achieve a common goal. Ensuring that individual robot behaviours lead to the desired swarm-level outcomes is challenging due to the lack of a central controller. This article uses two frameworks to facilitate formal specification and verification of robot swarms: (1) NuXMV, which models the system as a Finite State Machine, specifies properties using temporal logic, and verifies them through model checking with BDDs and SMT-solvers; and (2) GROOVE, which models the system as a Graph Grammar, specifies properties using temporal logic with graphical states, and verifies them via graph-specific model checking algorithms. We compare these formal approaches by modelling the Alpha swarm aggregation algorithm, which ensures that any robot disconnected from the swarm, capable only of short-range wireless communications, will eventually return to it. We find that GROOVE effectively leverages symmetry to reduce the state space, while NuXMV excels in handling models requiring extensive calculations and data manipulations not optimally expressed through graphs. We discuss the suitability of each approach for different systems and properties, suggesting future directions that combine the strengths of both approaches.