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的构建旨在易于扩展，以适应各种逻辑（用于指定待验证的属性）和模型（用于确定在何种对象上验证这些属性）。