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

File Description SizeFormat 
MCMAS_published_version.pdfPublished version1.18 MBAdobe PDFDownload
Title: MCMAS: an open-source model checker for the verification of multi-agent systems
Author(s): Lomuscio, AR
Qu, H
Raimondi, F
Item Type: Journal Article
Abstract: © 2015 The Author(s)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.
Publication Date: 26-Apr-2015
ISSN: 1433-2779
Publisher: Springer Verlag
Journal / Book Title: International Journal on Software Tools for Technology Transfer
Copyright Statement: © The Author(s) 2015. This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (, which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made
Publication Status: Published
Appears in Collections:Faculty of Engineering

Items in Spiral are protected by copyright, with all rights reserved, unless otherwise indicated.

Creative Commons