Epistemic Model Checkers: Detailed Overview

MCMAS (Model Checker for Multi-Agent Systems)

Official Website: https://sail.doc.ic.ac.uk/software/mcmas/
Developer: Imperial College London
Language: C++
Input Language: ISPL (Interpreted Systems Programming Language)

MCMAS is one of the most mature and widely-used epistemic model checkers. It's specifically designed for verifying temporal-epistemic properties in multi-agent systems using the interpreted systems semantics.

Key Features:

• Supports temporal-epistemic logic (CTLK - Computational Tree Logic with Knowledge)
• Uses interpreted systems as the underlying semantic model
• Handles multiple agents with individual knowledge bases
• Supports common knowledge and distributed knowledge
• Includes optimizations like symbolic model checking with BDDs
• Provides counterexample generation for failed properties
• Supports fairness constraints
• Can handle both synchronous and asynchronous systems

Strengths:

• Well-documented with extensive academic backing
• Efficient symbolic algorithms
• Good tool support with GUI interface
• Active development and maintenance
• Strong theoretical foundation

Limitations:

• Limited to interpreted systems semantics
• Steep learning curve for ISPL syntax
• Performance can degrade with large state spaces

MCK (Model Checker for Knowledge)

Official Website: https://cgi.cse.unsw.edu.au/~mck/pmck/
Developer: University of New South Wales
Language: C
Input Language: Extended SMV language with epistemic operators

MCK extends the traditional model checking approach to include epistemic reasoning. It builds upon the SMV framework but adds epistemic operators and semantics.

Key Features:

• Supports epistemic temporal logic
• Uses Kripke structures with epistemic accessibility relations
• Handles multiple agents and knowledge modalities
• Supports both individual and group knowledge concepts
• Integrates with existing SMV-based workflows
• Provides epistemic bisimulation checking

Strengths:

• Familiar SMV-like syntax for users of traditional model checkers
• Good integration with existing verification workflows
• Supports standard epistemic logic constructs

Limitations:

• Less actively maintained than MCMAS
• Limited documentation compared to newer tools
• Performance optimization not as advanced as symbolic approaches

Feature Comparison Matrix

Legend

• ✅ Full support/Excellent
• ⚠️ Limited support/Fair
• ❌ No support/Poor

Recommendations by Use Case

For Academic Research: MCMAS - Most comprehensive, well-documented, active development

For Integration with Existing SMV Workflows: MCK - Familiar syntax, good compatibility

For Performance-Critical Applications: MCMAS - Best symbolic algorithms and optimizations