The Community for Technology Leaders
Formal Methods in Computer Aided Design (2006)
San Jose, California, USA
Nov. 12, 2006 to Nov. 16, 2006
ISBN: 0-7695-2707-8
pp: 106-116
Mihaela Gheorghiu , University of Toronto, Canada
Marsha Chechik , University of Toronto, Canada
Shiva Nejati , University of Toronto, Canada
ABSTRACT
Recent 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.
INDEX TERMS
null
CITATION
Mihaela Gheorghiu, Marsha Chechik, Shiva Nejati, "Thorough Checking Revisited", Formal Methods in Computer Aided Design, vol. 00, no. , pp. 106-116, 2006, doi:10.1109/FMCAD.2006.33
95 ms
(Ver 3.3 (11022016))