基于改编命题动态逻辑的Agent交互协议推理

Reasoning about Agent Interaction Protocols Based on Adapted Propositional Dynamic Logic

Agent交互协议是“基于消息交流的Agent之间的”协调说明,用于提供交互的背景。交互协议是说明“所有参与Agent都应该遵守”的交互规则的公共文件。对命题动态逻辑进行改编得到的L逻辑,可以对多Agent系统的交互协议进行建模。为此,需要建立第一类协议说明语言,该语言是“把行为限制为由信道发送的消息的”行动语言,既可对协议结果进行表示和推理,也可对消息之外的行动进行推理,其约束语言用于说明消息和状态;每条消息被显式地定义为“对共享社会状态的处理”。

An agent interaction protocol is the specification that coordinates message-based communication between agents, and is used to provide a context of interaction. An interaction protocol is a public documents that explains the interaction rules by which all participating agents should abide. The logic Ladapted from propositional dynamic logic can model the interaction protocol of multi-agent system. Therefore, it is necessary to design a first-class of protocol specification language, which is an action language that restricts actions to be messages sent by a channel, which can not only represent and reason about outcomes of protocols, but also reason about actions other than messages, and its constraint language is used to specify messages and states. Each message is explicitly defined as a manipulation of a shared social state.