VITAMIN：一种面向多智能体系统模型检验的组合式框架
VITAMIN: A Compositional Framework for Model Checking of Multi-Agent Systems
AI总结：
本文提出VITAMIN组合式框架，以模块化、易扩展的方式支持多智能体系统的形式化验证，可灵活适配多种逻辑与模型，克服现有工具硬编码、缺乏组合性及难用的问题。
摘要：
多智能体系统（MAS）的验证构成了一项重大挑战。已有多种途径和方法可用于应对这一挑战；然而，支持这些方法的工具并不总是随时可用。即使能够获取此类工具，它们也往往采用硬编码实现，缺乏组合性，并且由于学习曲线陡峭而难以使用。在本文中，我们提出了一种旨在以模块化且灵活通用的方式对MAS进行形式化验证的方法，以及一个我们命名为VITAMIN的初始原型。与现有的MAS验证方法和框架不同，VITAMIN的构建方式便于扩展，以适应各种逻辑（用于指定待验证的性质）和各种模型（用于确定在什么对象上验证这些性质）。
英文摘要：
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).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
