Hands-on VITAMIN: A Compositional Tool for Model Checking of Multi-Agent Systems

Verifying software and hardware systems is challenging due to their complexity, often making exhaustive verification impractical. Transitioning from monolithic systems to Multi-Agent Systems (MAS) exacerbates these challenges, requiring advanced tools for effective verification. Existing tools like MCMAS and STV face limitations in modularity, flexibility, and usability. This paper is based on VITAMIN (VerIficaTion of A MultI-ageNt system), a formal verification framework designed to support various logic and model formalisms while providing a user-friendly experience. Specifically, we apply VITAMIN to a case study in the robotics domain, focusing on an extension of Alternating-time Temporal Logic with resource bounds (RB-ATL). Through this case study, we demonstrate VITAMIN’s ability to guide end-users in the formal verification process and report experimental results to showcase its usability and feasibility.