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
$\varphi$ is satisfied vacuously in a model $M$ if $\varphi$ has a
subformula $\psi$ that does not affect the satisfaction of $\varphi$
in~$M$, where ``does not affect'' means we can replace $\psi$ 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 regular expressions. Our goal in this work
is to extend vacuity detection to such a regular layer of
linear-temporal logics. We focus here on RELTL, which is the extension
of LTL with a regular layer. We define when a regular expression does
not affect the satisfaction of an RELTL formula by means of
universally quantified intervals. Thus, the transition to regular
vacuity takes us from monadic quantification to dyadic quantification.
We argue for the generality of our definition and show that
regular-vacuity detection is decidable, but involves an exponential
blow-up (in addition to the standard exponential blow-up for LTL model
checking).  This suggests that, in practice, one may need to work with
weaker definitions of vacuity or restrict attention to specifications
in which the usage of regular events is constrained.  We discuss such
weaker definitions, and show that their detection is not harder than
standard model checking. We also show that, under certain polarity
constraints, even general regular-vacuity detection can be reduced to
standard model checking.