Chek A Model Checker for Multi-Valued Reasoning

Abstract:  This paper describes our multi-valued symbolic modelchecker ?Chek. ?Chek is a generalization of an existing symbolic model-checking algorithm for a multi-valued extension of the temporal logic CTL. Multi-valued modelchecking supports reasoning with values other than just TRUE and FALSE. Multi-valued logics are useful in software engineering because they support explicit modeling of uncertainty, disagreement, and relative desirability or priority. For example, 3-valued logics have been used for interpreting results of static analysis with abstraction [5, 10], and for analyzing partial models [1]. The intermediate value of the logic is used to denote missing information. 4-valued logics have been used to model disagreements that arise when models drawn from different sources are composed [6]. The four values represent the four possible ways of combining the two classical values of the source models. Our model checker generalizes these approaches ? it works for the class of multi-valued logics whose logical values form a finite distributive lattice, and where there is a suitably defined negation operator that preserves De Morgan laws and involution (??a = a). Such structures are called quasi-boolean algebras [9]. Classical logic, as well as the 3- and 4-valued logics described in the literature, are examples of quasi-boolean algebras. In [3], we describe the properties of these logics. For tractability, we restrict ourselves to logics with a finite number of values. Examples of these logics are shown in Figure 1. 1(a) is classical 2-valued logic. 1(b) is a 3-valued logic suitable for representing partial models. 1(c) is the 4-valued logic TT T