Skip to main content
SpringerLink
Log in

Template-Based Unbounded Time Verification of Affine Hybrid Automata

  • Conference paper
Programming Languages and Systems (APLAS 2011)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7078))

Included in the following conference series:

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

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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)

    Google Scholar 

  2. 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)

    Chapter  Google Scholar 

  3. Alur, R., Dang, T., Ivancic, F.: Counter-example guided predicate abstraction of hybrid systems. Theoretical Computer Science (TCS) 354(2), 250–271 (2006)

    Article  MATH  Google Scholar 

  4. Asarin, E., Dang, T., Girard, A.: Hybridization methods for the analysis of nonlinear systems. Acta Inf. 43(7), 451–476 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  5. 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)

    Article  MathSciNet  MATH  Google Scholar 

  6. 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)

    Chapter  Google Scholar 

  7. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)

    Google Scholar 

  8. Dang, T., Gawlitza, T.M.: Template-based unbounded time verification of affine hybrid automata. Technical report, VERIMAG, Grenoble, France (2011)

    Google Scholar 

  9. Gaubert, S., Goubault, E., Taly, A., Zennou, S.: Static analysis by policy iteration on relational domains. In: Nicola [17]

    Google Scholar 

  10. 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)

    Chapter  Google Scholar 

  11. Gawlitza, T., Seidl, H.: Precise fixpoint computation through strategy iteration. In: Nicola [17]

    Google Scholar 

  12. 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)

    Chapter  Google Scholar 

  13. 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)

    Chapter  Google Scholar 

  14. 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)

    Chapter  Google Scholar 

  15. Gawlitza, T.M., Seidl, H.: Solving systems of rational equations through strategy iteration. TOPLAS (accepted, to appear)

    Google Scholar 

  16. Jurdzinski, M.: Deciding the winner in parity games is in up ∩ co-up. Inf. Process. Lett. 68(3), 119–124 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  17. De Nicola, R. (ed.): ESOP 2007. LNCS, vol. 4421, pp. 157–172. Springer, Heidelberg (2007)

    Book  Google Scholar 

  18. 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)

    Chapter  Google Scholar 

  19. 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)

    Chapter  Google Scholar 

  20. 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)

    Chapter  Google Scholar 

  21. Tarski, A.: A lattice-theoretical fixpoint theorem and its appications. Pac. J. Math. 5, 285–309 (1955)

    Article  MATH  Google Scholar 

  22. 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)

    Chapter  Google Scholar 

  23. 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)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Verimag, France

    Thao Dang & Thomas Martin Gawlitza

  2. University of Sydney, Australia

    Thomas Martin Gawlitza

Authors
  1. Thao Dang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas Martin Gawlitza
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Oxford, Parks Road, OX1 3QD, Oxford, UK

    Hongseok Yang

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation