Modelling and Verifying BDI Agents with Bigraphs

TL;DR

This paper introduces a novel approach to model and verify BDI agents using bigraphs, providing a formal encoding of CAN language semantics and demonstrating its effectiveness through UAV case studies.

Contribution

It presents the first formal encoding of BDI agent semantics with bigraphs, enabling verification with existing tools and supporting advanced reasoning features.

Findings

Successful encoding of CAN language semantics into bigraphs

Verification of UAV properties using BigraphER

Foundation for future reasoning about plan preferences and environment interactions

Abstract

The Belief-Desire-Intention (BDI) architecture is a popular framework for rational agents; most verification approaches are based on reasoning about implementations of BDI programming languages. We investigate an alternative approach based on reasoning about BDI agent semantics, through a model of the execution of an agent program. We employ Milner's bigraphs as the modelling framework and present an encoding for the Conceptual Agent Notation (CAN) language - a superset of AgentSpeak featuring declarative goals, concurrency, and failure recovery. We provide an encoding of the syntax and semantics of CAN agents, and give a rigorous proof that the encoding is faithful. Verification is based on the use of mainstream software tools including BigraphER, and a small case study verifying several properties of Unmanned Aerial Vehicles (UAVs) illustrates the framework in action. The executable framework is a foundational step that will enable more advanced reasoning such as plan preference, intention priorities and trade-offs, and interactions with an environment under uncertainty.