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

Luckcuck, Matt; Cardoso, Rafael C.

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.

Citation

Luckcuck, M., & Cardoso, R. C. (2021, May). Formal Verification of a Map Merging Protocol in the Multi-agent Programming Contest. Presented at 9th International Workshop, EMAS 2021, Virtual Event

• Presentation Conference Type: Edited Proceedings
• Conference Name: 9th International Workshop, EMAS 2021
• Start Date: May 3, 2021
• End Date: May 4, 2021
• Acceptance Date: Mar 9, 2022
• Online Publication Date: Mar 10, 2022
• Publication Date: Mar 10, 2022
• Deposit Date: Jul 25, 2025
• Print ISSN: 0302-9743
• Electronic ISSN: 1611-3349
• Peer Reviewed: Peer Reviewed
• Pages: 198-217
• Series Title: Lecture Notes in Computer Science
• Series Number: 13190
• Series ISSN: 1611-3349
• Book Title: Engineering Multi-Agent Systems: 9th International Workshop, EMAS 2021, Virtual Event, May 3–4, 2021, Revised Selected Papers
• ISBN: 9783030974565
• DOI: https://doi.org/10.1007/978-3-030-97457-2_12
• Public URL: https://nottingham-repository.worktribe.com/output/45862855
• Publisher URL: https://link.springer.com/chapter/10.1007/978-3-030-97457-2_12
• External URL: https://arxiv.org/abs/2106.04512