View article

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(req →Fgrant) (“every request is eventually followed by a grant”), we say that ϕ is satisfied vacuously in systems in which requests are never sent. Current …