Multi-valued model checking [3], a generalization of classical model checking [4], works for any multi-valued logics whose truth values form a quasi-boolean lattice. The model is defined by a multi-valued Kripke (mv-Kripke) structure, which is like a Kripke structure except that both atomic propositions and transitions between states may take any of the truth values of a given multi-values logic. Properties to be checked are expressed in CTL (Computational Tree Logic), generalized with multi-valued semantics.