Verifying Fault-Tolerance in Probabilistic Swarm Systems

Verifying Fault-Tolerance in Probabilistic Swarm Systems

Alessio Lomuscio, Edoardo Pirovano

Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence
Main track. Pages 325-331. https://doi.org/10.24963/ijcai.2020/46

We present a method for reasoning about fault-tolerance in unbounded robotic swarms. We introduce a novel semantics that accounts for the probabilistic nature of both the swarm and possible malfunctions, as well as the unbounded nature of swarm systems. We define and interpret a variant of probabilistic linear-time temporal logic on the resulting executions, including those arising from faulty behaviour by some of the agents in the swarm. We specify the decision problem of parameterised fault-tolerance, which concerns determining whether a probabilistic specification holds under possibly faulty behaviour. We outline a verification procedure that we implement and use to study a foraging protocol from swarm robotics, and report the experimental results obtained.
Keywords:
Agent-based and Multi-agent Systems: Agent Theories and Models
Agent-based and Multi-agent Systems: Formal Verification, Validation and Synthesis
Robotics: Multi-Robot Systems