loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
Jinzhao Wu, University of Electronic Science and Technology
Lin Zhao, Chinese Academy of Sciences
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.