(1) Assume τ is ABS. Let V C ⊆ V 1 be the set of critical variables. Note that S1 = S2.
Suppose (cid:3)s1, t1, a(cid:4) ∈ E1. Then it must hold that pre(a) ⊆ s1, so we get pre(g(a)) = pre(a)[V C] ⊆ pre(a) ⊆ s1 and, hence, 
(cid:3)s1, t2, g(a)(cid:4) ∈ E2, where t2 = s1 (cid:4) post(g(a)). Since R(a, g(a)) holds by deﬁnition it follows that τ is R↑. Then also suppose 
that R(a, (cid:2)) holds for some (cid:2). By deﬁnition of R, the only possibility is that (cid:2) = g(a), so we already know that (cid:3)s1, t2, g(a)(cid:4) ∈
E2. We get t2 = s1 (cid:4)post(g(a)) = s1 (cid:4)post(a) = t1, and, thus, that (cid:3)s1, t1, g(a)(cid:4) ∈ E2. Since s1 ∈ f (s1) and t1 ∈ f (t1) it follows 
that τ is C↑.
Suppose instead that (cid:3)s2, t2, g(a)(cid:4) ∈ E2. Then pre(g(a)) ⊆ s2, so we get pre(a)[V C] = pre(g(a)) ⊆ s2. Hence, there must be 
some state s1 ∈ S1 such that pre(a) ⊆ s1 and s1[V C] = s2[V C], i.e. s1 ∈ f (s2). Let t1 = s1 (cid:4)post(a). Then (cid:3)s1, t1, a(cid:4) ∈ E1 so τ is
A-framework-for-analysing-state-abstraction-metho_2022_Artificial-Intelligen