Generalized Strong Preservation by Abstract Interpretation

Title: Generalized Strong Preservation by Abstract Interpretation

Abstract: This research article explores the concept of abstract interpretation and its application to abstract model checking. It discusses the concept of strong preservation, which is highly desirable in model checking as it allows for drawing conclusions from negative answers on the abstract side. The paper introduces the concept of generalized strong preservation, which is applicable to abstract interpretation-based models. It also presents a method for minimally refining an abstract model to make it strongly preserving for a specific language. The paper concludes with a discussion on the relationship between behavioral equivalences and abstract interpretation, and how they can be characterized as completeness properties and refinement algorithms.

Main Research Question: How can abstract interpretation be used to design more general abstract models that are strongly preserving for a specific language?

Methodology: The study uses the standard abstract interpretation approach, which involves defining abstract domains and semantics based on concrete semantic domains. The paper focuses on generic (temporal) languages L of state formulae, which are inductively generated by given sets of atomic propositions and operators. The paper introduces the concept of generalized strong preservation, which is applicable to abstract interpretation-based models.

Results: The research shows that strong preservation can be generalized from standard abstract models to abstract interpretation-based models. It also presents a method for minimally refining an abstract model to make it strongly preserving for a specific language.

Implications: The findings of this research have significant implications for the field of abstract model checking. The ability to design more general abstract models that are strongly preserving for a specific language can lead to more accurate and efficient model checking. Additionally, the paper's characterization of behavioral equivalences as completeness properties and refinement algorithms provides a new perspective on these concepts and their applications.

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