DocumentCode
2940059
Title
Symbolic Model Checking for Three Valued Logic
Author
Guo, Jian ; Han, Jungang
Author_Institution
Microelectron. Inst., Xidian Univ., Xian
Volume
3
fYear
2009
fDate
6-8 Jan. 2009
Firstpage
401
Lastpage
405
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Communications and Mobile Computing, 2009. CMC '09. WRI International Conference on
Conference_Location
Yunnan
Print_ISBN
978-0-7695-3501-2
Type
conf
DOI
10.1109/CMC.2009.333
Filename
4797285
Link To Document