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.
展开▼
