A Policy Iteration Technique For Time Elapse over Template PolyhedraSriram Sankaranarayanan, Thao Dang, and Franjo Ivancic |
| In this paper, we present a policy iteration technique that computes an over-approximation of the time trajectories of a system using template polyhedra. Such polyhedra are obtained by conjoining a set of inequality templates with varying constant coefficients. Given a set of template expressions, we show the existence of a smallest template polyhedron that is a positive invariant w.r.t to the dynamics of the continuous variables, and hence, an over-approximation the time trajectories. Thus, we derive a time elapse operator for template polyhedra using policy iteration that computes tight over-approximations of the time trajectories. We exploit the result of the policy iteration to improve the precision of Taylor series-based flowpipe construction. Finally, we incorporate our ideas inside a prototype tool for safety verification of affine hybrid systems, with promising results on benchmarks. |
| Draft 2008. (Short paper will appear in HSCC 2008). |
| Due to copyright concerns, I am unable to make this paper available online. I will be glad to provide copies upon personal request. |