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 well-suited approach to specifying agent communication protocols due to its focus on concurrent communicating systems. We validate the specification's behaviour using five scenarios where the correct behaviour is known, and verify that eventually all the maps have merged.
翻译：通信是使多试剂系统能够进行合作的关键部分,这意味着对多试剂系统内部的通信议定书采用正式方法可提供对其可靠性的有益信任。本文描述了对一个复杂的通信协议的正式核查,该协议将协调其环境地图合并的代理人。该协议在2019年版的多代理人规划竞赛中被LFC小组使用。我们的协议的规格是在通信序列过程(CSP)中写成的,这是非常适合具体指明代理人通信协议的方法,因为它侧重于同时的通信系统。我们用已知正确行为的五种情景验证规格的行为,并核实所有地图最终已经合并。
相关内容
微信扫码咨询专知VIP会员