Rigorous Analysis of Idealised Pathfinding Ants in Higher-Order Logic

Abstract: This paper presents a modelling framework for an idealised system of foraging ants, using Higher-Order Logic (HOL) and implemented in the HOL Light proof assistant. Exploiting the expressive capabilities of HOL, we create a detailed, principled model that describes individual ant behaviours to explore long-term dynamics and formally verify the emergent property of the colony we are interested in, namely shortest path finding. Using HOL Light guarantees rigorous verification of the model, also confirming the simulation accuracy. We present our results as highlights for the potential of formal computer mathematics in studying complex 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.