Verifying BDI Agents in Dynamic Environments
Blair Archibald, Muffy Calder, Michele Sevegnani, Mengwei Xu · Proceedings/Proceedings of the ... International Conference on Software Engineering and Knowledge Engineering · 2022
The Belief-Desire-Intention (BDI) architecture is a popular framework for rational agents, yet most verification approaches are limited to analysing the behaviours of an agent in a subset of all possible environments.However, in practice, BDI agents operate in dynamic environments where the exact occurrence of external changes is difficult to predict.For safety/security we need to assess whether the agent behaves as required in all circumstances.To address this, we define environments, accounting for both sensor information about physical changes and new tasks to be completed, as a non-deterministic finitestate automata.We give an environment-enabled extension to the Conceptual Agent Notation (CAN) language including an executable semantics via an encoding to Milner's bigraphs and the BigraphER tool.We illustrate the framework through a simple Unmanned Aerial Vehicle (UAV) example that is verified using mainstream tools including PRISM model checker.Results show our approach can automatically identify agent design flaws to aid agent programmers in design, debugging, and analysis.