Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Hybrid Systems: Computation and Control

HSCC 2003: Hybrid Systems: Computation and Control pp 20–35Cite as

Reachability Analysis of Nonlinear Systems Using Conservative Approximation

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2623))

Abstract

In this paper we present an approach to approximate reachability computation for nonlinear continuous systems. Rather than studying a complex nonlinear system x = g(x), we study an approximating system x = f(x) which is easier to handle. The class of approximating systems we consider in this paper is piecewise linear, obtained by interpolating g over a mesh. In order to be conservative, we add a bounded input in the approximating system to account for the interpolation error. We thus develop a reachability method for systems with input, based on the relation between such systems and the corresponding autonomous systems in terms of reachable sets. This method is then extended to the approximate piecewise linear systems arising in our construction. The final result is a reachability algorithm for nonlinear continuous systems which allows to compute conservative approximations with as great degree of accuracy as desired, and more importantly, it has good convergence rate. If g is a C 2 function, our method is of order 2. Furthermore, the method can be straightforwardly extended to hybrid systems.

Research supported by European IST project “CC - Computation and Control” and CNRS project MathStic ”Squash - Analyse Qualitative des Systèmes Hybrides“.

This is a preview of subscription content, 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   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis and S. Yovine. The Algorithmic Analysis of Hybrid Systems, Theoretical Computer Science 138, 3–34, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  2. H. Anai and V. Weispfenning. Reach Set Computations Using Real Quantifier Elimination, Hybrid Systems: Computation and Control, in M. D. Di Benedetto and A. Sangiovanni-Vincentelli (Eds), 63–75 LNCS 2034, Springer-Verlag, 2001.

    Chapter  Google Scholar 

  3. E. Asarin, T. Dang and A. Girard. Reachability Analysis of Nonlinear Systems using Conservative Approximations, Technical Report IMAG Oct 2002, Grenoble http://www-verimag.imag.fr/~tdang/piecewise.ps.gz.

  4. E. Asarin and T. Dang and O. Maler. d/dt: A tool for Verification of Hybrid Systems, Computer Aided Verification, Springer-Verlag, LNCS, 2002.

    Google Scholar 

  5. M. D. Di Benedetto and A. Sangiovanni-Vincentelli. Hybrid Systems: Computation and Control, LNCS 2034, Springer-Verlag, 2001.

    Book  Google Scholar 

  6. O. Botchkarev and S. Tripakis. Verification of Hybrid Systems with Linear Differential Inclusions Using Ellipsoidal Approximations, Hybrid Systems: Computation and Control, in B. Krogh and N. Lynch (Eds), 73–88 LNCS 1790, Springer-Verlag, 2000.

    Chapter  Google Scholar 

  7. A. Chutinan and B. H. Krogh. Verification of Polyhedral Invariant Hybrid Automata Using Polygonal Flow Pipe Approximations, Hybrid Systems: Computation and Control, in F. Vaandrager and J. van Schuppen (Eds), 76–90 LNCS 1569, Springer-Verlag, 1999.

    Chapter  Google Scholar 

  8. T. Dang and O. Maler. Reachability Analysis via Face Lifting, Hybrid Systems: Computation and Control, in T. A. Henzinger and S. Sastry (Eds), 96–109 LNCS 1386 Springer-Verlag, 1998.

    Google Scholar 

  9. J. Della Dora, A. Maignan, M. Mirica-Ruse, and S. Yovine. Hybrid Computation, Proc. of ISSAC’01, 2001.

    Google Scholar 

  10. J. Dieudonné. Calcul Infinitésimal, Collection Méthodes, Hermann Paris, 1980.

    Google Scholar 

  11. A. Girard. Approximate Solutions of ODEs Using Piecewise Linear Vector Fields, Proc. CASC’02, 2002.

    Google Scholar 

  12. A. Girard. Detection of Event Occurence in Piecewise Linear Hybrid Systems, Proc. RASC’02, December 2002, Nottingham, UK.

    Google Scholar 

  13. M. R. Greenstreet and I. Mitchell. Reachability Analysis Using Polygonal Projections, Hybrid Systems: Computation and Control, in F. Vaandrager and J. van Schuppen (Eds), 76–90 LNCS 1569 Springer-Verlag, 1999.

    Chapter  Google Scholar 

  14. M. Greenstreet and C. Tomlin. Hybrid Systems: Computation and Control, LNCS, Springer-Verlag, 2002.

    MATH  Google Scholar 

  15. L. C. G. J. M. Habets and J. H. van Schuppen. Control of Piecewise-Linear Hybrid Systems on Simplices and Rectangles, Hybrid Systems: Control and Computation, in M. D. Di Benedetto and A. Sangiovanni-Vincentelli (Eds), 261–273 LNCS 2034, Springer-Verlag, 2001.

    Chapter  Google Scholar 

  16. T. A. Henzinger, P.-H. Ho and H. Wong-Toi. HyTech: A Model Checker for Hybrid Systems, Software Tools for Technology Transfer 1, 110–122, 1997.

    Article  MATH  Google Scholar 

  17. T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. Analysis of Nonlinear Hybrid Systems, IEEE Transactions on Automatic Control 43, 540–554, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  18. J. Hubbard and B. West. Differential Equations: A Dynamical Systems Approach, Higher-Dimensional Systems, Texts in Applied Mathematics, 18, Springer Verlag, 1995.

    Google Scholar 

  19. G. Lafferriere, G. Pappas, and S. Yovine. Reachability computation for linear systems, Proc. of the 14th IFAC World Congress, 7–12 E, 1999.

    Google Scholar 

  20. , K. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell, Software Tools for Technology Transfert 1, 1997.

    Google Scholar 

  21. T. H. Marshall. Volume formulae for regular hyperbolic cubes, Conform. Geom. Dyn., 25–28, 1998.

    Google Scholar 

  22. I. Mitchell and C. Tomlin. Level Set Method for Computation in Hybrid Systems, Hybrid Systems: Computation and Control, in B. Krogh and N. Lynch, 311–323 LNCS 1790, Springer-Verlag, 2000.

    Chapter  Google Scholar 

  23. P. Saint-Pierre. Approximation of Viability Kernels and Capture Basin for Hybrid Systems, Proc. of European Control Conference ECC’01, 2776–2783, 2001.

    Google Scholar 

  24. O. Stursberg, S. Kowalewski and S. Engell. On the generation of Timed Approximations for continuous systems, Mathematical and Computer Modelling of Dynamical Systems 6–1, 51-70, 2000.

    Google Scholar 

  25. A. Puri and P. Varaiya. Verification of Hybrid Systems using Abstraction, Hybrid Systems II, in P. Antsaklis, W. Kohn, A. Nerode, and S. Sastry (Eds), LNCS 999, Springer-Verlag, 1995.

    Google Scholar 

  26. S. Yovine. Kronos: A Verification Tool for Real-time Systems, Software Tools for Technology Transfer 1, 123–133, 1997.

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. VERIMAG, 2 avenue de Vignate, 38610, Gières, France

    Eugene Asarin & Thao Dang

  2. LMC-IMAG, 51 rue des Mathématiques, 38041, Grenoble, France

    Antoine Girard

Authors
  1. Eugene Asarin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thao Dang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Antoine Girard
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. CNRS-VERIMAG, 2 avenue de Vignate, 38610, Gières, France

    Oded Maler

  2. Weizmann Institute of Science, Rehovot, 76100, Israel

    Amir Pnueli

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Asarin, E., Dang, T., Girard, A. (2003). Reachability Analysis of Nonlinear Systems Using Conservative Approximation. In: Maler, O., Pnueli, A. (eds) Hybrid Systems: Computation and Control. HSCC 2003. Lecture Notes in Computer Science, vol 2623. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36580-X_5

Download citation

  • DOI: https://doi.org/10.1007/3-540-36580-X_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00913-9

  • Online ISBN: 978-3-540-36580-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation