abstract successor/predecessor functions $\operatorname{post}^\sharp$/$\operatorname{pre}^\sharp$ on the abstract transition system $\langle P,{\shortrightarrow}^\sharp\rangle$. The key point here is that successor/predecessor functions are defined as best correct approximations on the abstract domain $P$ of the corresponding concrete successor/predecessor functions. In standard abstract model checking [@bk08; @cgl94; @cgp99], the abstract transition relation is defined as the existential/existential relation ${\shortrightarrow}^{\exists\exists}$ between blocks of $P$, namely: $$\begin{gathered}
B {\shortrightarrow}^{\exists\exists} C \text{~~~~iff~~~~} \exists x\in B.\exists y\in C.\: x
{\shortrightarrow}y\\
\operatorname{post}^{\exists\exists}(B) {\triangleq}\{C\in P~|~B {\shortrightarrow}^{\exists\exists} C \};~~~~~~
\operatorname{pre}^{\exists\exists}(C) {\triangleq}\{B\in P~|~B {\shortrightarrow}^{\exists\exists} C\}.\end{gathered}$$ As shown in [@rt07], it turns out that $\operatorname{pre}^{\exists\exists}$ and $\operatorname{post}^{\exists\exists}$ are the best correct approximations of, respectively, $\operatorname{pre}$ and $\operatorname{post}$ functions on the above abstraction $(\alpha_P, \wp(\Sigma)_\subseteq , \wp(P)_\subseteq, \gamma_P)$. In fact, for a block $C\in P$, we have that $$\alpha_P(\operatorname{pre}(\gamma_P(C))) = \{B\in P~|~ B\cap \operatorname{pre}(C)\neq \varnothing\} 
= \operatorname{pre}^{\exists\exists}(C)$$ and an analogous equation holds for $\operatorname{post}$. We thus have that $\operatorname{pre}^{\exists\exists} = \alpha_P \circ \operatorname{pre}\circ \gamma_P$ and $\operatorname{post}^{\exists\exists} = \alpha_P \circ \operatorname{post}\circ \gamma_P$.

This abstract interpretation-based framework allows us to apply correctness kernels in the context of abstract model checking. The abstract transition system ${\mathcal{A}}= \langle P, {\shortrightarrow}^{\exists\exists} \rangle$ is viewed as an abstract interpretation defined by the abstract domain $(\alpha_P, \wp(\Sigma)_\subseteq ,$ $\wp(P)_\subseteq, \gamma_P)$ and 