Parameterized vacuity

Abstract

In model checking, a specification is vacuously true, if some subformula can be modified without affecting the truth value of the specification. Intuitively, this means that the property expressed in this subformula is satisfied for a trivial reason, and likely not the intended one. It has been shown by Kupferman and Vardi that vacuity detection can be reduced to model checking of simplified specifications where the subformulas of interest are replaced by constant truth values. In this paper, we argue that the common definition describes extreme cases of vacuity where the subformula indeed collapses to a constant truth value. We suggest a refined notion of vacuity (weak vacuity) which is parameterized by a user-defined class of vacuity causes. Under this notion, a specification is vacuously true, if a subformula collapses to a vacuity cause. Our analysis exhibits a close relationship between vacuity detection and temporal logic query solving. We exploit this relationship to obtain vacuity detection algorithms in symbolic, automata-theoretic, and multi-valued frameworks. © Springer-Verlag 2004.