Rigorous Analysis of Idealised Pathfinding Ants in Higher-Order Logic

被引：0
作者：
Maggesi, Marco [1 ]
Brogi, Cosimo Perini [2 ]
机构：
[1] Univ Florence, Florence, Italy
[2] IMT Sch Adv Studies Lucca, Lucca, Italy
来源：
LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: RIGOROUS ENGINEERING OF COLLECTIVE ADAPTIVE SYSTEMS, PT II, ISOLA 2024 | 2025年 / 15220卷
关键词：
Logical verification; Pathfinding ants; HOL Light; Emergent behaviours; Agent-based modelling; Formal methods; FORAGING STRATEGIES; OPTIMIZATION; STIGMERGY; BEHAVIOR; SYSTEMS; CHAOS;
D O I：
10.1007/978-3-031-75107-3_18
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
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.
引用
收藏
页码：297 / 315
页数：19
相关论文
共 54 条
  • [1] [Anonymous], 2014, Handbook of the History of Logic, DOI DOI 10.1016/B978-0-444-51624-4.50004-6
  • [2] Baanen A., 2024, The Hitchhiker's Guide to Logical Verification
  • [3] FORAGING STRATEGIES OF ANTS IN RESPONSE TO VARIABLE FOOD DENSITY
    BERNSTEIN, RA
    [J]. ECOLOGY, 1975, 56 (01) : 213 - 219
  • [4] Flexibility at the edge of chaos: A clear example from foraging in ants
    Bonabeau, E
    [J]. ACTA BIOTHEORETICA, 1997, 45 (01) : 29 - 50
  • [5] Self-organization in social insects
    Bonabeau, E
    Theraulaz, G
    Deneubourg, JL
    Aron, S
    Camazine, S
    [J]. TRENDS IN ECOLOGY & EVOLUTION, 1997, 12 (05) : 188 - 193
  • [6] Inspiration for optimization from social insect behaviour
    Bonabeau, E
    Dorigo, M
    Theraulaz, G
    [J]. NATURE, 2000, 406 (6791) : 39 - 42
  • [7] Chapman R., 2024, Formal Verification of Cryptographic Software at AWS: Current Practices and Future Trends
  • [8] Bio-PEPA: A framework for the modelling and analysis of biological systems
    Ciocchetta, Federica
    Hillston, Jane
    [J]. THEORETICAL COMPUTER SCIENCE, 2009, 410 (33-34) : 3065 - 3084
  • [9] Ant colony systems optimization applied to BNF grammars rule derivation (ACORD algorithm)
    de Mingo Lopez, Luis Fernando
    Gomez Blas, Nuria
    Morales Lucas, Clemencio
    [J]. SOFT COMPUTING, 2020, 24 (05) : 3141 - 3154
  • [10] Z3: An efficient SMT solver
    de Moura, Leonardo
    Bjorner, Nikolaj
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 : 337 - 340
123456