Lecture Notes in Computer Science, 2008, Volume 4981/2008, 654-657, DOI: 10.1007/978-3-540-78929-1_57

A Policy Iteration Technique for Time Elapse over Template Polyhedra
(Extended Abstract)

Sriram Sankaranarayanan, Thao Dang and Franjo Ivančić

View Related Documents

Abstract

We present a technique to compute over-approximations of the time trajectories of an affine hybrid 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 of the time trajectories. However, the least invariant is hard to compute efficiently. Therefore, we propose a policy iteration technique that iterates over the space of invariant certificates to converge onto a solution that is close to the least solution. We incorporate our ideas in our prototype tool TimePass for safety verification of affine hybrid systems, with promising results on benchmarks.

Fulltext Preview

Image of the first page of the fulltext document