Title :
Witness and Counter-Example on 3-Valued Model Checking
Author :
Jian Guo ; Jungang Han ; Naiyong Jin
Author_Institution :
Microelectron. Inst., Xidian Univ., Xidian
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;
Conference_Titel :
Fuzzy Systems and Knowledge Discovery, 2008. FSKD '08. Fifth International Conference on
Conference_Location :
Shandong
Print_ISBN :
978-0-7695-3305-6
DOI :
10.1109/FSKD.2008.589
