In this paper we study the relation between the lack of completeness
in abstract interpretation of symbolic trajectory evaluation and the
structure of the counterexample that can be derived from a negative
answer of the symbolic trajectory evaluation algorithm. We
characterize the spuriousness of counterexamples as a loss of
completeness of the underlying domain. We prove how standard
forward/backward completeness refinement provides a systematic way
for refining abstract symbolic trajecoty evaluation in order to gain
completeness for the properties of interest.
