MCMAS is an open-source, OBDD-based symbolic model checker tailored to the verification of Multi-Agent Systems (MAS). MAS descriptions are given by means of ISPL (Interpreted Systems Programming Language) programs. ISPL is an agent-based, modular language inspired by interpreted systems, a popular semantics in MAS.
MCMAS supports a rich set of specifications, including CTL operators, epistemic operators, ATL, and notions pertaining to correct behaviour. Basic fairness conditions are supported. MCMAS enables the generation of counterexamples and witness executions for a wide range of specifications.
MCMAS can be used from a shell. A graphical interface (based on Eclipse) supporting a wide range of features is provided.
MCMAS runs on most architectures (Linux, Mac, Windows).
To download the latest publicly available release (ver 1.3.0) please follow this link.
To install MCMAS, please refer to the installation section of the manual.
We also provide the following binary files:
A graphical interface to be used as an Eclipse plug-in is also available (Java 7 is required).
Please refer to the manual for installation and usage details.
We welcome feedback on MCMAS. Please send your comments or requests for help to mcmas@imperial.ac.uk.
The following documentation is available for MCMAS:
Please click on the links above to download the manual and the guide. The manual contains a tutorial and detailed information about MCMAS, and the guide gives the detailed instructions for installation.
We gratefully acknowledge support from the following projects: