Abstract
We redevelop and extend Dams’s results on over- and under-approximation with higher-order Galois connections:
(1) We show how Galois connections are generated from U-GLB-L-LUB-closed binary relations, and we apply them to lower and upper powerset constructions, which are weaker forms of powerdomains appropriate for abstraction studies.
(2) We use the powerset types within a family of logical relations, show when the logical relations preserve U-GLB-L-LUB-closure, and show that simulation is a logical relation. We use the logical relations to rebuild Dams’s most-precise simulations, revealing the inner structure of over- and under-approximation.
(3) We extract validation and refutation logics from the logical relations, state their resemblance to Hennessey-Milner logic and description logic, and obtain easy proofs of soundness and best precision.
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.
Similar content being viewed by others
References
Abramsky, S.: Abstract interpretation, logical relations, and Kan extensions. J. Logic and Computation 1, 5–41 (1990)
Abramsky, S.: Domain theory in logical form. Ann. Pure Appl. Logic 51, 1–77 (1991)
Baader, F., et al.: The Description Logic Handbook. Cambridge Univ. Press, Cambridge (2003)
Backhouse, K., Backhous, R.: Galois connections and logical relations. In: Boiten, E.A., Möller, B. (eds.) MPC 2002. LNCS, vol. 2386, p. 23. Springer, Heidelberg (2002)
Buneman, P., Davidson, S., Watters, A.: A semantics for complex objects and approximate queries. In: 7th ACM Symp. Principles of Database Systems (1988)
Ciocoiu, M.: Ontology-based translation. PhD thesis, University of Maryland (2001)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)
Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Logic and Computation 2, 511–547 (1992)
Cousot, P., Cousot, R.: Higher-order abstract interpretation. In: Proceedings IEEE Int. Conf. Computer Lang (1994)
Dams, D.: Abstract interpretation and partition refinement for model checking. PhD thesis, Technische Universiteit Eindhoven, The Netherlands (1996)
Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Trans. Prog. Lang. Systems 19, 253–291 (1997)
Giacobazzi, R., Quintarelli, E.: Incompleteness, counterexamples, and refinements in abstract model checking. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 356–373. Springer, Heidelberg (2001)
Gunter, C.: The mixed power domain. Theoretical Comp. Sci. 103, 311–334 (1992)
Hartmanis, J., Stearns, R.E.: Pair algebras and their application to automata theory. J. Information and Control 7, 485–507 (1964)
Heckmann, R.: Power domain constructions. PhD thesis, Univ. Saarbrücken (1990)
Heckmann, R.: Set domains. In: Proc. European Symp. Programming. LNCS, pp. 177–196. Springer, Heidelberg (1990)
Hennessy, M.C.B., Milner, R.: Algebraic laws for non-determinism and concurrency. JACM 32, 137–161 (1985)
Huth, M., Jagadeesan, R., Schmidt, D.A.: Modal transition systems: a foundation for three-valued program analysis. In: Proc. European Symp. Programming. LNCS, pp. 155–169. Springer, Heidelberg (2001)
Huth, M., Jagadeesan, R., Schmidt, D.A.: A domain equation for refinement of partial systems. Mathematical Structures in Computer Science (2004) (in press)
Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science 27, 333–354 (1983)
Larsen, K.G.: Modal Specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232–246. Springer, Heidelberg (1990)
Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for verification of concurrent systems. Formal Methods in System Design 6, 1–36 (1995)
Mycroft, A., Jones, N.D.: A relational framework for abstract interpretation. In: Ganzinger, H., Jones, N.D. (eds.) Programs as Data Objects. LNCS, vol. 217, pp. 156–171. Springer, Heidelberg (1986)
Nielson, F.: Two-level semantics and abstract interpretation. Theoretical Comp. Sci. 69, 117–242 (1989)
Plotkin, G.: Domains. Lecture notes, Univ. Pisa/Edinburgh (1983)
Ranzato, F., Tapparo, F.: Strong preservation as completeness in abstract interpretation. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 18–32. Springer, Heidelberg (2004)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Proceedings 28th ACM POPL (1999)
Schmidt, D.A.: Structure-preserving binary relations for program abstraction. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 246–266. 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
Schmidt, D.A. (2004). Closed and Logical Relations for Over- and Under-Approximation of Powersets. In: Giacobazzi, R. (eds) Static Analysis. SAS 2004. Lecture Notes in Computer Science, vol 3148. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27864-1_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-27864-1_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22791-5
Online ISBN: 978-3-540-27864-1
eBook Packages: Springer Book Archive