Formal Verification of a Map Merging Protocol in the Multi-agent Programming Contest

Luckcuck, Matt ORCID: 0000-0002-6444-9312 and Cardoso, Rafael C ORCID: 0000-0001-6666-6954 (2022) Formal Verification of a Map Merging Protocol in the Multi-agent Programming Contest. ENGINEERING MULTI-AGENT SYSTEMS, 13190. pp. 198-217. ISSN 0302-9743, 1611-3349

Text 2106.04512v2.pdf - Submitted version Download (533kB) | Preview

Abstract

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.

Item Type:	Article
Additional Information:	EMAS 2021 Proceedings Submitted Version
Uncontrolled Keywords:	Multi-Agent Programming Contest, Communicating Sequential Processes, Formal Verification, Agents Assemble, JaCaMo
Divisions:	Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User:	Symplectic Admin
Date Deposited:	20 Apr 2022 11:30
Last Modified:	06 Dec 2024 20:32
DOI:	10.1007/978-3-030-97457-2_12
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3153451