Model checking of multi-agent systems (MAS) is known to be hard, both theoretically and in practice. A smart abstraction of the state space may significantly reduce the model, and facilitate the verification. In this paper, we propose and study an intuitive agent-based abstraction scheme, based on the removal of variables in the representation of a MAS. This allows to do the reduction without generating the global model of the system. Moreover, the process is easy to understand and control even for domain experts with little knowledge of computer science. We formally prove the correctness of the approach, and evaluate the gains experimentally on models of a postal voting procedure.

翻译：多智能体系统的模型检测在理论和实践中均被视为难题。对状态空间进行智能抽象可显著简化模型并有助于验证。本文提出并研究了一种基于智能体直觉的抽象方案——通过移除多智能体表示中的变量来实现约简。该方法无需生成系统的全局模型即可完成约简过程，且即使对于计算机科学知识有限的领域专家而言，该过程也易于理解与控制。我们严格证明了该方法的正确性，并通过邮政投票程序模型进行了实验性效益评估。