 With a carefully chosen set FL(A) that depends on a PDL formula A (the so-called Fischer-Ladner closure of the set of sub-formulas of A), a filtration of an LTS M yields a finite filtrate M′, such that A is satisfiable at a world u in M if and only if it is satisfiable in the equivalence class containing u in the filtrate. (See Fischer and Ladner [1979].) 