This page includes a number of software packages for the verification of non-probabilistic systems that are unbounded or open. For tools that verify probabilistic systems, please visit this page.
MCMAS-P is an experimental model checker for the verification of multi-agent systems with an unbounded number of agents.
Click here to download the source code: MCMAS-P
MCMAS-S is an experimental model checker for the verification of security properties in unbounded multi-agent systems.
Click here to download the source code: MCMAS-S
MCMAS-OP is an experimental model checker for the verification of open multi-agent systems. Further details can be found in the corresponding paper (published at AAMAS 2019).