{\circ}f {\circ}\mu$. Hence, the correctness kernel of $\mu$ for $f$ does not exist. Observe that $\mu {\circ}f=f$ is clearly not continuous and therefore this example is consistent with Theorem \[kernel\].

Correctness Kernels in Abstract Model Checking
==============================================

Following the approach by Ranzato and Tapparo [@rt07], partitions of a state space $\Sigma$ can be viewed as particular abstract domains of the concrete domain $\wp(\Sigma)$. Let $\operatorname{Part}(\Sigma)$ denote the set of partitions of $\Sigma$. Given a partition $P\in \operatorname{Part}(\Sigma)$, the corresponding set of (possibly empty) unions of blocks of $P$, namely $\wp(P)$, is viewed as an abstract domain of $\wp(\Sigma)$ by means of the following Galois insertion $(\alpha_P, \wp(\Sigma)_\subseteq , \wp(P)_\subseteq, \gamma_P)$: $$\alpha_P(S) {\triangleq}\{B\in P~|~ B\cap S \neq \varnothing\}  
\text{~~and~~}
\gamma_P(\mathcal{B}) {\triangleq}\cup_{B\in \mathcal{B}} B.$$ Hence, the abstraction $\alpha_P(S)$ provides the minimal over-approximation of a set $S$ of states through blocks of $P$.

Consider a transition system $\mathcal{S} 
= \langle \Sigma, {\shortrightarrow}\rangle$ and a corresponding abstract transition system ${\mathcal{A}}=
\langle P, {\shortrightarrow}^\sharp \rangle$ defined over a state partition $P\in \operatorname{Part}(\Sigma)$.[^1] Fixpoint-based verification of a temporal specification on the abstract model ${\mathcal{A}}$ relies on the computation of least/greatest fixpoints of operators which are defined using Boolean connectives (union, intersection, complementation) on abstract states and 