Abstract
We re-examine vacuity in temporal logic model checking. We note two disturbing phenomena in recent results in this area. The first indicates that not all vacuities detected in practical applications are considered a problem by the system verifier. The second shows that vacuity detection for certain logics can be very complex and time consuming. This brings vacuity detection into an undesirable situation where the user of the model checking tool may find herself waiting a long time for results that are of no interest for her.
In this paper we define Temporal Antecedent Failure, an extension of antecedent failure to temporal logic, which refines the notion of vacuity. According to our experience, this type of vacuity always indicates a problem in the model, environment or formula. On top, detection of this vacuity is extremely easy to achieve. We base our definition and algorithm on regular expressions, that have become the major temporal logic specification in practical applications.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Armoni, R., Fix, L., Flaisher, A., Grumberg, O., Piterman, N., Tiemeyer, A., Vardi, M.: Enhanced vacuity detection in linear temporal logic. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 368–380. Springer, Heidelberg (2003)
Beatty, D., Bryant, R.: Formally verifying a microprocessor using a simulation methodology. In: Design Automation Conference, pp. 596–602 (1994)
Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 279–290. Springer, Heidelberg (1997)
Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in temporal model checking. Formal Methods in System Design 18(2), 141–163 (2001)
Beer, I., Ben-David, S., Landver, A.: On-the-fly model checking of RCTL formulas. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 184–194. Springer, Heidelberg (1998)
Ben-David, S., Fisman, D., Ruah, S.: Automata construction for regular expressions in model checking (IBM research report H-0229) (2004)
Ben-David, S., Fisman, D., Ruah, S.: Embedding finite automata within regular expressions. In: Margaria, T., Steffen, B. (eds.) 1st International Symposium on Leveraging Applications of Formal Methods, Springer, Heidelberg (2004)
Ben-David, S., Fisman, D., Ruah, S.: The safety simple subset. In: Ur, S., Bin, E., Wolfsthal, Y. (eds.) Hardware and Software, Verification and Testing. LNCS, vol. 3875, pp. 14–29. Springer, Heidelberg (2006)
Ben-David, S., Fisman, D., Ruah, S.: Temporal antecedent failure: Refining vacuity (IBM research report H-0252) (2007)
Berry, G., Sethi, R.: From regular expressions to deterministic automata. Theoretical Computer Science 48(1), 117–126 (1986)
Boul’e, M., Zilic, Z.: Efficient automata-based assertion-checker synthesis of psl properties. In: HLDVT 2006. Workshop on High LevelDesign, Validation, and Test (2006)
Bustan, D., Fisman, D., Havlicek, J.: Automata construction for PSL. Technical Report MCS05-04, The Weizmann Institute of Science (2005)
Bustan, D., Flaisher, A., Grumberg, O., Kupferman, O., Vardi, M.Y.: Regular vacuity. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, Springer, Heidelberg (2005)
Chechik, M., Gurfinkel, A., Gheorghiu, M.: Finding environmental guarantees. In: FASE 2007 (2007)
Clarke, E., Emerson, E.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (2000)
Dong, Y., saran Starosta, B., Ramakrishnan, C., Smolka, S.A.: Vacuity checking in the modal mu-claculus. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 147–162. Springer, Heidelberg (2002)
Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer (2006)
Gurfinkel, A., Chechik, M.: Extending extended vacuity. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 306–321. Springer, Heidelberg (2004)
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)
IBM’s Model Checker RuleBase. http://www.haifa.il.ibm.com/projects/verification/rb_homepage/index.html
Annex E of IEEE Standard for SystemVerilog — Unified Hardware Design, Specification, and Verification Language. IEEE Std 1800TM-2005
IEEE Standard for Property Specification Language (PSL). IEEE Std 1850TM-2005
Kupferman, O., Vardi, M.: Vacuity detection in temporal model checking. STTT 4(2), 224–233 (2003)
McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)
Namjoshi, K.S.: An efficiently checkable, proof-based formulation of vacuity in model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 57–69. Springer, Heidelberg (2004)
Purandare, M., Somenzi, F.: Vacuum cleaning CTL formulae, pp. 485–499 (July 2002)
Quielle, J., Sifakis, J.: Specification and verification of concurrent systems in cesar. In: 5th International Symposium on Programming (1982)
Samer, M., Veith, H.: Parametrized vacuity. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 322–336. Springer, Heidelberg (2004)
Tzoref, R., Grumberg, O.: Automatic refinement and vacuity detection for symbolic trajectory evaluation. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 190–204. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ben-David, S., Fisman, D., Ruah, S. (2007). Temporal Antecedent Failure: Refining Vacuity. In: Caires, L., Vasconcelos, V.T. (eds) CONCUR 2007 – Concurrency Theory. CONCUR 2007. Lecture Notes in Computer Science, vol 4703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74407-8_33
Download citation
DOI: https://doi.org/10.1007/978-3-540-74407-8_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74406-1
Online ISBN: 978-3-540-74407-8
eBook Packages: Computer ScienceComputer Science (R0)