Generalized Strong Preservation by Abstract Interpretation
Generalized Strong Preservation by Abstract Interpretation
复制标题
抽象解释的广义强保存
DOI：
10.1093/logcom/exl035
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
Francesco Tapparo
中科院分区：
文献类型：
--
作者：
Francesco Ranzato;Francesco Tapparo
标准的抽象模型检查依赖于抽象Kripke结构，该结构通过粘合不可区分的状态来近似具体模型，即通过划分具体状态空间。规范语言L的强保存性相当于L中公式的具体和抽象模型检验的等价性。我们展示了如何使用抽象解释来设计通用抽象模型，这些模型允许将标准抽象Kripke结构视为特定实例。因此，强保存被推广到基于抽象解释的模型中，并与抽象解释中的完备性概念紧密相关。对抽象模型进行最小细化以使其对某种语言L强保留的问题，可以表述为抽象解释中的最小域细化，以使L的逻辑/时间算子完备。结果表明，这种改进的强保持抽象模型总是存在的，并且可以用最大不动点来表征。因此，一些众所周知的行为等价，如双模拟、模拟和口吃，以及它们相应的分区细化算法，可以在抽象解释中优雅地描述为完备性和细化。
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 amounts to the equivalence of concrete and abstract model checking of formulas in L . We show how abstract interpretation can be used to design generic abstract models that allow to view standard abstract Kripke structures as particular instances. 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.