By Abstract Interpretation

Title: by Abstract Interpretation

Abstract: This research article explores the relationship between abstract interpretation and abstract model checking, with a particular focus on strong preservation. The authors propose a method for minimally refining abstract models to make them strongly preserving for a given temporal specification language. They establish a precise correspondence between complete abstract interpretations and strongly preserving abstract models, proving that the problem of minimally refining an abstract model can be formulated as a minimal domain refinement in abstract interpretation. The authors also show that some well-known behavioral equivalences, like bisimulation, simulation, and stuttering equivalence, can be elegantly characterized in abstract interpretation as completeness properties.

Main Research Question: How can we develop a method for minimally refining abstract models to make them strongly preserving for a given temporal specification language?

Methodology: The authors use abstract interpretation as a framework for abstract model checking. They propose a method for refining abstract models by considering them as abstract domains in the lattice of abstract domains related to the concrete semantic domain. They define a partitioning of the concrete state space into abstract domains that correspond to some partition of the state space. They also introduce the concept of a partitioning abstract model, which is an abstract model that corresponds to a partition of the state space.

Results: The authors show that state partitions are particular abstract domains in the lattice of abstract domains related to the concrete semantic domain. They establish a precise correspondence between complete abstract interpretations and strongly preserving abstract models. They also prove that the problem of minimally refining an abstract model can be formulated as a minimal domain refinement in abstract interpretation. Furthermore, they show that some well-known behavioral equivalences can be elegantly characterized in abstract interpretation as completeness properties.

Implications: The results of this research have significant implications for the field of abstract model checking. The proposed method for minimally refining abstract models to make them strongly preserving for a given temporal specification language can be applied to develop more efficient and accurate abstract models. The characterization of behavioral equivalences as completeness properties in abstract interpretation provides a new perspective on these concepts and may lead to further advancements in the field.

Link to Article: https://arxiv.org/abs/0401016v2 Authors: arXiv ID: 0401016v2