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 条
  • [21] Fettke P, 2022, LECT NOTES COMPUT SC, V13703, P65, DOI 10.1007/978-3-031-19759-8_5
  • [22] Feurzeig W., 1970, ACM SIGCUE OUTLOOK, V4, P13, DOI DOI 10.1145/965754.965757
  • [23] Gordon M. J., 1979, Edinburgh LCF
  • [24] Gordon M. J. C., 1993, Introduction to HOL: A TheoremProving Environment for Higher-Order Logic
  • [25] SELF-ORGANIZED SHORTCUTS IN THE ARGENTINE ANT
    GOSS, S
    ARON, S
    DENEUBOURG, JL
    PASTEELS, JM
    [J]. NATURWISSENSCHAFTEN, 1989, 76 (12) : 579 - 581
  • [26] Grasse P. P., 1959, Insectes Sociaux Paris, V6, P41, DOI 10.1007/BF02223791
  • [27] Harrison J, 2005, LECT NOTES COMPUT SC, V3582, P529
  • [28] Harrison J., 2016, The HOL Light System Reference
  • [29] Harrison J., 2024, The HOL Light Theorem Prover.
  • [30] Harrison J., 2017, HOL light tutorial
123456