Encoding BDI Syntax with Theories in Event-B

Abstract

The Belief–Desire–Intention (BDI) paradigm is a popular framework in the development of autonomous systems. However, assuring the correct design of BDI agents remains difficult: existing modelling formalisms often require ad-hoc encodings of BDI agents that can be difficult to validate, maintain, and reason about. This paper focuses on modelling the syntax of BDI agents and shows how algebraic modelling in Event-B theories (e.g. inductive data types and polymorphic constructors) yields a faithful, compact, and reusable encoding of BDI syntax. Even without committing to the full BDI semantics, the encoding already supports useful reasoning, including belief entailment and belief-based invariant checking, and provides a path towards a future BDI semantic encoding via operators in theories and machine events in Event-B.

Short Biography

Mengwei studied Mathematics for his undergraduate. After the undergraduate, Mengwei pursued a PhD degree in autonomous agents supervised by Professor Weiru Liu at University of Bristol. After the PhD, Mengwei worked as a Research Associate on trustworthy autonomous agents with e.g. Professor Dame Muffy Calder at the University of Glasgow. After it, Mengwei was a Research Fellow from Jan 2023 to August 2023 in Autonomy and Verification Group, working with Dr. Louise Dennis, focusing on safeguarding data privacy through trustworthy autonomous agents, at the University of Manchester. From Sep 2023, Mengwei is a lecturer (Assistant Professor) at Group of Advanced Model-Based Engineering and Reasoning (AMBER) at the School of Computing at the Newcastle University.