Paul Gainer, Clare Dixon, and Ullrich Hustadt (2016): ``Probabilistic Model Checking of Ant-Based Positionless Swarming.'' In L. Alboul, D. D. Damian, and J. M. Aitken, editors, Proceedings of the 17th Annual Conference Towards Autonomous Robotic Systems (TAROS 2016) [Sheffield, UK, 26 June-1 July 2016], pp. 127-138. LNCS 9716, Springer 2016.
Abstract, BibTeX. PDF (© Springer).

Robot swarms are collections of simple robots cooperating without centralized control. Control algorithms for swarms are often inspired by decentralised problem-solving systems found in nature. In this paper we conduct a formal analysis of an algorithm inspired by the foraging behaviour of ants, where a swarm of flying vehicles searches for a target at some unknown location. We show how both exhaustive model checking and statistical model checking can be used to check properties that complement the results obtained through simulation, resulting in information that would facilitate the logistics of swarm deployment.