Skip to main content
SpringerLink
Log in
Book cover

International Hybrid Systems Workshop

International Hybrid Systems Workshop

HS 1992, HS 1991: Hybrid Systems pp 209–229Cite as

Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems

  • Conference paper
  • First Online:

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

Abstract

We introduce the framework of hybrid automata as a model and specification language for hybrid systems. Hybrid automata can be viewed as a generalization of timed automata, in which the behavior of variables is governed in each state by a set of differential equations. We show that many of the examples considered in the workshop can be defined by hybrid automata. While the reachability problem is undecidable even for very restricted classes of hybrid automata, we present two semidecision procedures for verifying safety properties of piecewiselinear hybrid automata, in which all variables change at constant rates. The two procedures are based, respectively, on minimizing and computing fixpoints on generally infinite state spaces. We show that if the procedures terminate, then they give correct answers. We then demonstrate that for many of the typical workshop examples, the procedures do terminate and thus provide an automatic way for verifying their properties.

Supported in part by the BRA ESPRIT project REACT.

Supported in part by the National Science Foundation under grant CCR-9200794 and by the United States Air Force Office of Scientific Research under contract F49620-93-1-0056.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur, C. Courcoubetis, N. Halbwachs, D.L. Dill, and H. Wong-Toi. Minimization of timed transition systems. In CONCUR 92: Theories of Concurrency, Lecture Notes in Computer Science 630, pages 340–354. Springer-Verlag, 1992.

    Google Scholar 

  2. R. Alur and D.L. Dill. Automata for modeling real-time systems. In M.S. Paterson, editor, ICALP 90: Automata, Languages, and Programming, Lecture Notes in Computer Science 443, pages 322–335. Springer-Verlag, 1990.

    Google Scholar 

  3. A. Bouajjani, J.C. Fernandez, and N. Halbwachs. Minimal model generation. In R.P. Kurshan and E.M. Clarke, editors, CAV 90: Automatic Verification Methods for Finite-state Systems, Lecture Notes in Computer Science 531, pages 197–203. Springer-Verlag, 1990.

    Google Scholar 

  4. K. Cerāns. Decidability of bisimulation equivalence for parallel timer processes. In CAV 92: Automatic Verification Methods for Finite-state Systems, Lecture Notes in Computer Science. Springer-Verlag. To appear.

    Google Scholar 

  5. Z. Chaochen, C.A.R. Hoare, and A.P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269–276, 1991.

    Google Scholar 

  6. T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. In Proceedings of the Seventh Annual Symposium on Logic in Computer Science, pages 394–406. IEEE Computer Society Press, 1992.

    Google Scholar 

  7. D. Harel, A. Pnueli, and J. Stavi. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 26(2):222–243, 1983.

    Google Scholar 

  8. L. Lamport. A fast mutual exclusion algorithm. ACM Transactions on Computer Systems, 5(1):1–11, 1987.

    Google Scholar 

  9. D. Lee and M. Yannakakis. Online minimization of transition systems. In Proceedings of the 24th Annual Symposium on Theory of Computing. ACM Press, 1992.

    Google Scholar 

  10. O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In J.W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice, Lecture Notes in Computer Science 600, pages 447–484. Springer-Verlag, 1992.

    Google Scholar 

  11. X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. An approach to the description and analysis of hybrid systems. This volume.

    Google Scholar 

  12. X. Nicollin, J. Sifakis, and S. Yovine. From ATP to timed graphs and hybrid systems. In J.W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice, Lecture Notes in Computer Science 600, pages 549–572. Springer-Verlag, 1992.

    Google Scholar 

  13. F. Wang, A.K. Mok, and E.A. Emerson. Real-time distributed system specification and verification in asynchronous propositional temporal logic. In Proceedings of the 12th International Conference on Software Engineering, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. AT&T Bell Laboratories, USA

    Rajeev Alur

  2. Department of Computer Science, University of Crete, Greece

    Costas Courcoubetis

  3. Department of Computer Science, Cornell University, USA

    Thomas A. Henzinger & Pei -Hsin Ho

Authors
  1. Rajeev Alur
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Costas Courcoubetis
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Thomas A. Henzinger
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Pei -Hsin Ho
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Robert L. Grossman Anil Nerode Anders P. Ravn Hans Rischel

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.H. (1993). Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds) Hybrid Systems. HS HS 1992 1991. Lecture Notes in Computer Science, vol 736. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57318-6_30

Download citation

  • DOI: https://doi.org/10.1007/3-540-57318-6_30

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57318-0

  • Online ISBN: 978-3-540-48060-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation