Abstract
In POPL’00, Cousot and Cousot showed that the classical state-based model checking of a very general temporal language called \( \mu \curvearrowleft \star \)-calculus is an incomplete abstract interpretation of its trace-based semantics. In ESOP’01, Ranzato showed that the least refinement of the state-based model checking semantics of the \( \mu \curvearrowleft \star \)-calculus which is complete w.r.t. its trace-based semantics exists, and it is essentially the trace-based semantics itself. The analogous problem in the opposite direction is solved by the present paper. First, relatively to any incomplete temporal connective of the \( \mu \curvearrowleft \star \)-calculus, we characterize the structure of the models, i.e. transition systems, for which the state-based model checking is trace-complete. On this basis, we prove that the unique abstraction of the state-based model checking semantics of the \( \mu \curvearrowleft \star \)-calculus (actually, of any fragment allowing conjunctions) which is complete w.r.t. the trace-based semantics is the straightforward semantics carrying no information at all. The following consequence can be drawn: there is no way to either refine or abstract sets of states in order to get a model checking algorithm for (any fragment allowing conjunctions of) the \( \mu \curvearrowleft \star \)-calculus which is trace-complete.
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
T. Ball, A. Podelski, and S.K. Rajamani. Relative Completeness of Abstraction Refinement for Software Model Checking. In Proc. of TACAS’02, LNCS 2280, pp. 158–172, Springer, 2002.
C.H. Bennett. Logical reversibility of computation. IBM J. Research Dev., 21:905–940, 1981.
J. Chomicki. Temporal query languages: A survey. In Proc. 1st Int. Conf. on Temporal Logic, LNAI 827, pp. 506–534, Springer, 1994.
J. Chomicki, D. Toman, and M.H. Böhlen. Quering ATSQL databases with temporal logic. A CM Trans. Database Syst., 26(2):145–1178, 2001.
E.M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. A CM Trans. Program. Lang. Syst., 19(5):1512–1542, 1994.
E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Proc. CAV’00, LNCS 1855, pp. 154–169, Springer, 2000.
E.M. Clarke, O. Grumberg, and D. Peled. Model checking, The MIT Press, 1999.
J. Clifford, A. Croker, and A. Tuzhilin. On completeness of historical relational query languages. A CM Trans. Database Syst., 19(1):64–116, 1994.
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. ACM POPL’77, pp. 238–252. ACM Press, 1977.
P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proc. ACM POPL’79, pp. 269–282. ACM Press, 1979.
P. Cousot and R. Cousot. Temporal abstract interpretation. In Proc. ACM POPL’00, pp. 12–25. ACM Press, 2000.
D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. A CM Trans. Program. Lang. Syst., 19(2):253–291, 1997.
R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretations complete. J. A CM, 47(2):361–416, 2000.
R. Giacobazzi and E. Quintarelli. Incompleteness, counterexamples and refinements in abstract model checking. In Proc. SAS’01, LNCS 2126, pp. 356–373, Springer, 2001.
C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst. Des., 6:1–36, 1995.
M. Müller-Olm, D. Schmidt, and B. Steffen. Model checking: A tutorial introduction. In Proc. SAS’99, LNCS 1694, pp. 330–354. Springer, 1999.
F. Ranzato. On the completeness of model checking. In Proc. ESOP’01, LNCS 2028, pp. 137–154, Springer, 2001.
A.P. Sistla and O. Wolfson. Temporal triggers in active databases. IEEE Trans. Knowl. Data. Eng., 7(3):471–486, 1995.
A.U. Tansel. Adding time dimension to relational model and extending relational algebra. Information Systems, 11(4):343–355, 1986.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giacobazzi, R., Ranzato, F. (2002). States vs. Traces in Model Checking by Abstract Interpretation. In: Hermenegildo, M.V., Puebla, G. (eds) Static Analysis. SAS 2002. Lecture Notes in Computer Science, vol 2477. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45789-5_32
Download citation
DOI: https://doi.org/10.1007/3-540-45789-5_32
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44235-6
Online ISBN: 978-3-540-45789-3
eBook Packages: Springer Book Archive