MCK: Model Checking Knowledge

The system is intended as a testbed for a variety of approaches to model checking the logic of knowledge. The novelty of this model checker is that it supports several different ways of defining knowledge given a description of a multi-agent system and the observations made by the agents: observation alone; observation and clock; and perfect recall of all observations. Both linear and branching time temporal operators are supported. Currently, the system is based primarily on BDD-based model checking algorithms, but other approaches will be added as the system develops.

This work has been funded by an Australian Research Council Discovery Grant awarded to Ron van der Meyden. Peter Gammie was responsible for the current release. Extensions developed by Kai Baukus and Jeremy Lee will be included in a future release.

Documentation

Examples

A Robot with a Noisy Position Sensor

This is an example of verifying the implementation of a knowledge based program, in the sense of Fagin, Halpern, Moses and Vardi, Reasoning about Knowledge, MIT Press, 1995. The example is drawn from this book, and is a discretized version of an example of Brafman et al, JACM 97.

(MCK input file for the Robot)

One time Pad

This tests the security of the One Time Pad cipher on a single bit.

(MCK input file for the one time pad)

Increasing Mutual Knowledge in a Message Passing System

An example from R. van der Meyden, Common Knowledge and Update in Finite Environments, Information and Computation, 1998 that shows that in a message passing system with bounded but uncertain delivery times, the level of mutual knowledge about message delivery increases with time.

(MCK input file for the message passing system)

The Dining Cryptographers

The dining cryptographers protocol is a protocol for anonymous broadcast. For details see: D. Chaum The dining cryptographers problem: unconditional sender and recipient untraceability, Journal of Cryptology(1), 1988.

MCK input file for the protocol: dc_agent_protocol

An environment description setting up the protocol for 3 cryptographers sitting around a table: dc_environment3

Rivest's Oblivious Transfer Protocol

A protocol for oblivious transfer, with a trusted third party who does not need to be online at the time of the transfer. From Ronald L. Rivest. Unconditionally secure commitment and oblivious transfer schemes using private channels and a trusted initializer. (Unpublished report, available here).

MCK input file for Rivests protocol

Two Phase Commit

Two phase commit is a solution to the atomic commitment problem tpc3.

Source Code

• David Long's BDD library from CMU
• Peter Gammie's Haskell BDD interface (also available through the download link above)
• The Glasgow Haskell compiler, version 5.04 (Due to changes in GHC, MCK may not work with later versions)
• Various Haskell libraries, available from www.haskell.org: Happy (Haskell parser generator) c2hs (C to Haskell binding)

The system runs on Linux and Mac OS X. We have not tried other platforms as yet and would welcome positive and negative reports on this.

The current version of MCK is an alpha version. We make no warranty that the design of the system or its input language is stable, and welcome suggestions for improvements. We are particularly interested in hearing about novel applications.

Related Publications

• Model Checking Russian Cards , H.P. van Ditmarsch, W. van der Hoek, R. van der Meyden, J. Ruan, Electronic Notes in Theoretical Computer Science Volume 149, Issue 2 , 14 February 2006, Pages 105-123 Proceedings of the Third Workshop on Model Checking and Artificial Intelligence (MoChArt 2005) August 27, 2005 - San Francisco, CA, USA.
  
  
• A knowledge based analysis of cache coherence, K. Baukus and R. van der Meyden, International Conference on Formal Engineering Methods, Seattle, Nov 2004, LNCS No. 3308, pp. 99-114.
  
  
• MCK: Model Checking the Logic of Knowledge P. Gammie and R. van der Meyden, 16th International conference on Computer Aided Verification, CAV 2004, pp. 479- 483. (Copyright Springer-Verlag)
  
  
• Symbolic Model Checking the Knowledge of the Dining Cryptographers R. van der Meyden and K. Su, 17th IEEE Computer Security Foundations Workshop, Asilomar, June 2004, pp. 280-291
  
  
• Enhancing an epistemic logic model checker for application to extensions of the Dining Cryptographers problem, Lieu Le Vinh Nhu, UNSW Honours thesis, 2005.
  
  

Contact Information