Thorough Checking Revisited
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.