Speaker: Jim Woodcock, University of York (Emeritus)
Tuesday 2025-02-11 14:00, Room to be announced
Abstract:
In this talk, we unveil a powerful formal modelling framework for the Belief-Desire-Intention (BDI) agent paradigm, combining the strengths of Isabelle/HOL and Z-Machines. The BDI architecture is a cornerstone for designing intelligent agents who think, plan, and act by maintaining beliefs about their world, pursuing ambitious goals (desires), and executing intentions to turn those goals into reality.
Our approach introduces a general-purpose formal model of BDI systems, meticulously crafted using Z-Machines. This framework captures the full spectrum of agent behaviour, from beliefs and actions to rules, plans, pattern matching, and rule applications. But we don't stop at modelling: through the precision of Hoare Logic and the expressive power of Isabelle/Z-Machines, we enable formal verification of an agent's behaviour, ensuring its decisions are not just intelligent but provably correct.
What makes this exciting? By blending automated reasoning with compositional verification techniques, our framework can uncover hidden bugs, verify critical invariants, and establish high-level system properties. To bring this to life, we present a case study featuring a nuclear inspector robot: an intelligent agent with a high-stakes mission. Our method verifies its behaviour and identifies subtle flaws, hinting at the value of formal verification in real-world applications.
This work pushes the boundaries of agent-based systems, demonstrating how rigorous formal methods can unlock trust and reliability in intelligent agents. It's not just about smarter agents; it's about agents you can trust when it matters most.
This is joint work with Thomas Wright (Aarhus), Louise Dennis (Manchester), and Simon Foster (York).