Generalized Strong Preservation by Abstract Interpretation

Title: Generalized Strong Preservation by Abstract Interpretation

Abstract: This research article explores the concept of strong preservation in abstract interpretation, a framework used for abstract model checking. It proposes a generalized approach to strong preservation, which is applicable to any abstract model specified by a generic abstract domain, not just state partitions. The study presents a precise correspondence between complete abstract interpretation and strongly preserving abstract model checking, establishing a fix-point solution for the problem of minimally refining abstract model checking to achieve strong preservation. It also characterizes behavioral equivalences used in process algebras like bisimulation and stuttering, and their corresponding partition refinement algorithms in pure abstract interpretation as completeness properties.

Research Question: How can the concept of strong preservation be generalized and applied to any abstract model specified by a generic abstract domain in the abstract interpretation framework?

Methodology: The study uses the abstract interpretation framework, which involves approximating the concrete state semantics of a temporal specification language with an abstract semantics induced by an abstract domain. The methodology involves generalizing the concept of strong preservation for abstract models specified by state partitions to any abstract model specified by a generic abstract domain. This is achieved by generalizing a formulation of strong preservation and establishing a correspondence between complete abstract interpretation and strongly preserving abstract model checking.

Results: The research presents a generalized approach to strong preservation that is applicable to any abstract model specified by a generic abstract domain. It also establishes a precise correspondence between complete abstract interpretation and strongly preserving abstract model checking, and shows that some behavioral equivalences used in process algebras can be characterized in pure abstract interpretation as completeness properties.

Implications: The generalized strong preservation approach has implications for the design of abstract model checking frameworks and tools. It allows for a more flexible and precise approach to strong preservation, which can lead to more accurate and efficient model checking. The characterization of behavioral equivalences as completeness properties in pure abstract interpretation provides a new perspective on these concepts and may lead to new algorithms and techniques in the field of abstract interpretation and model checking.

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