This paper describes our multi-valued symbolic model-checker XChek. XChek is a generalization of an existing symbolic model-checking algorithm for a multi-valued extension of the temporal logic CTL. Multi-valued model-checking supports reasoning with values other than just TRUE and FALSE.

This article introduces the concept of multi-valued model-checking and describes a multi-valued symbolic model-checker, ΧChek. 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 article provides a theoretical basis for multi-valued model-checking and discusses some of its applications. A companion article [Chechik et al. 2002b] 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 ΧCTL, 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 explore the relationship between ΧCTL and CTL, and provide a symbolic model-checking algorithm for ΧCTL. We also address the use of fairness in multi-valued model-checking. Finally, we discuss some applications of the multi-valued model-checking approach.

Temporal logic query checking was first introduced by W. Chan in order to speed up design understanding by discovering properties not known a priori. A query is a temporal logic formula containing a special symbol ?/sub 1/, known as a placeholder. Given a Kripke structure and a propositional formula /spl phi/, we say that /spl phi/ satisfies the query if replacing the placeholder by /spl phi/ results in a temporal logic formula satisfied by the Kripke structure. A solution to a temporal logic query on a Kripke structure is the set of all propositional formulas that satisfy the query. Query checking helps discover temporal properties of a system and, as such, is a useful tool for model exploration. In this paper, we show that query checking is applicable to a variety of model exploration tasks, ranging from invariant computation to test case generation. We illustrate these using a Cruise Control System. Additionally, we show that query checking is an instance of a multi-valued model checking of Chechik et al. This approach enables us to build an implementation of a temporal logic query checker, TLQSolver, on top of our existing multi-valued model checker /sub /spl chi//Chek. It also allows us to decide a large class of queries and introduce witnesses for temporal logic queries-an essential notion for effective model exploration.

A temporal logic query is a temporal logic formula with placeholders. Given a model, a solution to a query is a set of assignments of propositional formulas to placeholders, such that replacing the placeholders with any of these assignments results in a temporal logic formula that holds in the model. Query checking, first introduced by William Chan \citechan00, is an automated technique for finding solutions to temporal logic queries. It allows discovery of the temporal properties of the system and as such may be a useful tool for model exploration and reverse engineering.This paper describes an implementation of a temporal logic query checker. It then suggests some applications of this tool, ranging from invariant computation to test case generation, and illustrates them using a Cruise Control System.