MCMAS-P is an experimental model checker for the verification of Unbounded Multi-Agent Systems (UMAS), a class of multi-agent systems where the number of agents is unknown at design time.

MCMAS-P takes input in PISPL (Parameterised Interpreted Systems Programming Language), a programming language that closely follows parameterised interpreted systems, an extension of interpreted systems (one of the main formalisms for multi-agent systems) to reason about the temporal-epistemic properties of UMAS.

MCMAS-P is built on top of MCMAS, an OBDD-based symbolic model checker tailored to the verification of multi-agent systems.

MCMAS-P is available for download from here.