- The MCK model checker is one of only a few comparable systems internationally, and unique in the range of semantics-of-knowledge and model checking algorithms that it supports. It features:
- Observational, clock and perfect recall semantics of knowledge (subjective) probabilistic knowledge specifications
- Binary decision diagram based and bounded model checking algorithms, and
- Synthesis of implementations of knowledge-based programs
- Demonstrated applicability of the technology to a range of applications, including detecting non-optimal use of information in computer hardware designs, analysis of computer security protocols, and verification of pursuit-evasion scenarios.
- Improved software reliability and security
- Model Checking Knowledge and Probability, Defence R&D Canada
- Security Protocol Optimization and Verification by Epistemic Model Checking, US Air Force AOARD grant
- Independence-based Optimization of Epistemic Model Checking, US Air Force AOARD grant
- The MCK model checker has been licensed to Rationative Systems Inc.