Multi-Valued Symbolic Model-Checking

Abstract

This paper introduces the concept of multi-valued model-checking and describes a multi-valued symbolic model-checker XChek. Multi-valued model-checking is a generalization of classical model-checking, useful for analyzing models that contain uncertainty (lack of essential information) or inconsistency (contradictory information often occurring when information is gathered from multiple sources). Multi-valued logics support the explicit modeling of uncertainty and disagreement by providing additional truth values in the logic.

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.