The concept of spurious states [45,92] is more general and declarative, and it uses state reﬁnement. A spurious state is 
a state that is reachable in the abstract graph, but that does not correspond to any reachable state in the ground graph. 
For a state s in the ground graph, the corresponding set of spurious states is S(s) = R2( f (s)) \ f (R1(s)). Spurious states 
are undesirable in an abstract solution since this solution cannot then be reﬁned into a ground solution. A similar notion is 
used in model-checking, where a spurious state is a counter-example that can be reached in the abstract model, but not in 
the ground model [19,40]. A necessary and suﬃcient condition for avoiding spurious states is that an abstraction satisﬁes 
the downward path preserving (DPP) property [92]. The DPP property guarantees that S(s) = ∅ for all s. It was deﬁned for 
strong homomorphic abstractions using the following two conditions:
1. R2( f (s)) ⊆ f (R1(s)) for all s ∈ S1,
A-framework-for-analysing-state-abstraction-metho_2022_Artificial-Intelligen