MCMAS: An Open-Source Model Checker for the Verification of Multi-Agent Systems

2 min read

MCMAS is a symbolic model checker for multi-agent systems. Agents are described in ISPL (Interpreted Systems Programming Language) by their private local states, actions, protocols and evolution rules, and properties are written in ATLK: branching-time logic plus knowledge operators (“agent i knows φ”, common and distributed knowledge) plus strategic operators from ATL (“this coalition has a strategy to force φ”). Sets of states and transitions are stored as ordered binary decision diagrams, with support for fairness constraints and counterexample generation.

Findings

  • On the dining cryptographers benchmark (checking that a non-paying cryptographer learns nothing about who paid), MCMAS verified 60 cryptographers in 14.2 seconds. MCK timed out from 30 cryptographers, and MCTK took 72.4 seconds at 50 and timed out at 60.
  • The paper reports a software-procurement web-services case with about 10^6 reachable states, where knowledge properties of the contracting parties check in a few seconds.
  • MCMAS has been open source since 2003 and is released under the GNU GPL.

Limits

  • Finite-state, discrete models only. Continuous dynamics and timing must be abstracted away before the checker sees them.
  • Epistemic properties are about what agents could know under the model’s observability, not what a real robot’s estimator believes.
  • Perfect recall and other expensive semantics are only partly supported, as the authors note.

Relevance

“Does robot i know that robot j is faulty?” is an epistemic question, and MCMAS is one of the few tools that can state it. That fits detection in teams where robots see different things, though the gap between the ISPL model and a real swarm is large. Luckcuck et al. list an AUV verified this way; see multi-robot systems, Byzantine fault tolerance and robust robotics.