[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Hybridization methods for the analysis of nonlinear systems

  • Original Article
  • Published:
Acta Informatica Aims and scope Submit manuscript

Abstract

In this article, we describe some recent results on the hybridization methods for the analysis of nonlinear systems. The main idea of our hybridization approach is to apply the hybrid systems methodology as a systematic approximation method. More concretely, we partition the state space of a complex system into regions that only intersect on their boundaries, and then approximate its dynamics in each region by a simpler one. Then, the resulting hybrid system, which we call a hybridization, is used to yield approximate analysis results for the original system. We also prove important properties of the hybridization, and propose two effective hybridization construction methods, which allow approximating the original nonlinear system with a good convergence rate.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Alur R., Courcoubetis C., Halbwachs N., Henzinger T.A., Ho P.-H., Nicollin X., Olivero A., Sifakis J. and Yovine S. (1995). The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(1): 3–34

    Article  MATH  Google Scholar 

  2. Alur R., Dang T. and Ivancic F. (2006). Counter-example guided predicate abstraction of hybrid systems. Theor. Comput. Sci. 354(2): 250–271

    Article  MATH  MathSciNet  Google Scholar 

  3. Alur R. and Dill D.L. (1994). A theory of timed automata. Theor. Comput. Sci. 126(2): 183–235

    Article  MATH  MathSciNet  Google Scholar 

  4. Alur R., Henzinger T.A., Lafferriere G. and Pappas G. (2000). Discrete abstractions of hybrid systems. Proc. IEEE 88(2): 971–984

    Article  Google Scholar 

  5. Anai, H., Weispfenning, V.: Reach set computations using real quantifier elimination. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.) Hybrid Systems: Computation and Control, vol. 2034 in LNCS, pp. 63–75. Springer, Heidelberg (2001)

  6. Asarin, E., Bournez, O., Dang, T., Maler, O.: Approximate reachability analysis of piecewise-linear dynamical systems. In: Krogh, B.H., Lynch, N. (eds.) Hybrid Systems: Computation and Control, vol. 1790 in LNCS, pp. 20–31. Springer, Heidelberg (2000)

  7. Asarin, E., Dang, T., Maler, O.: d/dt: A tool for verification of hybrid systems. In: Ed Brinksma, Kim Guldstrand Larsen (eds.) Computer Aided Verification, vol. 2404 in LNCS, pp. 365–370. Springer, Heidelberg (2002)

  8. Asarin, E., Dang, T.: Abstraction by projection and application to multi-affine systems. In: Alur, R., Pappas, G.J. (eds) Hybrid Systems: Control and Computation, vol. 2993 LNCS, pp. 32–47. Springer, Heidelberg (2004)

  9. Asarin, E., Dang, T., Girard, A.: Reachability analysis of nonlinear systems using conservative approximations. In: Maler, O., Pnueli, A. (eds.) Hybrid Systems: Computation and Control, vol. 2623 in LNCS, pp. 20–35. Springer, Heidelberg (2003)

  10. Asarin E., Maler O. and Pnueli A. (1995). Reachability analysis of dynamical systems having piecewise-constant derivatives. Theor. Comput. Sci. 138(1): 35–66

    Article  MATH  MathSciNet  Google Scholar 

  11. Aubin J.-P., Lygeros J., Quincampoix M., Sastry S. and Seube N. (2002). Impulse differential inclusions: a viability approach to hybrid systems. IEEE Trans. Autom. Control 47(1): 2–20

    Article  MathSciNet  Google Scholar 

  12. Barringer, H., Kuiper, R., Pnueli, A.: A really abstract concurrent model and its temporal logic. In: POPL’86: Principles of Programming Languages, pp. 173–183 (1986)

  13. Botchkarev, O., Tripakis, S.: Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations. In: Krogh B., Lynch N. (eds.), Hybrid Systems: Computation and Control, vol. 1790 in LNCS, pp. 73–88. Springer, Heidelberg (2000)

  14. Branicky M.S., Borkar V.S. and Mitter S.K. (1998). A unified framework for hybrid control: model and optimal control theory. IEEE Trans. on Automatic Control 43(1): 31–45

    Article  MATH  MathSciNet  Google Scholar 

  15. Chutinan, A., Krogh, B.H.: Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) Hybrid systems: Computation and Control, vol. 1569 in LNCS, pp. 76–90. Springer, Heidelberg (1999)

  16. Clarke, E., Fehnker, A., Han, Z., Krogh, B., Ouaknine, J., Stursberg, O., Theobald, M.: Abstraction and counterexample-guided refinement in model checking of hybrid systems. Int. J. Foundations of Comput. Sci. 14(4), 583–604 (2003)

    Google Scholar 

  17. Dang, T.: Approximate reachability computation for polynomial systems. In: Hespanha, J., Tiwari, A. (eds.) Hybrid Systems: Control and Computation, vol. 3927 in LNCS, pp. 138–152. Springer, Heidelberg (2006)

  18. Dang, T., Donze, A., Maler, O.: Verification of analog and mixed-signal circuits using hybrid systems techniques. In: Hu, A., Martin, A. (eds.) Formal Methods for Computer Aided Design, vol. 3312 in LNCS, pp. 21–36. Springer, Heidelberg (2004)

  19. Dang, T., Maler, O.: Reachability Analysis via Face Lifting. In: Henzinger, T.A., Sastry, S. (eds.), Hybrid Systems: Computation and Control, vol. 1386 in LNCS, pp. 96–109. Springer, Heidelberg (1998)

  20. Davoren, J.M., Coulthard, V., Markey, N., Moor, T.: Non-deterministic temporal logics for general flow systems. In: Alur, R., G.J. Pappas, G.J. (eds.) Hybrid Systems: Computation and Control HSCC04, vol. 2993 in LNCS, pp. 280–295. Springer, Heidelberg (2004)

  21. Decarlo R.A., Branicky M.S., Pettersson S. and Lennartson B. (2000). Perspectives and results on the stability and stabilizability of hybrid systems. Proc. the IEEE 88(7): 1069–1082

    Article  Google Scholar 

  22. Della Dora, J., Maignan, A., Mirica-Ruse, M., Yovine, S.: Hybrid computation. In: Proceedings International Symposium on Symbolic and Algebraic Computation ISSAC’01 (2001)

  23. Dieudonné J. (1968). Calcul Infinitésimal. Collection Méthodes. Hermann, Paris

    MATH  Google Scholar 

  24. Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 995–1072. Elsevier, Amsterdam (1990)

  25. Frehse, G.: PHAVer: Algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) Hybrid Systems: Computation and Control, vol. 3414 in LNCS, pp. 258–273. Springer, Heidelberg (2005)

  26. Girard, A.: Approximate solutions of ODEs using piecewise linear vector fields. In: Proceedings of the Int. Workshop on Computer Algebra in Scientific Computing CASC’02 (2002)

  27. Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Morari, M., Thiele, L. (eds.) Hybrid Systems: Computation and Control, vol. 3414 in LNCS, pp. 291–305. Springer, Heidelberg (2005)

  28. Greenstreet, M.R., Mitchell, I.: Reachability analysis using polygonal projections. In: Vaandrager, F., van Schuppen, J.H. (eds.) Hybrid Systems: Computation and Control, vol. 1569 in LNCS, pp. 76–90. Springer, Heidelberg (1999)

  29. Habets, L.C.G.J.M., van Schuppen, J.H.: Control of piecewise-linear hybrid systems on simplices and rectangles. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.) Hybrid systems: Computation and Control, vol.. 2034 LNCS, pp. 261–273. Springer, Heidelberg (2001)

  30. Hämmerlin G. and Karl-Heinz Hoffmann K.-H. (1991). Numerical Mathematics. Springer, Heidelberg

    Google Scholar 

  31. Hartong, W., Hedrich, L., Barke, E.: On discrete modelling and model checking for nonlinear analog systems. In: Ed Brinksma, Kim Guldstrand Larsen (eds.) Computer Aided Verification, vol. 2404 in LNCS, pp. 401–413. Springer, Heidelberg (2002)

  32. Henzinger T.A., Ho P.-H. and Wong-Toi H. (1997). HyTech: A model checker for hybrid systems. Softw. Tools Technol. Transf. 1(1–2): 110–122

    Article  MATH  Google Scholar 

  33. Henzinger T.A., Kopke P.W., Puri A. and Varaiya P. (1998). What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1): 94–124

    Article  MATH  MathSciNet  Google Scholar 

  34. Hubbard, J., West, B.: Differential equations: a dynamical system approach, part 2: higher dimensional systems. Texts in Applied Mathematics, 18 Springer, Heidelberg (1995)

  35. Johansson M. and Rantzer A. (1998). Computation of piecewise quadratic Lyapunov functions for hybrid systems. IEEE Trans. Autom. Control 43(4): 555–559

    Article  MATH  MathSciNet  Google Scholar 

  36. Kloetzer, M., Belta, C.: Reachability analysis of multi-affine systems. In: Hespanha, J., Tiwari, A. (eds.) Hybrid Systems: Computation and Control, vol. 3927 in LNCS, pp. 348–362. Springer, Heidelberg (2006)

  37. Kratz, F., Sokolsky, O., Pappas, G.J., Lee, I.: R-Charon : a modeling language for reconfigurable hybrid systems. In: Hespanha, J., Tiwari, A. (eds.) Hybrid Systems: Computation and Control, vol. 3927 in LNCS, pp. 392–406. Springer, Heidelberg (2006)

  38. Kuhn H.W. (1960). Some combinatorial lemmas in topology. IBM J. Res. Dev. 4(5): 518–524

    Article  MATH  MathSciNet  Google Scholar 

  39. Kurzhanski, A., Varaiya, P.: Ellipsoidal techniques for reachability analysis. In: Krogh, B., Lynch, N. (eds.) Hybrid Systems: Computation and Control, vol. 1790 in LNCS, pp. 202–214. Springer, Heidelberg (2000)

  40. Lafferriere G., Pappas G. and Yovine S. (2001). Symbolic reachability computation of families of linear vector fields. J. Symbolic Comput. 32(3): 231–253

    Article  MATH  MathSciNet  Google Scholar 

  41. Larsen K., Pettersson P. and Yi W. (1997). Uppaal in a nutshell. Soft. Tools Technol. Transf. 1(1–2): 134–152

    Article  MATH  Google Scholar 

  42. Liberzon D. (2003). Switching in systems and control. Volume in series Systems and Control: Foundations and Applications. Birkhauser, Boston

    MATH  Google Scholar 

  43. Manna Z. and Pnueli A. (1991). The temporal logic of reactive and concurrent systems: specification. Springer, New York

    MATH  Google Scholar 

  44. Mitchell, I., Templeton, J.A.: A toolbox of Hamilton-Jacobi solvers for analysis of nondeterministic continuous and hybrid Systems. In: Morari, M., Thiele, L. (eds.) Hybrid Systems: Computation and Control, vol. 3414 in LNCS, pp. 480–494. Springer, Heidelberg (2005)

  45. Kvasnica, M., Grieder, P., Baoti, M., Morari, M.: Multi-Parametric Toolbox (MPT). In: Alur, R., Pappas, G.J. (eds.) Hybrid Systems: Computation and Control, vol. 2993 in LNCS, pp. 448–462. Springer, Heidelberg (2004)

  46. Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, A., Pappas, G. (eds.) Hybrid Systems: Computation and Control, vol. 2993 LNCS, pp. 477–492. Springer, Heidelberg (2004)

  47. Prajna, S., Papachristodoulou, A.: Analysis of switched and hybrid systems - beyond piecewise quadratic methods. In: Proceedings of the American Control Conference ACC (2003)

  48. Puri, A., Varaiya, P.: Verification of sybrid systems using abstraction. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) Hybrid Systems II, vol. 999 in LNCS, pp. 359–369, Springer, Heidelberg (1995)

  49. Rondepierre, A., Dumas, J.G.: Algorithms for hybrid optimal control. Technical report IMAG-ccsd-00004191, arXiv math.OC/0502172 (2005)

  50. Saint-Pierre, P.: Approximation of Viability Kernels and Capture Basin for Hybrid Systems. In: Proceedings of European Control Conference ECC’01, pp. 2776–2783 (2001)

  51. Sastry S. (1999). Nonlinear systems: analysis, stability and control. Springer, Heidelberg

    MATH  Google Scholar 

  52. Stuart A.M. and Humphries A.R. (1996). Dynamical systems and numerical analysis. Cambridge Monographs on Applied and Computational Mathematics. Cambridge University Press, Cambridge

    MATH  Google Scholar 

  53. Stursberg, O., Kowalewski, S.: Approximating switched continuous systems by rectangular automata. In: Proceedings European Control Conference ECC, (1999)

  54. Tabuada, P., Pappas, G.: Model-checking LTL over controllable linear systems is decidable, In: Maler, O., Pnueli, A. (eds.) Hybrid Systems: Computation and Control, vol. 2623 LNCS, pp. 498–513, Springer, Heidelberg (2003)

  55. Tiwari, A., Khanna, G.: Series of abstractions for hybrid automata. In: Tomlin, C., Greenstreet, M.R. (eds.) Hybrid Systems: Computation and Control, vol. 2289 LNCS, pp. 465–478, (2002)

  56. Tiwari, A., Khanna, A.: Nonlinear systems: approximating reach sets. In: Alur, R., Pappas, G.J. (eds.) Hybrid Systems: Computation and Control, vol. 2993 LNCS, pp. 600–614. Springer, Heidelberg (2004)

  57. Tomlin C., Mitchell I., Bayen A. and Oishi M. (2003). Computational techniques for the verification of hybrid systems. Proc. IEEE 91(7): 986–1001

    Article  Google Scholar 

  58. Torrisi F.D. and Bemporad A. (2004). HYSDEL - A tool for generating computational hybrid models. IEEE Trans. Control Syst. Technol. 12(2): 235–249

    Article  MathSciNet  Google Scholar 

  59. Van der Schaft, A.J., Schumacher, J.M.: An introduction to hybrid dynamical systems. Lect. Notes in Control and Information Sciences, Vol 251. Springer, London, (2000)

  60. Yovine, S.: Kronos: A verification tool for real-time systems. Soft. Tools Technol. Trans. 1(1–2), 123–133 (1997)

Download references

Author information

Authors and Affiliations

  1. Université Paris 7, LIAFA, 2 pl. Jussieu, 75251, Paris, Cedex 5, France

    Eugene Asarin

  2. VERIMAG, 2 ave. de Vignate, 38610, Gieres, France

    Thao Dang

  3. Université Joseph Fourier, LMC, B.P. 53, 38041, Grenoble Cedex 9, 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

Corresponding author

Correspondence to Thao Dang.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Asarin, E., Dang, T. & Girard, A. Hybridization methods for the analysis of nonlinear systems. Acta Informatica 43, 451–476 (2007). https://doi.org/10.1007/s00236-006-0035-7

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00236-006-0035-7

Keywords

Search

Navigation