In this work, we continue our study on discrete abstractions of dynamical

systems. To this end, we use a family of partitioning functions to generate an

abstraction. The intersection of sub-level sets of the partitioning functions

defines cells, which are regarded as discrete objects. The union of cells makes

up the state space of the dynamical systems. Our construction gives rise to a

combinatorial object - a timed automaton. We examine sound and complete

abstractions. An abstraction is said to be sound when the flow of the time

automata covers the flow lines of the dynamical systems. If the dynamics of the

dynamical system and the time automaton are equivalent, the abstraction is

complete.

The commonly accepted paradigm for partitioning functions is that they ought

to be transversal to the studied vector field. We show that there is no

complete partitioning with transversal functions, even for particular dynamical

systems whose critical sets are isolated critical points. Therefore, we allow

the directional derivative along the vector field to be non-positive in this

work. This considerably complicates the abstraction technique. For

understanding dynamical systems, it is vital to study stable and unstable

manifolds and their intersections. These objects appear naturally in this work.

Indeed, we show that for an abstraction to be complete, the set of critical

points of an abstraction function shall contain either the stable or unstable

manifold of the dynamical system.