Advertisement

Algorithmic analysis of nonlinear hybrid systems

  • Thomas A. Henzinger
  • Pei -Hsin Ho
Session 7: Invited Titorial
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)

Abstract

Hybrid systems model discrete programs that are embedded in continuous environments. Model-checking tools are available for the analysis of linear hybrid systems, whose continuous variables are bounded by piecewise-linear trajectories. Most embedded programs, however, operate in nonlinear environments. We present, analyze, and apply two algorithms for translating nonlinear hybrid systems into linear hybrid systems.

The clock translation replaces nonlinear variables by clock variables; the rate translation approximates nonlinear variables by piecewise-linear envelopes. Both translations are sound for reachability; that is, if we establish a safety property of the translated linear system, we may conclude that the original nonlinear system satisfies the property. The clock translation is also complete for reachability; that is, the original system and the translated system satisfy the same safety properties. The two translations apply to incomparable classes of nonlinear hybrid systems. From the clock translation we obtain a new decidability result for hybrid systems.

With the help of Hytech, a symbolic model checker for linear hybrid systems, we automatically verify a nonlinear railroad gate control program using the clock translation, and a nonlinear temperature control program using the rate translation.

Keywords

Hybrid System Safety Property Label Transition System Action Predicate Rate Translation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    R. Alur, C. Coucoubetis, 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.Google Scholar
  2. 2.
    R. Alur, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. Hybrid Systems, Lecture Notes in Computer Science 736, pp. 209–229. Springer, 1993.Google Scholar
  3. 3.
    R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.CrossRefGoogle Scholar
  4. 4.
    R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. IEEE Real-time Systems Symposium, pp. 2–11, 1993.Google Scholar
  5. 5.
    J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, 1992.CrossRefGoogle Scholar
  6. 6.
    P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. ACM Symposium on Principles of Programming Languages, 1977.Google Scholar
  7. 7.
    R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors. Hybrid Systems. Lecture Notes in Computer Science 736. Springer, 1993.Google Scholar
  8. 8.
    T.A. Henzinger, P. Kopke, A. Puri, and P. Varaiya. What's decidable about hybrid automata? ACM Symposium on Theory of Computing, 1995.Google Scholar
  9. 9.
    T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193–244, 1994.Google Scholar
  10. 10.
    X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. An approach to the description and analysis of hybrid systems. Hybrid Systems, Lecture Notes in Computer Science 736, pp. 149–178. Springer, 1993.Google Scholar
  11. 11.
    A. Olivero, J. Sifakis, and S. Yovine. Using abstractions for the verification of linear hybrid systems. CAV 94: Computer-aided Verification, Lecture Notes in Computer Science 818, pp. 81–94. Springer, 1994.Google Scholar
  12. 12.
    A. Puri and P. Varaiya. Decidability of hybrid systems with rectangular differential inclusions. CAV 94: Computer-aided Verification, Lecture Notes in Computer Science 818, pp. 95–104. Springer, 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Thomas A. Henzinger
    • 1
  • Pei -Hsin Ho
    • 1
  1. 1.Computer Science DepartmentCornell UniversityIthaca

Personalised recommendations