We present an efficient algorithm for computing discrete abstractions of
arbitrary memory span for nonlinear discrete-time and sampled systems, in
which, apart from possibly numerically integrating ordinary differential
equations, the only nontrivial operation to be performed repeatedly is to
distinguish empty from non-empty convex polyhedra. We also provide sufficient
conditions for the convexity of attainable sets, which is an important
requirement for the correctness of the method we propose.