Regular vacuity

Abstract. 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 model checking. A major feature of recent industrial property-specification languages is their regular layer, which includes regular expressions and formulas constructed from regula