One of the advantages of temporal-logic model-checking tools is their ability to accompany a negative answer to a correctness query with a counterexample to the satisfaction of the specification in the system. On the other hand, when the answer to the correctness query is positive, most model-checking tools provide no witness for the satisfaction of the specification. In the last few years there has been growing awareness of the importance of suspecting the system or the specification of containing an error also in cases where model checking succeeds. In particular, several works have recently focused on the detection of the vacuous satisfaction of temporal logic specifications. For example, when verifying a system with respect to the specification ψ = G(rep → Fgrant) ("every request is eventually followed by a grant"), we say that ψ is satisfied vacuously in systems in which requests are never sent. Current works have focused on detecting vacuity with respect to subformula occurrences. In this work we investigate vacuity detection with respect to subformulas with multiple occurrences. The generality of our framework requires us to re-examine the basic intuition underlying the concept of vacuity, which until now has been defined as sensitivity with respect to syntactic perturbation. We study sensitivity with respect to semantic perturbation, which we model by universal propositional quantification. We show that this yields a hierarchy of vacuity notions. We argue that the right notion is that of vacuity defined with respect to traces. We then provide an algorithm for vacuity detection and discuss pragmatic aspects.
展开▼
