Multi-Valued Model Checking via Groebner Basis Approach

The management of uncertainty and imprecision is becoming essential for modeling many real problems. Multivalued model checking, a generalization of classical model checking, is useful for analyzing models that contain uncertainty or inconsistency. This paper shows that Groebner bases can provide canonical symbolic representations for multi-valued logics, and therefore, can be applied to symbolic multi-valued model checking. We propose a general polynomial form of multi-valued logics, and then present a modified model checking algorithm based on the algebraic representations of mv-Kripke structures as well as mv-CTL formulas. This algebraic approach to multi-valued model checking could serve as a useful supplement to the existent method based on Multi-valued Decision Diagrams, and may give new guidance for verifying properties of systems containing uncertain or inconsistent information.