Scholarlink

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.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Encoding BDI Syntax with Theories in Event-B

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Mengwei Xu,
  • Peter Rivière,
  • Toshiaki Aoki,
  • Marie Farrell,
  • Yamine Aït Ameur,
  • Neeraj Kumar Singh,
  • Guillaume Dupont

摘要

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.