## Fixed Point Iteration for Computing the Time Elapse Operator

*Sriram Sankaranarayanan,
Henny Sipma,
Zohar Manna.
*
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.

© Henny Sipma /
sipma@cs.stanford.edu
Last modified: Nov 19 14:40:50 PDT 2004