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

翻译：多智能体系统（MAS）的验证是一项重大挑战。尽管存在多种应对此挑战的方法与途径，但支持它们的工具并非总是易于获取。即使能够获取此类工具，它们也往往是硬编码的，缺乏组合性，并且由于学习曲线陡峭而难以使用。本文提出了一种旨在以模块化和通用方式对MAS进行形式化验证的方法，并介绍了一个我们命名为VITAMIN的初始原型。与现有的MAS验证方法和框架不同，VITAMIN的设计易于扩展，能够兼容多种逻辑（用于指定待验证的属性）和模型（用于确定在何种对象上验证这些属性）。