swMATH ID: 9465
Software Authors: Ron van der Meyden; Peter Gammie; Kai Baukus; Jeremy Lee; Cheng Luo; Xiaowei Huang
Description: MCK: 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.
Homepage: http://cgi.cse.unsw.edu.au/~mck/pmck/
Related Software: MCMAS; VerICS; NuSMV; CUDD; MOCHA; SPIN; DEMO; Verics; SMCDEL; jMocha; MCMAS-SLK; nuXmv; Simulink; PVS; z3; MMC; PicoSAT; 3APL; AgentSpeak; PRISM
Cited in: 33 Publications
Further Publications: http://cgi.cse.unsw.edu.au/~mck/pmck/mcks/publications

Citations by Year