Communication is a critical part of enabling multi-agent systems to cooperate. This means that applying formal methods to protocols governing communication within multi-agent systems provides useful confidence in its reliability. In this paper, we describe the formal verification of a complex communication protocol that coordinates agents merging maps of their environment. The protocol was used by the LFC team in the 2019 edition of the Multi-Agent Programming Contest (MAPC). Our specification of the protocol is written in Communicating Sequential Processes (CSP), which is a well-suited approach to specifying agent communication protocols due to its focus on concurrent communicating systems. We validate the specification's behaviour using scenarios where the correct behaviour is known, and verify that eventually all the maps have merged.
翻译：通信是使多试剂系统能够开展合作的关键部分,这意味着对多试剂系统内部通信协议采用正式方法,可提供对其可靠性的有益信心。在本文件中,我们描述了对一个复杂的通信协议的正式核查,该协议负责协调将环境地图合并的代理人。该协议在2019年版的多代理人规划竞赛中被LFC小组使用。我们的协议的规格是在通信程序程序(CSP)中写成的,这是一个非常适合具体指明代理人通信协议的方法,因为它侧重于同时的通信系统。我们用已知正确行为的情形验证规格的行为,并核实所有地图最终已经合并。
相关内容
微信扫码咨询专知VIP会员