This page lists extensions of MCMAS that handle different specification logics and verification methods. For extensions that handle unbounded or open systems, please visit this page.
MCMAS-SDD is an experimental SDD-based symbolic model checker for the verification of multi-agent systems.
Click here to download the source code: MCMAS-SDD
MCMAS-SLK is an experimental model checker for the verification of multi-agent systems against specifications given in epistemic strategy logic.
Click here to download the source code: MCMAS-SLK
MCMAS-SL[1G] is an experimental model checker for the verification of multi-agent systems against specifications given in one-goal strategy logic.
Click here to download the source code: MCMAS-SL[1G]
MCMAS-LDLK is an experimental model checker for the verification of multi-agent systems against specifications given in the logic LDLK.