(0 ≤ i ≤ n) and si ∈ R1(si−1) for all i (1 ≤ i ≤ n).
(cid:10) ∈ f (ti).

(cid:10) ∈ f (tn) such that s

(cid:10) ∈ R1(s).

s

The corresponding cases of upwards reﬁnability are deﬁned symmetrically.

These  concepts  are  illustrated  in  Fig. 2.  In  all  cases,  a  path  σ = t0, t1, t2, t3 in  the  abstract  graph  G2 is  reﬁned  into 
a corresponding path in the ground graph  G1. Curly arrows denote paths, i.e. they may consist of several arcs and pass 
through states not shown in the ﬁgure.
Loose reﬁnement only requires that there is a path corresponding to σ in the ground graph, i.e. there must be a path 
from some state in  f (t0) = {s00, s01} to some state in  f (t3) = {s30, s31}. This is satisﬁed by the path from s00 to s31, which is 
thus a loose reﬁnement of σ . The intermediate states t1 and t2 are ignored in the reﬁnement. Weak reﬁnement additionally 

11

C. Bäckström and P. Jonsson

Artiﬁcial Intelligence 302 (2022) 103608

1
2
3
4

1
2
3
4

1
2
3
4
5
6
7
8
9
A-framework-for-analysing-state-abstraction-metho_2022_Artificial-Intelligen