Abstract
Over-approximating the set of all reachable states of a given system is an important task for the verification of safety properties. Such an unbounded time verification is in particular challenging for hybrid systems. We recently developed an algorithm that over-approximates the set of all reachable states of a given affine hybrid automata by performing linear template-based abstract interpretation [4]. In this article we extend the previous results by adding uncertainty to the model of affine hybrid automata. Uncertainty can be used for abstracting the behavior of non-linear hybrid systems. We adapt our techniques to this model and show that, w.r.t. given linear templates, the abstract reachability problem is still in coNP by reducing abstract reachability for affine hybrid automata with uncertainty to abstract reachability for affine programs (affine hybrid automata where only discrete transitions are allowed). We thus provide a new connection between a continuous time model and a purely discrete model.
This work was partially funded by the ANR project VEDECY.
VERIMAG is a joint laboratory of CNRS, Université Joseph Fourier and Grenoble INP.
This is a preview of subscription content, log in via an institution to check access.
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
Asarin, E., Bournez, O., Dang, T., Maler, O.: Approximate reachability analysis of piecewise linear dynamical systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 20–31. Springer, Heidelberg (2000)
Chutinan, A., Krogh, B.: Computational techniques for hybrid system verification. IEEE Trans. on Automatic Control (48), 64–75 (2003)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)
Dang, T., Gawlitza, T.M.: Template-based unbounded time verification of affine hybrid automata. Technical report, VERIMAG (2011)
Frehse, G., Guernic, C.L., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: Spaceex: Scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011)
Gawlitza, T.M.: Strategieverbesserungsalgorithmen für exakte Programmanalysen, Ph.D. Thesis. Dr. Hut Verlag, München, Munich, Germany (October 2009)
Girard, A., Guernic, C.L., Maler, O.: Efficient computation of reachable sets of linear time-invariant systems with inputs. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 257–271. Springer, Heidelberg (2006)
Kurzhanskiy, A., Varaiya, P.: Ellipsoidal techniques for reachability analysis of discrete-time linear systems. IEEE Trans. Automatic Control (52), 26–38 (2007)
Kvasnica, M., Grieder, P., Baotić, M., Morari, M.: Multi-parametric toolbox (mpt). In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 448–462. Springer, Heidelberg (2004)
Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477–492. Springer, Heidelberg (2004)
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25–41. Springer, Heidelberg (2005)
Sankaranarayanan, S., Dang, T., Ivančić, F.: A policy iteration technique for time elapse over template polyhedra. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 654–657. Springer, Heidelberg (2008)
Tarski, A.: A lattice-theoretical fixpoint theorem and its appications. Pac. J. Math. 5, 285–309 (1955)
Tiwari, A., Khanna, G.: Nonlinear systems: Approximating reach sets. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 600–614. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dang, T., Gawlitza, T.M. (2011). Discretizing Affine Hybrid Automata with Uncertainty. In: Bultan, T., Hsiung, PA. (eds) Automated Technology for Verification and Analysis. ATVA 2011. Lecture Notes in Computer Science, vol 6996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24372-1_36
Download citation
DOI: https://doi.org/10.1007/978-3-642-24372-1_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24371-4
Online ISBN: 978-3-642-24372-1
eBook Packages: Computer ScienceComputer Science (R0)