{\shortrightarrow}^{\exists\exists}\rangle$ defined over a state partition $P\in \operatorname{Part}(\Sigma)$ and a finite abstract path $\pi =
\langle B_1,...,B_n\rangle$ in ${\mathcal{A}}$, where each $B_i$ is a block of $P$. Typically, this is a path counterexample to the validity of a temporal formula that has been given as output by a model checker (for simplicity we do not consider here loop path counterexamples). The set of concrete paths that are abstracted to $\pi$ are defined as follows: $$\operatorname{paths}(\pi) {\triangleq}\{\tuple{s_1,...,s_n}\in \Sigma^n~|~\forall i\in [1,n]. s_i\in B_i \;\&\; \forall i\in [1,n). s_i {\shortrightarrow}s_{i+1}\}.$$ The abstract path $\pi$ is *spurious* when it represents no real concrete path, i.e., when $\operatorname{paths}(\pi)=\varnothing$. The sequence of sets of states $\operatorname{sp}(\pi) = 
\langle S_1,...,S_n\rangle$ is inductively defined as follows: $S_1 {\triangleq}B_1$; $S_{i+1} {\triangleq}\operatorname{post}(S_i)\cap B_{i+1}$. As shown in [@cgjlv03], it turns out that $\pi$ is spurious iff there exists a least $k\in [1,n-1]$ such that $S_{k+1}=\varnothing$. In such a case, the partition $P$ is refined by splitting the block $B_{k}$. The three following sets partition the states of the block $B_{k}$:

dead-end states: $B_{k}^{\text{dead}} {\triangleq}S_{k}\neq \varnothing$

bad states: $B_{k}^{\text{bad}} {\triangleq}B_{k} \cap \operatorname{pre}(B_{k+1}) \neq \varnothing$

irrelevant states: $B_{k}^{\text{irr}} {\triangleq}B_{k}\smallsetminus
(B_{k}^{\text{dead}} \cup B_{k}^{\text{bad}})$

The split of the block $B_{k}$ must separate dead-end states from 