Modelling and Verifying BDI Agents with Bigraphs
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.
Cite
@article{arxiv.2105.02578,
title = {Modelling and Verifying BDI Agents with Bigraphs},
author = {Blair Archibald and Muffy Calder and Michele Sevegnani and Mengwei Xu},
journal= {arXiv preprint arXiv:2105.02578},
year = {2021}
}
Comments
50 pages, 24 figures