crypto agents

Model Checking Knowledge

MCK is a model checker for the logic of knowledge, developed at the School of Computer Science and Engineering at the University of New South Wales. 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 synchonrous and asynchronous perfect recall of all observations. Both linear and branching time temporal operators are supported.

Earlier releases of MCK were based primarily on BDD-based model checking algorithms, but MCK now also supports bounded model checking as well as explicit state model checking.

For a brief overview of MCK and some of its applications, see the MCK White Paper.

MCK can be trialed via the MCK WEB APP.
A set of examples involving reasoning about knowledge in consensus protocols, using a version of MCK with an extended scripting language, is here.

Development of MCK has been funded by

Research on applications of MCK has been funded by

The following people have contributed to the development of MCK (in roughly historical order):

read more