 The finite model property offers a basis for a sub-procedure (SP2) that consists in enumerating one by one the finite models of PDL and testing whether one of them satisfies the formula. (For all formulas A and for all finite models M, it is easy to test if M sat A by applying the definition of V(A).)  Thus, if A is satisfiable, it must eventually find a model M such that M sat A, and answer “yes” when it does. Symmetrically to the first sub-procedure (SP1), if the formula A is not satisfiable, then (SP2) will never find a model satisfying it, it will run forever, and one could not be sure about it at any time. 