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被设计为易于扩展，能够兼容多种逻辑（用于指定待验证属性）与模型（用于界定在何种模型上验证这些属性）。