MCMAS: Model Checker for Multi-Agent Systems

Submitted by on Dec 14 2015 } Suggest Revision
By: Alessio Lomuscio
From: VAS Group, Imperial College London
Resource Type:
Data Format:


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