MCMAS is an OBDD-based symbolic model checker
tailored to the verification of Multi-Agent Systems (MAS). MAS
descriptions are given by means of programs in ISPL (Interpreted
Systems Programming Language), a modular language inspired by
interpreted systems, a popular semantics in MAS.
MAS supports a rich set of specifications,
including CTL operators, epistemic operators, ATL, and notions
pertaining to correct behaviour. Basic fairness conditions are
MCMAS produces counterexamples and witness executions for a wide range
In addition to stand-alone mode a graphical interface (based on Eclipse) supporting a wide range of features is provided.