Abstract
In model checking, a specification is vacuously true, if some subformula can be modified without affecting the truth value of the specification. Intuitively, this means that the property expressed in this subformula is satisfied for a trivial reason, and likely not the intended one. It has been shown by Kupferman and Vardi that vacuity detection can be reduced to model checking of simplified specifications where the subformulas of interest are replaced by constant truth values.
In this paper, we argue that the common definition describes extreme cases of vacuity where the subformula indeed collapses to a constant truth value. We suggest a refined notion of vacuity (weak vacuity) which is parameterized by a user-defined class of vacuity causes. Under this notion, a specification is vacuously true, if a subformula collapses to a vacuity cause. Our analysis exhibits a close relationship between vacuity detection and temporal logic query solving. We exploit this relationship to obtain vacuity detection algorithms in symbolic, automata-theoretic, and multi-valued frameworks.
This work was supported by the European Community Research Training Network “Games and Automata for Synthesis and Validation” (GAMES), the EU Project ECRYPT, and by the Austrian Science Fund Project Z29-N04. The results presented in this paper have been developed as part of [18].
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Armoni, R., Fix, L., Flaisher, A., Grumberg, O., Piterman, N., Tiemeyer, A., Vardi, M.Y.: 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.L., Bryant, R.E.: Formally verifying a microprocessor using a simulation methodology. In: Proceedings of the 31st Annual ACM/IEEE Design Automation Conference (DAC), pp. 596–602. ACM Press, New York (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)
Bruns, G., Godefroid, P.: Temporal logic query checking. In: Symposium on Logic in Computer Science (LICS), pp. 409–417. IEEE Computer Society, Los Alamitos (2001)
Bustan, D., Flaisher, A., Grumberg, O., Kupferman, O., Vardi, M.Y.: Regular vacuity. Submitted for publication
Chan, W.: Temporal-logic queries. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 450–463. Springer, Heidelberg (2000)
Chechik, M., Gurfinkel, A.: TLQSolver: A temporal logic query checker. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 210–214. Springer-Verlag, Heidelberg (2003)
Clarke, E.M., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 19–29. IEEE Computer Society Press, Los Alamitos (2002)
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-Verlag, Heidelberg (2004)
Gurfinkel, A., Chechik, M., Devereux, B.: Temporal logic query checking: A tool for model exploration. IEEE Transactions on Software Engineering 29(10), 898–914 (2003)
Gurfinkel, A., Devereux, B., Chechik, M.: Model exploration with temporal logic query checking. In: Proceedings of the 10th ACMSIGSOFT Symposium on Foundations of Software Engineering (FSE), pp. 139–148. ACM Press, New York (2002)
Hornus, S., Schnoebelen, P.: On solving temporal logic queries. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 163–177. Springer-Verlag, Heidelberg (2002)
Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 82–98. Springer, Heidelberg (1999)
Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. International Journal on Software Tools for Technology Transfer (STTT) 4(2), 224–233 (2003)
Amir Pnueli. 9th International Conference on Computer Aided Verification (CAV), Question from the audience, cited from [4] (1997)
Samer, M.: PhD thesis, Vienna University of Technology. preparation
Samer, M.: Temporal logic queries in model checking. Master’s thesis, Vienna University of Technology (May 2002)
Samer, M., Veith, H.: Validity of CTL queries revisited. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 470–483. Springer, Heidelberg (2003)
Samer, M., Veith, H.: A syntactic characterization of distributive LTL queries. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1099–1110. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Samer, M., Veith, H. (2004). Parameterized Vacuity. In: Hu, A.J., Martin, A.K. (eds) Formal Methods in Computer-Aided Design. FMCAD 2004. Lecture Notes in Computer Science, vol 3312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30494-4_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-30494-4_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23738-9
Online ISBN: 978-3-540-30494-4
eBook Packages: Springer Book Archive