Verifying Fault-Tolerance in Probabilistic Swarm Systems
Abstract
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.
Cite
Text
Lomuscio and Pirovano. "Verifying Fault-Tolerance in Probabilistic Swarm Systems." International Joint Conference on Artificial Intelligence, 2020. doi:10.24963/IJCAI.2020/46Markdown
[Lomuscio and Pirovano. "Verifying Fault-Tolerance in Probabilistic Swarm Systems." International Joint Conference on Artificial Intelligence, 2020.](https://mlanthology.org/ijcai/2020/lomuscio2020ijcai-verifying/) doi:10.24963/IJCAI.2020/46BibTeX
@inproceedings{lomuscio2020ijcai-verifying,
title = {{Verifying Fault-Tolerance in Probabilistic Swarm Systems}},
author = {Lomuscio, Alessio and Pirovano, Edoardo},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2020},
pages = {325-331},
doi = {10.24963/IJCAI.2020/46},
url = {https://mlanthology.org/ijcai/2020/lomuscio2020ijcai-verifying/}
}