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

TL;DR

VITAMIN is a modular, extensible framework for formal verification of multi-agent systems, addressing usability and flexibility issues present in existing tools.

Contribution

It introduces a compositional methodology and prototype that support easy extension for different logics and models in MAS verification.

Findings

Prototype demonstrates modular verification capabilities

Framework supports multiple logics and models

Enhances usability and extensibility of MAS verification tools

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).