论文标题
用于模型检查多代理系统的实用抽象
Practical Abstraction for Model Checking of Multi-Agent Systems
论文作者
论文摘要
众所周知，多代理系统（MAS）的模型检查在理论上还是在实践中都是困难的。智能的状态空间抽象可以显着降低模型，并促进验证。在本文中，我们根据MAS表示变量的去除，提出和研究基于直观剂的抽象方案。这允许在不生成系统的全局模型的情况下进行减少。此外，即使对于对计算机科学知识的领域专家来说，这个过程也很容易理解和控制。我们正式证明了该方法的正确性，并根据邮政投票程序的模型进行实验评估。
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.
