Skip to main content
SpringerLink
Log in

Optimization-Based Verification and Stability Characterization of Piecewise Affine and Hybrid Systems

  • Conference paper
  • First Online:
Hybrid Systems: Computation and Control (HSCC 2000)

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

Included in the following conference series:

Abstract

In this paper, we formulate the problem of characterizing the stability of a piecewise affine (PWA) system as a verification problem. The basic idea is to take the whole IRn as the set of initial conditions, and check that all the trajectories go to the origin. More precisely, we test for semi-global stability by restricting the set of initial conditions to an (arbitrarily large) bounded set X(0), and label as “asymptotically stable in T steps” the trajectories that enter an invariant set around the origin within a finite time T, or as “unstable in T steps” the trajectories which enter a set X inst of (very large) states. Subsets of X(0) leading to none of the two previous cases are labeled as “non-classifiable in T steps”. The domain of asymptotical stability in T steps is a subset of the domain of attraction of an equilibrium point, and has the practical meaning of collecting the initial conditions from which the settling time to a specified set around the origin is smaller than T. In addition, it can be computed algorithmically in finite time. Such an algorithm requires the computation of reach sets, in a similar fashion as what has been proposed for verification of hybrid systems. In this paper we present a substantial extension of the verification algorithm presented in [6] for stability characterization of PWA systems, based on linear and mixed-integer linear programming. As a result, given a set of initial conditions we are able to determine its partition into subsets of trajectories which are asymptotically stable, or unstable, or non-classifiable in T steps.

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. R. Alur, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In A.P. Ravn R.L. Grossman, A. Nerode and H. Rischel, editors, Hybrid Systems, volume 736 of Lecture Notes in Computer Science, pages 209–229. Springer Verlag, 1993.

    Google Scholar 

  2. A. Asarin, O. Maler, and A. Pnueli. On the analysis of dynamical systems having piecewise-constant derivatives. Theoretical Computer Science, 138:35–65, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  3. A. Balluchi, M. Di Benedetto, C. Pinello, C. Rossi, and A. Sangiovanni-Vincentelli. Hybrid control for automotive engine management: the cut-off case. In T.A. Henzinger and S. Sastry, editors, Hybrid Systems: Computation and Control, volume 1386 of Lecture Notes in Computer Science, pages 13–32. Springer Verlag, 1998.

    Google Scholar 

  4. A. Bemporad, G. Ferrari-Trecate, and M. Morari. Observability and controllability of piecewise affine and hybrid systems. IEEE Trans. Automatic Control, to appear. http://control.ethz.ch/.

  5. A. Bemporad and M. Morari. Control of systems integrating logic, dynamics, and constraints. Automatica, 35(3):407–427, March 1999.

    Article  MATH  MathSciNet  Google Scholar 

  6. A. Bemporad and M. Morari. Verification of hybrid systems via mathematical programming. In F.W. Vaandrager and J.H. van Schuppen, editors, Hybrid Systems: Computation and Control, volume 1569 of Lecture Notes in Computer Science, pages 31–45. Springer Verlag, 1999.

    Chapter  Google Scholar 

  7. A. Bemporad, M. Morari, V. Dua, and E. N. Pistikopoulos. The explicit linear quadratic regulator for constrained systems. Technical Report AUT99-16, Automatic Control Lab, ETH Zürich, Switzerland, 1999.

    Google Scholar 

  8. A. Bemporad and F.D. Torrisi. Inner and outer approximation of polytopes using hyper-rectangles. Technical Report AUT00-02, Automatic Control Lab, ETH Zurich, 2000.

    Google Scholar 

  9. V.D. Blondel and J.N. Tsitsiklis. Complexity of stability and controllability of elementary hybrid systems. Automatica, 35:479–489, March 1999.

    Article  MATH  MathSciNet  Google Scholar 

  10. M. S. Branicky. Studies in hybrid systems: modeling, analysis, and control. PhD thesis, LIDS-TH 2304, Massachusetts Institute of Technology, Cambridge, MA, 1995.

    Google Scholar 

  11. M. S. Branicky. Multiple Lyapunov functions and other analysis tools for switched and hybrid systems. IEEE Trans. Automatic Control, 43(4):475–482, April 1998.

    Article  MATH  MathSciNet  Google Scholar 

  12. K. Fukuda. cdd/cdd+ Reference Manual. Institute for operations Research ETH-Zentrum, ETH-Zentrum, CH-8092 Zurich, Switzerland, 0.61 (cdd) 0.75 (cdd+) edition, December 1997.

    Google Scholar 

  13. E.G. Gilbert and I. Kolmanovsky. Maximal output admissible sets for discrete-time systems with disturbance inputs. In Proc. American Contr. Conf., pages 2000–2005, 1995.

    Google Scholar 

  14. E.G. Gilbert and K. Tin Tan. Linear systems with state and control constraints: the theory and applications of maximal output admissible sets. IEEE Trans. Automatic Control, 36(9):1008–1020, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  15. 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 

  16. M. Johannson and A. Rantzer. Computation of piece-wise quadratic Lyapunov functions for hybrid systems. IEEE Trans. Automatic Control, 43(4):555–559, 1998.

    Article  Google Scholar 

  17. M. Kantner. Robust stability of piecewise linear discrete time systems. In Proc. American Contr. Conf., pages 1241–1245, Evanston, IL, USA, 1997.

    Google Scholar 

  18. Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Integration graphs: a class of decidable hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems, volume 736 of Lecture Notes in Computer Science, pages 179–208. Springer Verlag, 1993.

    Google Scholar 

  19. S. Kowalewski, O. Stursberg, M. Fritz, H. Graf, I. Hoffmann, J. Preußig, M. Remelhe, S. Simon, and H. Treseler. A case study in tool-aided analysis of discretely controlled continuos systems: the two tanks problem. In Hybrid Systems V, volume 1567 of Lecture Notes in Computer Science, pages 163–185. Springer-Verlag, 1999.

    Chapter  Google Scholar 

  20. D. Liberzon and A.S. Morse. Basic problems in stability and design of switched systems. IEEE Control Systems Magazine, 19(5):59–70, October 1999.

    Article  Google Scholar 

  21. J. Lygeros, D.N. Godbole, and S. Sastry. A game theoretic approach to hybrid system design. In R. Alur and T. Henzinger, editors, Hybrid Systems III, volume 1066 of Lecture Notes in Computer Science, pages 1–12. Springer Verlag, 1996.

    Chapter  Google Scholar 

  22. J. Lygeros, C. Tomlin, and S. Sastry. Controllers for reachability specifications for hybrid systems. Automatica, 35(3):349–370, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  23. R. Raman and I. E. Grossmann. Relation between milp modeling and logical inference for chemical process synthesis. Computers Chem. Engng., 15(2):73–84, 1991.

    Article  Google Scholar 

  24. E. Sontag. From linear to nonlinear: Some complexity comparisons. In Proc. 34th IEEE Conf. on Decision and Control, pages 2916–2920, 1995.

    Google Scholar 

  25. E. D. Sontag. Nonlinear regulation: The piecewise linear approach. IEEE Trans. Automatic Control, 26(2):346–358, April 1981.

    Article  MATH  MathSciNet  Google Scholar 

  26. E.D. Sontag. Interconnected automata and linear systems: A theoretical framework in discrete-time. In R. Alur, T.A. Henzinger, and E.D. Sontag, editors, Hybrid Systems III-Verification and Control, number 1066 in Lecture Notes in Computer Science, pages 436–448. Springer-Verlag, 1996.

    Google Scholar 

  27. M.L. Tyler and M. Morari. Propositional logic in control and monitoring problems. Automatica, 35(4):565–582, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  28. V. I. Utkin. Variable structure systems with sliding modes. IEEE Trans. Automatic Control, 22(2):212–222, April 1977.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Automatic Control Laboratory, Swiss Federal Institute of Technology, ETH Zentrum - ETL I24.2, CH 8092, Zürich, Switzerland

    Alberto Bemporad, Fabio Danilo Torrisi & Manfred Morari

Authors
  1. Alberto Bemporad
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fabio Danilo Torrisi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Manfred Morari
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA, 02139, USA

    Nancy Lynch

  2. Department of Electrical and Computer Engineering, Carnegie Mellon University, Pittsburgh, PA, 15235, USA

    Bruce H. Krogh

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bemporad, A., Torrisi, F.D., Morari, M. (2000). Optimization-Based Verification and Stability Characterization of Piecewise Affine and Hybrid Systems. In: Lynch, N., Krogh, B.H. (eds) Hybrid Systems: Computation and Control. HSCC 2000. Lecture Notes in Computer Science, vol 1790. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46430-1_8

Download citation

  • DOI: https://doi.org/10.1007/3-540-46430-1_8

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67259-3

  • Online ISBN: 978-3-540-46430-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation