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.