The Modal Logic of Abstraction Refinement
Jakob Piribauer, Vinzent Zschuppe
TL;DR
The paper addresses how branching-time CTL properties evolve under abstraction refinement by introducing alethic modalities that express 'there exists a refinement in which' ($\lozenge$) and 'in all refinements' ($\Box$). It defines MLAR as the modal logic of abstraction refinement over three classes: $\mathsf{MLAR}^{\mathit{fin}}_{\mathcal{T}}$, $\mathsf{MLAR}^{\mathit{all}}_{\mathcal{T}}$, and $\mathsf{MLAR}$, grounded on CTL-valuations. The main contributions are precise lower and upper bounds: $\mathsf{S4.2} \subseteq \mathsf{MLAR}^{\mathit{fin}}_{\mathcal{T}}$ (tight for some $\mathcal{T}$), $\mathsf{S4.2.1} \subseteq \mathsf{MLAR}^{\mathit{all}}_{\mathcal{T}}$ (tight for some $\mathcal{T}$), and $\mathsf{MLAR}$ situated between $\mathsf{S4.1}$ and $\mathsf{S4.2.1} \cap \mathsf{S4FPF}$. The authors introduce control statements—pure buttons, pure weak buttons, switches, plus innovations like $\mathbf{B}$-restricted switches and decisions—to prove the bounds, and discuss implications for abstraction-refinement-based verification of CTL properties and the limits of extending refinement concepts to general branching-time logics. The work also connects MLAR bounds to known modal logics and notes PSPACE-completeness for satisfiability checks in these settings.
Abstract
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.