Verifying Fault-Tolerance in Probabilistic Swarm Systems


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 swarms systems. We define and interpret a variant of probabilistic linear-time temporal logic on the resulting executions, including those resulting from faulty behaviour by some of the agents in the swarm. We introduce the decision problem of parameterised fault-tolerance, which concerns determining whether a probabilistic specification holds under possibly faulty behaviour. We introduce a procedure that we implement and use to study a foraging protocol from swarm robotics, and report the experimental results obtained.

Proceedings of the 29th International Joint Conference on Artificial Intelligence and the 17th Pacific Rim International Conference on Artificial Intelligence (IJCAI-PRICAI20)