In section 3.3 we have defined a predicate ∞, where ∞(α) means that α can have non-terminating computation. We call LPDL the logic obtained by augmenting PDL with the predicate ∞. Clearly, RPDL is at least as expressive as LPDL; The inductive definition of ∞(α) in the language of RPDL is witness of it. RPDL is in fact strictly more expressive than LPDL. This was shown in Harel and Sherman [1982].  As it can be suspected, both RPDL and LPDL have more expressive power than PDL. It is established by proving that some formulas of RPDL and of LPDL have no equivalent expression in PDL.  The proof involves the technique of filtration which is designed to collapse an LTS to a finite model while leaving invariant the truth or falsity of certain formulas. For some set of PDL formulas X, it consists in grouping into equivalence classes the states of an LTS that satisfy exactly the same formulas in X. The set of equivalence classes of states thus obtained becomes the set of states of the filtrate model, and a transition is built appropriately over them.