Intuitive Modelling and Formal Analysis of Collective Behaviour in Foraging Ants

We demonstrate a novel methodology that integrates intuitive modelling, simulation, and formal verification of collective behaviour in biological systems. To that end, we consider the case of a colony of foraging ants, where, for the combined effect of known biological mechanisms such as stigmergic interaction, pheromone release, and path integration, the ants will progressively work out the shortest path to move back and forth between their nest and a hypothetical food repository. Starting from an informal description in natural language, we show how to devise intuitive specifications for such scenario in a formal language. We then make use of a prototype software tool to formally assess whether such specifications would indeed replicate the expected collective behaviour of the colony as a whole.