Formal Specification, and Verification of a Cooperative Multi-robots System for Delivery Service

The growing demand for efficient delivery services, especially in regions with infrastructure challenges, has led to the emergence of multi-robot systems as a potential solution. This paper introduces a formal specifying and verifying of a cooperative multi-robots system specifically developed for delivery services. The approach encompasses both the design of a delivery robot prototype and a rigorous formal specification framework to ensure robust coordination and safety. Using Büchi automata and UPPAAL model-checking tool, the system's safety and liveness properties which are represented by computational tree logic (CTL) were validated, demonstrating reliable navigation and task performance in dynamic environments. The results confirm the system's potential for enhancing delivery operations, providing a scalable, verifiable model suited for real-world deployment.