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  and the MCTK 1.0 manual
for more details.
| Released time
|| Source code
| August 19, 2011
|| LGPL 2.1
|| minor revision for version 1.0.0|
| April 10, 2009
||This version supports fair model checking for temporal logics of knowledge CTLK and ECKLn, as well as CTL*|
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.