MCTK: Model Checking Time and Knowledge

MCTK is a symbolic model checker for temporal logic of knowledge, developed by Kaile Su and Xiangyu Luo. It is developed based on NuSMV by CUDD under the Open Source license that allows free academic and non-commercial usage. It functionally extends the NuSMV 2.1.2 by dealing with CTL* and more worthy to point out, the CKLn formulas raised by Halpern and Vardi, which integrates knowledge and time with arbitrary order. In other words, MCTK can check the more complicated ECKLn that is an extension of CKLn by adding the path quantifiers A and E. The main model checking algorithm is given by Kaile Su in [1,2] and the current version 1.0 of MCTK interprets epistemic modalities under observable semantics. Please refer to paper [1] and the MCTK 1.0 manual for more details.

  • Download MCTK

 Released time
 Version  Source code
 License  Remarks
 August 19, 2011  1.0.1  MCTK-1.0.1(20110819).tar.gz  LGPL 2.1  minor revision for version 1.0.0
 April 10, 2009
 1.0.0 MCTK-1.0.0.tar.bz2 
LGPL 2.1 This version supports fair model checking for temporal logics of knowledge CTLK and ECKLn, as well as CTL*

[1] Kaile Su, Abdul SattarXiangyu LuoModel Checking Temporal Logics of Knowledge Via OBDDsComput. J. 50(4): 403-420 (2007)
[2] Kaile Su. Model Checking Temporal Logics of Knowledge in Distributed SystemsAAAI 2004: 98-103
[3] Kaile Su, Guanfeng Lv, Yan Zhang. Reasoning about Knowledge by Variable Forgetting. In Proceedings of the 9th International Conference on Principles of Knowledge Representation and Reasoning (KR-2004), Morgan Kaufmann Publishers, Inc., 2004.
[4] Ron van der Meyden and Kaile Su. Symbolic Model Checking the Knowledge of the Dining Cryptographers. 17th IEEE Computer Security Foundations Workshop, Asilomar, June 2004.
[5] Kai Engelhardt, Ron van der Meyden and Kaile Su. Modal Logics with a Hierarchy of Local Propositional Quantifiers (Preliminary Version), Proc. Advances in Modal Logic, Toulouse,France, Oct. 2002.(Best Paper Award)
[6] NuSMV website:
[7] Kaile Su, Abdul Sattar, Guanfeng Lv, Yan Zhang. Variable Forgetting in Reasoning about Knowledge. J. Artif. Intell. Res. (JAIR) 35: 677-716 (2009)

The basic theory of MCTK is proposed by Kaile Su (sukl at pku dot edu dot cn) and the tool is implemented by Xiangyu Luo (shiangyuluo at gmail dot com). Welcome to email bugs and suggestions on MCTK to help us improve it.