Verifying Unbounded and Open Systems

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

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

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

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

Click here to download the source code: MCMAS-OP