Generalized Strong Preservation by Abstract Interpretation

DOI10.1093/LOGCOM/EXL035zbMATH Open1120.68074arXivcs/0401016OpenAlexW2069150132MaRDI QIDQ3437262FDOQ3437262

Authors: Francesco Tapparo, Francesco Ranzato 

Publication date: 14 May 2007

Published in: Journal Of Logic And Computation (Search for Journal in Brave)

Abstract: Standard abstract model checking relies on abstract Kripke structures which approximate concrete models by gluing together indistinguishable states, namely by a partition of the concrete state space. Strong preservation for a specification language L encodes the equivalence of concrete and abstract model checking of formulas in L. We show how abstract interpretation can be used to design abstract models that are more general than abstract Kripke structures. Accordingly, strong preservation is generalized to abstract interpretation-based models and precisely related to the concept of completeness in abstract interpretation. The problem of minimally refining an abstract model in order to make it strongly preserving for some language L can be formulated as a minimal domain refinement in abstract interpretation in order to get completeness w.r.t. the logical/temporal operators of L. It turns out that this refined strongly preserving abstract model always exists and can be characterized as a greatest fixed point. As a consequence, some well-known behavioural equivalences, like bisimulation, simulation and stuttering, and their corresponding partition refinement algorithms can be elegantly characterized in abstract interpretation as completeness properties and refinements.

Full work available at URL: https://arxiv.org/abs/cs/0401016

Recommendations

• Programming Languages and Systems
• scientific article; zbMATH DE number 1948410
• Verification, Model Checking, and Abstract Interpretation
• Tools and Algorithms for the Construction and Analysis of Systems
• scientific article; zbMATH DE number 2110619

zbMATH Keywords

abstract interpretationcompletenessrefinementbehavioural equivalenceabstract model checkingstrong preservation

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (20)

• Deriving Bisimulations by Simplifying Partitions
• Title not available (Why is that?)
• Conservativity of nested relational calculi with internal generic functions
• Preservation of weak SAI's under increasing transformations with applications
• Code obfuscation against abstraction refinement attacks
• An abstract interpretation framework for genotype elimination algorithms
• Tools and Algorithms for the Construction and Analysis of Systems
• Refining and compressing abstract model checking
• Generalizing the Paige-Tarjan algorithm by abstract interpretation
• Generalizing simulation to abstract domains
• Complete abstractions and subclassical modal logics
• An efficient simulation algorithm based on abstract interpretation
• Probabilistic bisimulation and simulation algorithms by abstract interpretation
• Programming Languages and Systems
• Smaller Abstractions for ∀CTL* without Next
• Expressiveness and completeness in abstraction
• Correctness kernels of abstract interpretations
• More Precise Partition Abstractions
• Verification, Model Checking, and Abstract Interpretation
• Bisimulation and simulation algorithms on probabilistic transition systems by abstract interpretation

This page was built for publication: Generalized Strong Preservation by Abstract Interpretation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3437262)