/MCTK2

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, ATLK, ATL*K and their time-bounded versions. These temporal epistemic logics are model checked based on the observable semantics.

GNU General Public License v3.0GPL-3.0

MCTK2

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