8

C. Bäckström and P. Jonsson

Artiﬁcial Intelligence 302 (2022) 103608

is M↑. It follows that  f

Proof. (1) Assume τ is M↑R↑C↑. Let e1 = (cid:3)s1, t1, (cid:2)1(cid:4) be an arbitrary arc in E1. Since τ is R↑ there is some arc (cid:3)s2, t2, (cid:2)2(cid:4) ∈ E2
such  that  R((cid:2)1, (cid:2)2).  Since  τ is  also  C↑ there  must  be  such  an  arc  where  s2 ∈ f (s1) and  t2 ∈ f (t1),  i.e.  s2 = f (s1) and 
t2 = f (t1) since  f
is a homomorphism. Let e2 = (cid:3)s2, t2, (cid:2)2(cid:4) be an arbitrary arc in 
(2) Assume that τ is M↑R(cid:14)C(cid:14). It follows from (1) that  f
E2. Since τ is R↓ there is some arc (cid:3)s1, t1, (cid:2)1(cid:4) ∈ E1 such that R((cid:2)1, (cid:2)2). Since τ is also C↓ there must be such an arc where 
s1 ∈ f (s2) and t1 ∈ f (t2), i.e. s2 = f (s1) and t2 = f (t1) since  f
is M↑. It follows that  f
is a strong homomorphism, since e2
was chosen arbitrarily.
(4) Immediate from (3) by symmetry. (cid:2)
A-framework-for-analysing-state-abstraction-metho_2022_Artificial-Intelligen