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 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.
KeywordsModel Check Boolean Function Temporal Logic Regular Expression Linear Temporal Logic
- 1.Accellera, http://www.accellera.org
- 6.Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem (1996)Google Scholar
- 7.Büchi, J.: On a decision method in restricted second order arithmetic. In: Proc. Internat. Congr. Logic, Method. and Philos. Sci. 1960, Stanford, pp. 1–12 (1962)Google Scholar
- 8.Clarke, E., Grumberg, O., McMillan, K., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: Proc. 32nd DAC, pp. 427–432 (1995)Google Scholar
- 9.Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
- 13.Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification, Testing, and Verification, pp. 3–18. Chapman & Hall, Boca Raton (1995)Google Scholar
- 15.Gurfinkel, A., Chechik, M.: Extending extended vacuity. In: 5th FMCAD. LNCS, vol. 2212, pp. 306–321 (2004)Google Scholar
- 19.Kupferman, O., Vardi, M.: Vacuity detection in temporal model checking. STTT 4(2), 224–233 (2003)Google Scholar
- 20.Kurshan, R.: FormalCheck User’s Manual. Cadence Design, Inc. (1998)Google Scholar
- 21.Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)Google Scholar
- 24.Savelsberg, M., van emde Boas, P.: Bounded tiling, an alternative to satisfiability. In: 2nd Frege conference, pp. 354–363. Akademya Verlag (1984)Google Scholar
- 26.Vardi, M.: Nontraditional applications of automata theory. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 575–597. Springer, Heidelberg (1994)Google Scholar