Asset Details
Do you wish to reserve the book?
Bridging higher-order logic and efficient computations for a rigorous analysis of idealised pathfinding ants
Hey, we have placed the reservation for you!
By the way, why not check out events that you can attend while you pick your title.
Oops! Something went wrong.
Looks like we were not able to place the reservation. Kindly try again later.
Are you sure you want to remove the book from the shelf?
Bridging higher-order logic and efficient computations for a rigorous analysis of idealised pathfinding ants
Do you wish to request the book?
Bridging higher-order logic and efficient computations for a rigorous analysis of idealised pathfinding ants
Please be aware that the book you have requested cannot be checked out. If you would like to checkout this book, you can reserve another copy
We have requested the book for you!
Your request is successful and it will be processed during the Library working hours. Please check the status of your request in My Requests.
Oops! Something went wrong.
Looks like we were not able to place your request. Kindly try again later.
Journal Article
Bridging higher-order logic and efficient computations for a rigorous analysis of idealised pathfinding ants
2025
Overview
We present a novel approach to modelling and verifying ant colony pathfinding behaviour in an idealised scenario mirroring the double bridge experiment from biological research. We implement our analysis framework in the HOL Light proof assistant to provide rigorous verification of emergent collective dynamics. Unlike most of the existing approaches, which are limited by state explosion or fixed-size constraints, we formally prove that an ant colony of
any size
converges on the optimal path, given specified preconditions. This establishes that the selection of a shortest path is a stable, emergent property
independent of the colony’s population
. To enhance the computational performance of the analysis on colonies of a given size, we implement a faithful translation between HOL Light and SMT-LIB2. This bridge allows proof obligations to be discharged efficiently by modern SAT solvers, thereby integrating the expressive power of higher-order logic with the speed of automated reasoning tools, and creating a division of labour between formal verification and dynamic simulation. Our work advances the application of computerised mathematics to collective adaptive systems, providing a unified framework for modelling, simulation, and formal verification.
Publisher
Springer Berlin Heidelberg,Springer Nature B.V
