MCMAS: an open-source model checker for the verification of multi-agent systems

详细信息    查看全文

• 作者：Alessio Lomuscio ; Hongyang Qu…
• 关键词：Verification ; Multi ; agent systems ; Model checking
• 刊名：International Journal on Software Tools for Technology Transfer
• 出版年：2017
• 出版时间：February 2017
• 年：2017
• 卷：19
• 期：1
• 页码：9-30
• 全文大小：1357KB
• 刊物类别：Computer Science
• 刊物主题：Software Engineering; Software Engineering/Programming and Operating Systems; Theory of Computation;
• 出版者：Springer Berlin Heidelberg
• ISSN：1433-2787
• 卷排序：19

文摘

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.