Abstract
Model-checking gained wide popularity for analyzing software and hardware systems. However, even when the desired property holds, the property or the model may still require fixing. For example, a property ϕ: “on all paths, a request is followed by an acknowledgment”, may hold because no requests have been generated. Vacuity detection has been proposed to address the above problem. This technique is able to determine that the above property ϕ is satisfied vacuously in systems where requests are never sent. Recent work in this area enabled the computation of interesting witnesses for the satisfaction of properties (in our case, those that satisfy ϕ and contain a request) and vacuity detection with respect to subformulas with single and multiple subformula occurrences.
Often, the answer “vacuous” or “not vacuous”, provided by existing techniques, is insufficient. Instead, we want to identify all subformulas of a given CTL formula that cause its vacuity, or better, identify all maximal such subformulas. Further, these subformulas may be mutually vacuous. In this paper, we propose a framework for identifying a variety of degrees of vacuity, including mutual vacuity between different subformulas. We also cast vacuity detection as a multi-valued model-checking problem.
Chapter PDF
Similar content being viewed by others
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)
Beaty, D., Bryant, R.: Formally Verifying a Microprocessor Using a Simulation Methodology. In: Proceedings of DAC 1994, 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, Springer, Heidelberg (1997)
Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient Detection of Vacuity in Temporal Model Checking. FMSD 18(2), 141–163 (2001)
Birkhoff, G.: Lattice Theory, 3rd edn. Americal Mathematical Society (1967)
Bruns, G., Godefroid, P.: Model Checking Partial State Spaces with 3-Valued Temporal Logics. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274–287. Springer, Heidelberg (1999)
Bruns, G., Godefroid, P.: Temporal Logic Query-Checking. In: LICS 2001, June 2001, pp. 409–417 (2001)
Bruns, G., Godefroid, P.: Model Checking with Multi-Valued Logics. Tech. Memorandum ITD-03-44535H, Bell Labs (May 2003)
Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-Valued Symbolic Model-Checking. ACM Trans. on Soft. Eng. and Method. (2003) (in press)
Chechik, M., Devereux, B., Easterbrook, S., Lai, A., Petrovykh, V.: Efficient Multiple-Valued Model-Checking Using Lattice Representations. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 451–465. Springer, Heidelberg (2001)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Trans. on Prog. Lang. and Sys. 8(2), 244–263 (1986)
Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order (1990)
Dong, Y., Sarna-Starosta, B., Ramakrishnan, C.R., Smolka, S.A.: Vacuity Checking in the Modal Mu-Calculus. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 147–162. Springer, Heidelberg (2002)
Gurfinkel, A.: Multi-Valued Symbolic Model-Checking: Fairness, Counter-Examples, Running Time. Master’s thesis, University of Toronto (October 2002)
Gurfinkel, A., Chechik, M.: Generating Counterexamples for Multi-Valued Model-Checking. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, Springer, Heidelberg (2003)
Gurfinkel, A., Chechik, M.: Multi-Valued Model-Checking via Classical Model-Checking. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 266–280. Springer, Heidelberg (2003)
Gurfinkel, A., Chechik, M., Devereux, B.: Temporal Logic Query Checking: A Tool for Model Exploration. IEEE Tran. on Soft. Eng. 29(10), 898–914 (2003)
Huth, M., Jagadeesan, R., Schmidt, D.A.: Modal Transition Systems: A Foundation for Three-Valued Program Analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 155–169. Springer, Heidelberg (2001)
Kleene, S.C.: Introduction to Metamathematics. Van Nostrand, New York (1952)
Kozen, D.: Results on Propositional μ-calculus. Theor. Comp. Sci. 27, 334–354 (1983)
Kupferman, O.: Augmenting Branching Temporal Logics with Existential Quantification over Atomic Propositions. J. Logic and Computation 7, 1–14 (1997)
Kupferman, O., Vardi, M.: 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.: Vacuity Detection in Temporal Model Checking. STTT 4(2), 224–233 (2003)
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)
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
Gurfinkel, A., Chechik, M. (2004). How Vacuous Is Vacuous?. In: Jensen, K., Podelski, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2004. Lecture Notes in Computer Science, vol 2988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24730-2_34
Download citation
DOI: https://doi.org/10.1007/978-3-540-24730-2_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21299-7
Online ISBN: 978-3-540-24730-2
eBook Packages: Springer Book Archive