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 suggestion 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. © Springer-Verlag 2004.
CITATION STYLE
Gurfinkel, A., & Chechik, M. (2004). Extending extended vacuity. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3312, 306–321. https://doi.org/10.1007/978-3-540-30494-4_22
Mendeley helps you to discover research relevant for your work.