DocumentCode
2787581
Title
Thorough Checking Revisited
Author
Nejati, Shiva ; Gheorghiu, Mihaela ; Chechik, Marsha
Author_Institution
Dept. of Comput. Sci., Toronto Univ., Ont.
fYear
2006
fDate
Nov. 2006
Firstpage
106
Lastpage
116
Abstract
Previous years have seen a proliferation of 3-valued models for capturing abstractions of systems, since these enable verifying both universal and existential properties. Reasoning about such systems is either inexpensive and imprecise (compositional checking), or expensive and precise (thorough checking). In this paper, we prove that thorough and compositional checks for temporal formulas in their disjunctive forms coincide, which leads to an effective procedure for thorough checking of a variety of abstract models and the entire mu-calculus
Keywords
formal verification; process algebra; temporal logic; abstract models; compositional checking; disjunctive forms; mu-calculus; temporal formulas; thorough checking; Automata; Computer science; High temperature superconductors; Logic; Minimization methods; Robustness;
fLanguage
English
Publisher
ieee
Conference_Titel
Formal Methods in Computer Aided Design, 2006. FMCAD '06
Conference_Location
San Jose, CA
Print_ISBN
0-7695-2707-8
Type
conf
DOI
10.1109/FMCAD.2006.33
Filename
4021016
Link To Document