, (cid:2)

)

(cid:10)

(cid:10)

Combining Theorems 21 and 22 gives the following corollary.

Corollary 23. (1) M↓R↓C↓ ⇒ PS↓,  (2) M↑R↑C↑ ⇒ PS↑.

Combining this corollary with Theorem 14 yields that all homomorphic abstractions have property PS↑.
These  results  will  be  used  later,  in  Sec. 7,  where  we  will  analyse  a  number  of  abstraction  methods,  deriving  some 

properties explicitly and then infer other properties using the results above.
5.  SAS+ and implicit state-transition graphs
A-framework-for-analysing-state-abstraction-metho_2022_Artificial-Intelligen