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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Blanchini, F.: Set invariance in control. Automatica 35 11, 1747–1889 (1999)
Gaubert, S., Goubault, E., Taly, A., Zennou, S.: Static analysis by policy iteration on relational domains. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 237–252. Springer, Heidelberg (2007)
Fehnker, A., Ivančić, F.: Benchmarks for hybrid systems verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 326–341. Springer, Heidelberg (2004)
Sankaranarayanan, S., Dang, T., Ivančić, F.: Symbolic model checking of hybrid systems using template polyhedra. In: TACAS (to appear, 2008)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sankaranarayanan, S., Dang, T., Ivančić, F. (2008). A Policy Iteration Technique for Time Elapse over Template Polyhedra. In: Egerstedt, M., Mishra, B. (eds) Hybrid Systems: Computation and Control. HSCC 2008. Lecture Notes in Computer Science, vol 4981. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78929-1_57
Download citation
DOI: https://doi.org/10.1007/978-3-540-78929-1_57
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78928-4
Online ISBN: 978-3-540-78929-1
eBook Packages: Computer ScienceComputer Science (R0)