state s3 ∈ f3(s1) such that t3 ∈ R3(s3). By deﬁnition of  f3 there must also be some state s2 ∈ S2 such that s2 ∈ f1(s1) and 
s3 ∈ f2(s2). Then t3 ∈ R3( f2(s2)), so t3 ∈ f (R2(s2)) since τ2 is P↓. That is, there is some t2 ∈ R2(s2) such that t3 ∈ f (t2). It 
follows that t2 ∈ R2( f1(s1)), so t2 ∈ f1(R1(s1)) since τ1 is P↓. Hence, t3 ∈ f2( f1(t1)) = f3(t1) so t3 ∈ f3(R1(s1)). It follows 
that R3( f3(s1)) ⊆ f3(R1(s1)) and, thus, that τ3 is P↓ since s1 was chosen arbitrarily.
PS↓: Analogous to the PW↓ case. (cid:2)
The properties Pk↑ and Pk↓, on the other hand, are not transitive for any ﬁxed k, which is less important since they are 
primarily used as tools for deﬁning other properties.
We  deﬁne  composition  of  metric  transformations  in  the  obvious  way.  Let  G1,  G2 and  G3 be  STGs,  let  τ1 =
(cid:3) f1, R1, w1, w2(cid:4) be a metric transformation from G1 to G2 and let τ2 = (cid:3) f2, R2, w2, w3(cid:4) be a metric transformation from
A-framework-for-analysing-state-abstraction-metho_2022_Artificial-Intelligen