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
MCMAS-Pis available for download from here.