Advertisement

Regular Vacuity

  • Doron Bustan
  • Alon Flaisher
  • Orna Grumberg
  • Orna Kupferman
  • Moshe Y. Vardi
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)

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 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.

Keywords

Model Check Boolean Function Temporal Logic Regular Expression Linear Temporal Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
  2. 2.
    Armon, R., Fix, L., Flaisher, A., Grumberg, O., Piterman, N., Tiemeyer, A., Vardi, M.: Enhanced vacuity detection for linear temporal logic. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 368–380. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  3. 3.
    Armoni, R., et al.: The ForSpec temporal logic: A new temporal property-specification logic. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 211–296. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  4. 4.
    Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 363–367. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  5. 5.
    Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. FMSD 18(2), 141–162 (2001)zbMATHGoogle Scholar
  6. 6.
    Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem (1996)Google Scholar
  7. 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. 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. 9.
    Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  10. 10.
    Eiter, T., Gottlob, G., Schwentick, T.: Second-order logic over strings: Regular and non-regular fragments. In: Kuich, W., Rozenberg, G., Salomaa, A. (eds.) DLT 2001. LNCS, vol. 2295, pp. 37–56. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  11. 11.
    Fischer, M., Ladner, R.: Propositional dynamic logic of regular programs. JCSS 18, 194–211 (1979)zbMATHMathSciNetGoogle Scholar
  12. 12.
    Gastin, P., Oddoux, D.: Fast LTL to büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  13. 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
  14. 14.
    Gottlob, G., Kolaitis, P.G., Schwentick, T.: Existential second-order logic over graphs: Charting the tractability frontier. JACM 51(2), 312–362 (2000)CrossRefMathSciNetGoogle Scholar
  15. 15.
    Gurfinkel, A., Chechik, M.: Extending extended vacuity. In: 5th FMCAD. LNCS, vol. 2212, pp. 306–321 (2004)Google Scholar
  16. 16.
    Gurfinkel, A., Chechik, M.: How vacuous is vacuous. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 451–466. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  17. 17.
    Henriksen, J., Thiagarajan, P.: Dynamic linear time temporal logic. Annals of Pure and Applied Logic 96(1–3), 187–207 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Hopcroft, J., Ullman, J.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)zbMATHGoogle Scholar
  19. 19.
    Kupferman, O., Vardi, M.: Vacuity detection in temporal model checking. STTT 4(2), 224–233 (2003)Google Scholar
  20. 20.
    Kurshan, R.: FormalCheck User’s Manual. Cadence Design, Inc. (1998)Google Scholar
  21. 21.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)Google Scholar
  22. 22.
    Purandare, M., Somenzi, F.: Vacuum cleaning CTL formulae. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 485–499. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  23. 23.
    Rabin, M.: Decidability of second order theories and automata on infinite trees. Transaction of the AMS 141, 1–35 (1969)zbMATHCrossRefMathSciNetGoogle Scholar
  24. 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
  25. 25.
    Sistla, A., Clarke, E.: The complexity of propositional linear temporal logic. Journal ACM 32, 733–749 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  26. 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
  27. 27.
    Vardi, M., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Doron Bustan
    • 2
  • Alon Flaisher
    • 1
  • Orna Grumberg
    • 1
  • Orna Kupferman
    • 3
  • Moshe Y. Vardi
    • 2
  1. 1.TechnionHaifa
  2. 2.Rice University 
  3. 3.Hebrew University 

Personalised recommendations