Modelling and verifying BDI agents with bigraphs
Modelling and verifying BDI agents with bigraphs
复制标题
使用双图对 BDI 代理进行建模和验证
DOI：
10.1016/j.scico.2021.102760
复制
发表时间：
2022
影响因子：
1.3
通讯作者：
Archibald B
中科院分区：
文献类型：
--
作者：
Archibald B
信念-欲望-意图（Belief-Desire-Intention， BDI）架构是一种流行的理性主体框架；现有的验证方法要么直接将简化的BDI语言（例如缺少故障恢复等功能）编码到现有的验证框架（例如Promela）中，要么对特定的BDI语言实现进行推理。我们采用另一种方法，采用米尔纳的图作为全功能BDI语言的建模框架，概念代理符号（CAN）是AgentSpeak的超集，具有声明性目标、并发性和故障恢复。我们提供了canagent的语法和语义编码，并给出了编码忠实性的严格证明。验证基于包括BigraphER在内的主流软件工具的使用，并且验证无人驾驶飞行器（uav）的几个属性的小案例研究说明了该框架的作用。可执行框架是一个基础步骤，它将支持更高级的推理，如计划偏好、意图优先级和权衡，以及与不确定环境的交互。
The Belief-Desire-Intention (BDI) architecture is a popular framework for rational agents; existing verification approaches either directly encode simplified (e.g. lacking features like failure recovery) BDI languages into existing verification frameworks (e.g. Promela), or reason about specific BDI languageimplementations. We take an alternative approach and employ Milner's bigraphs as a modelling framework for a fully featured BDI language, the Conceptual Agent Notation (CAN)—a superset of AgentSpeak featuring declarative goals, concurrency, and failure recovery. We provide an encoding of the syntax and semantics ofCanagents, 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. Theexecutableframework 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.