Artiﬁcial Intelligence 302 (2022) 103608

1
2
3
4

1
2
3
4

1
2
3
4
5
6
7
8
9

function LPath(s,t)
choose a state path σ = t0, t1, . . . , tk such that t0 ∈ f (s) and tk ∈ f (t)
if there is no such σ then fail
else return Reﬁne(t0,tk)

function WSPath(s,t)
choose a state path σ = t0, t1, . . . , tk such that t0 ∈ f (s) and tk ∈ f (t)
if there is no such σ then fail
else return Reﬁne(t0, t1, . . . , tk)

function Reﬁne(t0, t1, . . . , tk)
choose s0 ∈ f (t0)
if k = 0 then return s0
else
σ2 = Reﬁne(t1, . . . , tk)
s1 = ﬁrst(σ2)
choose a state path σ1 from s0 to s1
if there is no such σ1 then fail
else return the concatenation σ1; σ2

Fig. 3. Algorithms for path reﬁnement. The choose statements are non-deterministic and serve as backtrack points.
A-framework-for-analysing-state-abstraction-metho_2022_Artificial-Intelligen