Model Checking Knowledge (MCK) in Distributed and Multi-Agent Systems

Model checking methodology automates the verification of computer software and hardware designs, based on algorithms that enable complete analysis of all possible behaviours of a system. Standard model checkers only consider how a system state evolves; whilst MCK model checker analyses how the knowledge of system components evolve over time.

Competitive advantage

  • 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.

Impact

  • Improved software reliability and security

Successful applications

  • 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

Our partners

  • The MCK model checker has been licensed to Rationative Systems Inc.
Tags
lensCommunications, Digital, Quantum and Cyber