The classic method for abstracting temporal properties when realizing abstract model checking is based on defining an abstract satisfiability relation which under-approximates the standard one. As a consequence, satisfiability of universal properties is directly preserved from the abstract model to the concrete one. However, this result may be impractical due to the imprecision and incompleteness with which abstract models are usually constructed. Thus, in the case a model checking tool supporting abstract model checking gives a negative answer, the user must analyze the counter-examples produced to decide whether the property really fails or, on the contrary, the abstract model is too imprecise to obtain a definitive result. We have developed an alternative method for abstracting temporal properties based on the idea of over-approximation. In this paper, we compare these two methods with respect to the satisfiability/refutation of universal/existential properties, proving that they produce complementary results. Finally, we study the conditions which ensure that the method based on over-approximation also produces definitive answers when analyzing universal properties.