Robot Swarms as Hybrid Systems: Modelling and Verification

TL;DR

This paper models swarm robotic systems as hybrid systems and employs reachability analysis to verify their global behaviors, addressing the challenge of ensuring reliable collective performance.

Contribution

It introduces a hybrid systems modeling approach for swarm robots and demonstrates the application of formal verification techniques to analyze their behavior.

Findings

Hybrid modeling facilitates formal verification of swarm behaviors

Reachability analysis helps identify potential failures in swarm coordination

Applying formal methods improves confidence in swarm system reliability

Abstract

A swarm robotic system consists of a team of robots performing cooperative tasks without any centralized coordination. In principle, swarms enable flexible and scalable solutions; however, designing individual control algorithms that can guarantee a required global behavior is difficult. Formal methods have been suggested by several researchers as a mean to increase confidence in the behavior of the swarm. In this work, we propose to model swarms as hybrid systems and use reachability analysis to verify their properties. We discuss challenges and report on the experience gained from applying hybrid formalisms to the verification of a swarm robotic system.