First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07) Multi-Valued Model Checking via Groebner Basis Approach Shanghai, China June 06-June 08 ISBN: 0-7695-2856-2
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TASE.2007.35
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.
Citation:
Jinzhao Wu, Lin Zhao, "Multi-Valued Model Checking via Groebner Basis Approach," tase, pp.35-44, First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07), 2007 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||