多Agent程序设计竞赛中地图合并协议的形式化验证
Formal Verification of a Map Merging Protocol in the Multi-Agent Programming Contest
摘要：
通信是使多智能体系统能够合作的关键部分。这意味着将形式化方法应用于多智能体系统内的通信协议，可以为其可靠性提供有用的信心。在本文中，我们描述了形式化验证的一个复杂的通信协议，协调代理合并他们的环境的地图。LFC团队在2019年的多智能体编程竞赛（MAPC）中使用了该协议。我们的协议规范是写在通信顺序进程（CSP），这是一个非常适合的方法来指定智能体通信协议，由于其重点是并发通信系统。我们使用已知正确行为的场景来验证规范的行为，并验证最终所有映射都已合并。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
