Fixed Point Iteration for Computing the Time Elapse OperatorSriram 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
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.
We instantiate our technique to linear hybrid systems with
piecewise-affine dynamics to compute polyhedral approximations to
the time successors. Using our prototype implementation
TimePass, we demonstrate the performance of our technique
on benchmark examples.
|
| Hybrid Systems: Computation and Control (HSCC 2006), To Appear. |
| © 2005, Springer Verlag |