We redevelop and extend Dams's results on over- and underapproximation with higher-order Galois connections: (1) We show how Galois connections are generated from U-GLB-L-LUBclosed 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 overand 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. © Springer-Verlag 2004.
CITATION STYLE
Schmidt, D. A. (2004). Closed and logical relations for overand under-approximation of powersets. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3148, 22–37. https://doi.org/10.1007/978-3-540-27864-1_5
Mendeley helps you to discover research relevant for your work.