Regular Vacuity

The application of model-checking tools to complex systems involves a nontrivial step of modelling the system by a finite-state model and a translation of the desired properties into a formal specification. While a positive answer of the model checker guarantees that the model satisfies the specification, correctness of the modelling is not checked. Vacuity detection is a successful approach for finding modelling errors that cause the satisfaction of the specification to be trivial. For example, the specification “every request is eventually followed by a grant” is satisfied vacuously in models in which requests are never sent. In general, a specification ϕ is satisfied vacuously in a model M if ϕ has a subformula ψ that does not affect the satisfaction of ϕ in M, where “does not affect” means we can replace ψ by a universally quantified proposition. Previous works focus on temporal logics such as LTL, CTL, and CTL∗ , and reduce vacuity detection to standard m...

• Type: Conference
• Year: 2005
• Where: CHARME
• Authors: Doron Bustan, Alon Flaisher, Orna Grumberg, Orna Kupferman, Moshe Y. Vardi
• Keywords: CHARME 2005, Hardware, Regular, Regular Layer, Vacuity Detection