column 3 of Table 1.

Theorem 44. 
(1) ABS ⇒ P1(cid:14),
(4) RRAa ⇒ PS↓,
Proof. Combine Theorem 42 with Theorem 22 and Corollary 23. (cid:2)

(3) VDA ⇒ P1↓PS↑,
(6) DLBS ⇒ PS↓P1↑.

(2) VP ⇒ P1↓PS↑,
(5) RRAb ⇒ PS↓,

We now explicitly derive the remaining reﬁnement properties of the methods, to achieve tight separations. These are 

summarised in column 4 of Table 1.

23

C. Bäckström and P. Jonsson

Artiﬁcial Intelligence 302 (2022) 103608

(cid:10)

(cid:10)

(cid:10) such  that  t

). We further have t

(cid:10) satisﬁes both

(cid:10) ∈ S2 such that t

(cid:10) ∈ f (R1(s0)) since t

(3a) ABS (cid:3) PL↓,
(4b) VP (cid:3) P2↓,
(6) RRAa ⇒ PS↑,
(9) GIDL (cid:3) P1↑,

(2) ABS (cid:3) PS↑,
(4a) VP (cid:3) PL↓,
(5b) VDA (cid:3) P2↓,
(8) GIDL (cid:3) P1↓,
(11) DLBS (cid:3) P↑.

(cid:10) we also have pre(g(ak+1)) ⊆ t
(cid:10) to t, i.e. t ∈ R2(t
A-framework-for-analysing-state-abstraction-metho_2022_Artificial-Intelligen