Abstract
Computing over-approximations of all possible time trajectories is an important task in the analysis of hybrid systems. Sankaranarayanan et al. [20] suggested to approximate the set of reachable states using template polyhedra. In the present paper, we use a max-strategy improvement algorithm for computing an abstract semantics for affine hybrid automata that is based on template polyhedra and safely over-approximates the concrete semantics. Based on our formulation, we show that the corresponding abstract reachability problem is in co-NP. Moreover, we obtain a polynomial-time algorithm for the time elapse operation over template polyhedra.
This work was partially funded by the ANR project VEDECY.
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
Adjé, A., Gaubert, S., Goubault, E.: Computing the smallest fixed point of nonexpansive mappings arising in game theory and static analysis of programs. In: MTNS (2008)
Adjé, A., Gaubert, S., Goubault, E.: Coupling Policy Iteration with Semi-Definite Relaxation to Compute Accurate Numerical Invariants in Static Analysis. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 23–42. Springer, Heidelberg (2010)
Alur, R., Dang, T., Ivancic, F.: Counter-example guided predicate abstraction of hybrid systems. Theoretical Computer Science (TCS) 354(2), 250–271 (2006)
Asarin, E., Dang, T., Girard, A.: Hybridization methods for the analysis of nonlinear systems. Acta Inf. 43(7), 451–476 (2007)
Clarke, E.M., Fehnker, A., Han, Z., Krogh, B.H., Ouaknine, J., Stursberg, O., Theobald, M.: Abstraction and counterexample-guided refinement in model checking of hybrid systems. Int. J. Found. Comput. Sci. 14(4), 583–604 (2003)
Costan, A., Gaubert, S., Goubault, É., Martel, M., Putot, S.: A Policy Iteration Algorithm for Computing Fixed Points in Static Analysis of Programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 462–475. Springer, Heidelberg (2005)
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, Grenoble, France (2011)
Gaubert, S., Goubault, E., Taly, A., Zennou, S.: Static analysis by policy iteration on relational domains. In: Nicola [17]
Gawlitza, T., Seidl, H.: Precise Relational Invariants through Strategy Iteration. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 23–40. Springer, Heidelberg (2007)
Gawlitza, T., Seidl, H.: Precise fixpoint computation through strategy iteration. In: Nicola [17]
Gawlitza, T., Seidl, H.: Precise Interval Analysis vs. Parity Games. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 342–357. Springer, Heidelberg (2008)
Gawlitza, T.M., Monniaux, D.: Improving Strategies via SMT Solving. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 236–255. Springer, Heidelberg (2011)
Gawlitza, T.M., Seidl, H.: Computing Relaxed Abstract Semantics w.r.t. Quadratic Zones Precisely. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 271–286. Springer, Heidelberg (2010)
Gawlitza, T.M., Seidl, H.: Solving systems of rational equations through strategy iteration. TOPLAS (accepted, to appear)
Jurdzinski, M.: Deciding the winner in parity games is in up ∩ co-up. Inf. Process. Lett. 68(3), 119–124 (1998)
De Nicola, R. (ed.): ESOP 2007. LNCS, vol. 4421, pp. 157–172. Springer, Heidelberg (2007)
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.: Series of Abstractions for Hybrid Automata. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 465–478. Springer, Heidelberg (2002)
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). Template-Based Unbounded Time Verification of Affine Hybrid Automata. In: Yang, H. (eds) Programming Languages and Systems. APLAS 2011. Lecture Notes in Computer Science, vol 7078. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25318-8_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-25318-8_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25317-1
Online ISBN: 978-3-642-25318-8
eBook Packages: Computer ScienceComputer Science (R0)