Skip to content

Commit 7a6f5c2

Browse files
Update pubs.bib
1 parent 5e8c92a commit 7a6f5c2

File tree

1 file changed

+1
-2
lines changed

1 file changed

+1
-2
lines changed

pubs.bib

+1-2
Original file line numberDiff line numberDiff line change
@@ -17,12 +17,11 @@ @Inbook{Wright2025
1717
editor="Hinchey, Mike
1818
and Steffen, Bernhard",
1919
title="Formal Verification of BDI Agents",
20-
bookTitle="The Combined Power of Research, Education, and Dissemination: Essays Dedicated to Tiziana Margaria on the Occasion of Her 60th Birthday",
20+
booktitle="The Combined Power of Research, Education, and Dissemination: Essays Dedicated to Tiziana Margaria on the Occasion of Her 60th Birthday",
2121
year="2025",
2222
publisher="Springer Nature Switzerland",
2323
address="Cham",
2424
pages="302--326",
25-
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' 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's behaviour.",
2625
isbn="978-3-031-73887-6",
2726
doi="10.1007/978-3-031-73887-6_20",
2827
note={[<span class="tas_vn">TAS Verifiability Node</span>]},

0 commit comments

Comments
 (0)