Iterative abstraction refinement techniques are one of the most prominent paradigms for the analysis and verification of systems with large or infinite state spaces. This paper investigates the changes of truth values of system properties expressible in computation tree logic (CTL) when abstractions of transition systems are refined. To this end, the paper utilizes modal logic by defining alethic modalities expressing possibility and necessity on top of CTL: The modal operator $\lozenge$ is interpreted as "there is a refinement, in which ..." and $\Box$ is interpreted as "in all refinements, ...". Upper and lower bounds for the resulting modal logics of abstraction refinement are provided for three scenarios: 1) when considering all finite abstractions of a transition system, 2) when considering all abstractions of a transition system, and 3) when considering the class of all transition systems. Furthermore, to prove these results, generic techniques to obtain upper bounds of modal logics using novel types of so-called control statements are developed.

翻译：迭代抽象精化技术是分析和验证具有大规模或无限状态空间系统的最主要范式之一。本文研究了当迁移系统的抽象被精化时，计算树逻辑（CTL）可表达的系统属性真值的变化。为此，本文利用模态逻辑，在CTL之上定义了表达可能性与必然性的真势模态：模态算子 $\lozenge$ 被解释为“存在一种精化，在其中……”，而 $\Box$ 被解释为“在所有精化中，……”。针对三种场景，给出了所得抽象精化模态逻辑的上界与下界：1）考虑迁移系统的所有有限抽象时；2）考虑迁移系统的所有抽象时；3）考虑所有迁移系统构成的类时。此外，为了证明这些结果，本文发展了使用新型所谓控制语句来获取模态逻辑上界的通用技术。