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).
We also provide the following binary files:
A graphical interface to be used as an Eclipse plug-in is also avaliable (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 email@example.com.
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: