How Vacuous is Vacuous?

Abstract

Model-checking gained wide popularity in analyzing software and hardware systems because of its ability to produce a counter-example when the desired universal temporal logic formula fails to hold. Yet, when this property is true, most model-checkers do not give users any additional information, The property may hold for the wrong reason, and the model or the property may still require fixing. For example, the property p: ``on all paths, a request is followed by an acknowledgment'' may hold because no requests have been generated.

Vacuity detection has been proposed to address the above problem. This technique is able to determine that the above property p is satisfied vacuously in systems where requests are never sent. Recent work in this area enabled the computation of interesting witnesses for the satisfaction of properties (in our case, those that satisfy p and contain a request) and vacuity detection with respect to subformulas with single and multiple subformula occurrences.

Often, the answer ``vacuous'' or ``not vacuous'' provided by existing techniques, is insufficient. Instead, we want to identify all subformulas of a given CTL formula that cause its vacuity, or better, identify all maximal such subformulas. Further, these subformulas may be mutually vacuous. In this paper, we propose a framework for identifying a variety of degrees of vacuity, including mutual vacuity between different subformulas. We cast this as a multi-valued model-checking problem and present the implementation of the general vacuity detection algorithm on top of a multi-valued model-checker.