MCTK2 is a symbolic model checker for multi-agent systems. It has a SMV-like input language, in which each agent is modeled as a module with observability description of variables. It currently supports the verification of CTLK, LTLK and their time-bounded versions. These temporal epistemic logics are model checked based on the observable semantics.
MCTK2 is now under development, built upon JTLV. The source code under development can be obtained from https://github.com/hovertiger/MCTK2-under-development
Cheers,
Xiangyu Luo College of Computer Science & Technology Huaqiao University Email: luo.xiangyu (at) yahoo.com