This paper provides a theoretical basis for multi-valued model-checking and discusses some of its applications. A companion paper~[Chechik et~al., 2002] describes implementation issues in detail. The model-checker works for any member of a large class of multi-valued logics. Our modeling language is based on a generalization of Kripke structures, where both atomic propositions and transitions between states may take any of the truth values of a given multi-valued logic. Properties are expressed in XCTL, our multi-valued extension of the temporal logic CTL.
We define the class of logics, present the theory of multi-valued
sets and multi-valued relations used in our model-checking algorithm,
and define the multi-valued extensions of CTL and Kripke
structures. We show that XCTL preserves the properties we expect it to
have, and that the model-checking algorithm is guaranteed to
terminate. We also address the use of fairness in multi-valued
model-checking. Finally, we discuss some applications of the
multi-valued model-checking approach.