Rigorous Analysis of Idealised Pathfinding Ants in Higher-Order Logic

This paper presents a modelling framework for an idealised system of foraging ants using Higher-Order Logic (HOL), which we implemented in the HOL Light proof assistant. Exploiting the expressive capabilities of HOL Light, we create a detailed, principled model that describes individual ant behaviours to explore long-term dynamics and formally verify the colony’s emergent property we are interested in, namely shortest path finding. Using HOL Light guarantees rigorous model verification and confirms the simulation accuracy. We present our results as highlights of the potential of computerised mathematics in studying collective adaptive systems. By merging formal methods with complex systems science, we aim to explore emergent behaviours in biological and artificial systems with mathematical precision and reliability.