Abstract
The model checking community has proposed numerous definitions of vacuous satisfaction, i.e., formal criteria which tell whether a temporal logic specification holds true on a system model for the intended reason. In this paper we attempt to study the notion of vacuous satisfaction from first principles. We show that despite the apparently vague formulation of the vacuity problem, most proposed notions of vacuity for temporal logic can be cast into a uniform and simple framework, and compare previous approaches to vacuity detection from this unified point of view.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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
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)
Barwise, J., van Benthem, J.: Interpolation, preservation, and pebble games. Journal of Symbolic Logic 64(2), 881–903 (1999)
Beatty, D.L., Bryant, R.E.: Formally verifying a microprocessor using a simulation methodology. In: DAC 1994. Proc. 31st Annual ACM IEEE Design Automation Conference, 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 (FMSD) 18(2), 141–163 (2001)
Ben-David, S., Fisman, D., Ruah, S.: Temporal antecedent failure: Refining vacuity. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 492–506. Springer, Heidelberg (2007)
Bruns, G., Godefroid, P.: Temporal logic query checking. In: LICS 2001. Proc. 16th Annual IEEE Symposium on Logic in Computer Science, pp. 409–417. IEEE Computer Society Press, Los Alamitos (2001)
Bustan, D., Flaisher, A., Grumberg, O., Kupferman, O., Vardi, M.Y.: Regular vacuity. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 191–206. Springer, Heidelberg (2005)
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, Heidelberg (2003)
Chockler, H., Strichman, O.: Easier and more informative vacuity checks. In: MEMOCODE 2007, pp. 189–198. IEEE Computer Society Press, Los Alamitos (2007)
Clarke, E.M., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking. In: LICS 2002. Proc. 17th Annual IEEE Symposium on Logic in Computer Science, pp. 19–29. IEEE Computer Society Press, Los Alamitos (2002)
Clarke, E.M., Veith, H.: Counterexamples revisited: Principles, algorithms, applications. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 208–224. Springer, Heidelberg (2004)
D’Agostino, G., Hollenberg, M.: Logical questions concerning the μ-calculus: Interpolation, Lyndon and Loś-Tarski. Journal of Symbolic Logic 65(1), 310–332 (2000)
Dong, Y., Sarna-Starosta, B., Ramakrishnan, C., Smolka, S.A.: Vacuity checking in the modal mu-calculus. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, Springer, Heidelberg (2002)
French, T.: Decidability of quantified propositional branching time logics. In: Stumptner, M., Corbett, D.R., Brooks, M. (eds.) AI 2001: Advances in Artificial Intelligence. LNCS (LNAI), vol. 2256, pp. 165–176. Springer, Heidelberg (2001)
Groce, A., Kroening, D.: Making the most of BMC counterexamples. Electronic Notes in Theoretical Computer Science (ENTCS) 119(2), 67–81 (2005)
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)
Gurfinkel, A., Chechik, M., Devereux, B.: Temporal logic query checking: A tool for model exploration. IEEE Transactions on Software Engineering (TSE) 29(10), 898–914 (2003)
Gurfinkel, A., Devereux, B., Chechik, M.: Model exploration with temporal logic query checking. In: Proc. 10th International Symposium on the Foundations of Software Engineering (FSE-10), pp. 139–148. ACM Press, New York (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–96. 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)
Maksimova, L.: Absence of interpolation and of Beth’s property in temporal logics with “the next” operation. Siberian Mathematical Journal 32(6), 109–113 (1991)
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)
Pnueli, A.: 9th International Conference on Computer-Aided Verification. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, Springer, Heidelberg (1997) (cited from [5])
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)
Samer, M.: Reasoning about Specifications in Model Checking. PhD thesis, Vienna University of Technology (2004)
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.: Parameterized vacuity. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 322–336. Springer, Heidelberg (2004)
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)
Samer, M., Veith, H.: Deterministic CTL query solving. In: TIME 2005, pp. 156–165. IEEE Computer Society Press, Los Alamitos (2005)
Simmonds, J., Davies, J., Gurfinkel, A., Chechik, M.: Exploiting resolution proofs to speed up LTL vacuity detection for BMC. In: FMCAD 2007. Proc. 7th International Conference on Formal Methods in Computer-Aided Design, IEEE Computer Society Press, Los Alamitos (to appear, 2007)
Visser, A.: Bisimulations, model descriptions and propositional quantifiers. Logic Group Preprint Series, Nbr. 161, Dept. Philosophy, Utrecht University (1996)
Wittgenstein, L.: On Certainty. In: Anscombe, G.E.M., von Wright, G.H. (eds.) Harper and Row (1968)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Samer, M., Veith, H. (2007). On the Notion of Vacuous Truth. In: Dershowitz, N., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2007. Lecture Notes in Computer Science(), vol 4790. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75560-9_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-75560-9_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75558-6
Online ISBN: 978-3-540-75560-9
eBook Packages: Computer ScienceComputer Science (R0)