MCMAS: an open-source model checker for the verification of multi-agent systems
MCMAS: an open-source model checker for the verification of multi-agent systems
复制标题
DOI：
10.1007/s10009-015-0378-x
复制
发表时间：
2017-02-01
影响因子：
1.5
通讯作者：
Raimondi, Franco
中科院分区：
文献类型：
--
作者：
Lomuscio, Alessio;Qu, Hongyang;Raimondi, Franco
我们提出MCMA，这是用于验证多代理系统的模型检查器。 MCMAS支持有效的符号技术，用于验证多代理系统，以针对代表时间，认知和战略特性的规格进行验证。我们介绍了支持的规范语言的基本语义以及在MCMAS中实现的算法，包括其公平性和反例生成功能。我们提供了实施的详细描述。我们通过讨论许多示例并通过将其与其他模型检查器与常见案例研究中的多代理系统进行比较来评估其性能来说明其使用。
We present MCMAS, a model checker for the verification of multi-agent systems. MCMAS supports efficient symbolic techniques for the verification of multi-agent systems against specifications representing temporal, epistemic and strategic properties. We present the underlying semantics of the specification language supported and the algorithms implemented in MCMAS, including its fairness and counterexample generation features. We provide a detailed description of the implementation. We illustrate its use by discussing a number of examples and evaluate its performance by comparing it against other model checkers for multi-agent systems on a common case study.