Scholarlink

<p>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 <i>any size</i> converges on the optimal path, given specified preconditions. This establishes that the selection of a shortest path is a stable, emergent property <i>independent of the colony’s population</i>. 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.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Bridging higher-order logic and efficient computations for a rigorous analysis of idealised pathfinding ants

  • 期刊论文

  • 发表日期：

    2025年12月1日

查看全文
  • Cosimo Perini Brogi,
  • Marco Maggesi

摘要

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.