Title :
Symbolic Model Checking for Three Valued Logic
Author :
Guo, Jian ; Han, Jungang
Author_Institution :
Microelectron. Inst., Xidian Univ., Xian
Abstract :
Classical model checking can not be used to reason about system with uncertainty. We extend model checking in order to verify properties of a 3-valued system. A triple decision diagram (TDD) and its operations are given. Then states, transitional relations and label function of a system with a partial Kripke structure are implemented by TDDs. The algorithm of 3 valued symbolic model checking is presented. Finally potential applications in hardware and SoC are discussed.
Keywords :
symbol manipulation; temporal logic; SoC; TDD; classical model checking; partial Kripke structure; symbolic model checking; three valued logic; triple decision diagram; Boolean functions; Hardware; Logic design; Microelectronics; Mobile communication; Mobile computing; Signal design; Telecommunication computing; Uncertainty; SOC; formal verification; model checking; three-valued logic;
Conference_Titel :
Communications and Mobile Computing, 2009. CMC '09. WRI International Conference on
Conference_Location :
Yunnan
Print_ISBN :
978-0-7695-3501-2
DOI :
10.1109/CMC.2009.333
