Extending Extended Vacuity
Abstract
There has been a growing interest in detecting whether a logic
specification holds in the system vacuously. For example, a
specification "every request is eventually followed by an
acknowledgment" holds vacuously on those systems that never generate
requests. In a recent paper, Armoni et al. have argued against
previous definitions of vacuity, defined as sensitivity with respect
to syntactic perturbation. They suggested that vacuity should be
robust, i.e., insensitive to trivial changes in the logic and
in the model, and is better described as sensitivity with respect to
semantic perturbation, represented by universal propositional
quantification. In this paper, we extend the above results by giving
a formal definition of robust vacuity that allows us to define and
detect vacuous satisfaction and vacuous failure for arbitrary CTL*
properties, even with respect to multiple occurrences of subformulas.
We discuss complexity of our approaches and study the relationship
between vacuity and abstraction.