@inbook{aac50cc85e6147058d43764aa67efb26,
title = "Formal Verification of BDI Agents",
abstract = "This paper presents a formal modelling approach for Belief-Desire-Intention (BDI) agents using Isabelle/HOL and Z-Machines. The BDI architecture is widely used for modelling intelligent agents, where agents possess beliefs about the environment, desires or goals to achieve, and intentions to execute plans for goal attainment. The paper introduces a general-purpose model of the BDI architecture using Z-Machines. The modelling framework includes specifications for beliefs, actions, rules, plans, pattern matching, and rule applications. The proposed model can be used to formally verify BDI agents{\textquoteright} behaviour using Hoare Logic and Isabelle/Z-Machines. This framework then contributes to advancing formal modelling and verification of agent-based systems, showing how we can integrate automated reasoning to establish invariant properties of agents with compositional techniques to prove more significant properties of BDI systems. We demonstrate the effectiveness of our approach through a case study of a nuclear inspector robot, showing how we can verify invariants and uncover bugs in the system{\textquoteright}s behaviour.",
keywords = "BDI, agent verification, theorem proving, Isabelle/HOL, Z-Machines, model checking",
author = "Thomas Wright and Dennis, {Louise A.} and Jim Woodcock and Simon Foster",
year = "2024",
month = oct,
day = "23",
doi = "10.1007/978-3-031-73887-6_20",
language = "English",
isbn = "978-3-031-73886-9",
series = "The Combined Power of Research, Education, and Dissemination",
publisher = "Springer Cham",
pages = "302--326",
booktitle = "The Combined Power of Research, Education, and Dissemination",
address = "Switzerland",
}