We investigate techniques for automatically generating symbolic approximations to the time solution of a system of differential equations. This is an important primitive operation for the safety analysis of continuous and hybrid systems. In this paper we design a \emph{time elapse operator} that computes a symbolic over-approximation of time solutions to a continous system starting from a given inital region. Our approach is iterative over the cone of functions (drawn from a suitable universe) that are non negative over the initial region. At each stage, we iteratively remove functions from the cone whose Lie derivatives do not lie inside the current iterate. If the iteration converges, the set of states defined by the final iterate is shown to contain all the time successors of the initial region. The convergence of the iteration can be forced using abstract interpretation operations such as widening and narrowing.
In Hybrid Systems: Computation and Control; 9th International Workshop (HSCC 2006), LNCS 3927, pp 537-551, Springer Verlag, 2006.
BibTex, Postscript, PDF. © 2006, Springer Verlag.