DocumentCode
477824
Title
Witness and Counter-Example on 3-Valued Model Checking
Author
Jian Guo ; Jungang Han ; Naiyong Jin
Author_Institution
Microelectron. Inst., Xidian Univ., Xidian
Volume
2
fYear
2008
fDate
18-20 Oct. 2008
Firstpage
633
Lastpage
637
Abstract
Model checking of 3-valued logical formulae is analyzed. The solution is presented when the value of model checking for a 3-valued logical formula is UNKNOWN. In this paper, a proof system is established on a 3-valued logic, with additional proof steps, by which the approaches of extracting witness (counter-example) when the result on checking a formula with existential (universal) path quantifier is UNKNOWN are obtained. The direction of refinement in a partial Kripke structure is given by witnesses and counter-examples.
Keywords
formal logic; formal verification; theorem proving; 3-valued logical formula; 3-valued model checking; counter example; existential path quantifier; proof system; witness extraction; Application software; Explosions; Fuzzy systems; Hardware; Logic; Microelectronics; Telecommunication computing; counter-example; model checking; partial Kripke structure; witness;
fLanguage
English
Publisher
ieee
Conference_Titel
Fuzzy Systems and Knowledge Discovery, 2008. FSKD '08. Fifth International Conference on
Conference_Location
Shandong
Print_ISBN
978-0-7695-3305-6
Type
conf
DOI
10.1109/FSKD.2008.589
Filename
4666193
Link To Document