# Modelling and Verifying BDI Agents with Bigraphs

arXiv: https://arxiv.org/abs/2105.02578 · HTML: https://mlsanity.com/paper/2105.02578/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 6 May 2021.

## Built on by (most cited first, 1 of 1)

- [Evaluating Theory of Mind and Internal Beliefs in LLM-Based Multi-Agent Systems](https://mlsanity.com/paper/2603.00142/) (2026)

## Abstract (arXiv)

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.