These operations can be arbitrarily interleaved with each other. The process typically stops when |(cid:9)| = 1 and no more 
shrinking is required to achieve the desired size of the abstract state space. Let G = (cid:3)S, E(cid:4) be an STG in (cid:9) at some point 
during this process. Then S ⊆ T (V
(cid:10) · D) if and only if G is the result of applying at least 
one shrink operation. Let GA = (cid:3)S A , E A(cid:4) be the ﬁnal single STG in (cid:9). Then S A ⊆ T (V · D) and |S A| ≤ N for some predeﬁned 
value N.
Once again, let G = (cid:3)S, E(cid:4) be an STG in (cid:9) at some point during the process. Although S will often contain states deﬁned 
by more than one variable, we may view S itself as the domain of a new single compound variable (which is also how M&S
is usually described in the literature). Hence, the shrink operation is nothing else but method VDA (Deﬁnition 34) where all
A-framework-for-analysing-state-abstraction-metho_2022_Artificial-Intelligen