Code

C++

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).