VITAMIN: A Compositional Framework for Model Checking of Multi-Agent Systems

TL;DR

The paper tackles the challenge of verifying multi-agent systems (MAS) by introducing VITAMIN, a highly compositional framework that decouples model formalisms from the logics used to specify properties. The main approach is a modular architecture with separate components for Models, Logics, a Model Checker Interface, and a User Interface, enabling multiple verification strategies ($explicit$, $symbolic$, $abstract$) and easy extension to new logics such as $ATL$ and $SL$ on model classes like $CGS$ and $IS$. The authors contribute a detailed architectural design, a hierarchy of components, and user-focused workflows for both expert and non-expert users, implemented in Python with a Streamlit GUI and a public repository. Although presented as a prototype without benchmarking, VITAMIN aims to facilitate broader adoption of formal verification in MAS by reducing specialization barriers and enabling community-driven extension of logics and models, with future work including NLP-assisted property specification and expanded model-checking interfaces.

Abstract

The verification of Multi-Agent Systems (MAS) poses a significant challenge. Various approaches and methodologies exist to address this challenge; however, tools that support them are not always readily available. Even when such tools are accessible, they tend to be hard-coded, lacking in compositionality, and challenging to use due to a steep learning curve. In this paper, we introduce a methodology designed for the formal verification of MAS in a modular and versatile manner, along with an initial prototype, that we named VITAMIN. Unlike existing verification methodologies and frameworks for MAS, VITAMIN is constructed for easy extension to accommodate various logics (for specifying the properties to verify) and models (for determining on what to verify such properties).

Figures (14)

• Figure 1: VITAMIN's architecture.
• Figure 2: Model component insights.
• Figure 3: Logic component insights.
• Figure 4: Model Checker Interface insights.
• Figure 5: Meta-node for Strategy Logic.