Skip to main content
SpringerLink
Log in

Hybrid I/O Automata Revisited

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

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

Included in the following conference series:

Abstract

In earlier work, we developed a mathematical hybrid I/O automaton (HIOA) modeling framework, capable of describing both discrete and continuous behavior. This framework has been used to analyze examples of automated transportation systems, intelligent vehicle high-way systems, air traffic control systems, and consumer electronics applications. Here, we reconsider the basic definitions of the HIOA framework, in particular, the dual use of external variables for discrete and continuous communication. We present a new HIOA model that is simpler than the earlier model, due to a clearer separation between discrete and continuous activity.

Supported by AFOSR F49620-00-1-0097, F49620-97-1-0337; NTT MIT9904-12; NSF ACI-9876931, CCR-9909114, CCR-9804665; PATH 1784-18454LD.

Supported by MURST project TOSCA.

Supported by Esprit Project 26270, Verification of Hybrid Systems (VHS).

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

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. R. Alur and T.A. Henzinger. Reactive modules. Proc. LICS’96, pp. 207–218, 1996.

    Google Scholar 

  3. R. Alur and T.A. Henzinger. Modularity for timed and hybrid systems. In Proc. of CONCUR’97, LNCS 1243, pp. 74–88, 1997.

    Google Scholar 

  4. D.J.B. Bosscher, I. Polak, and F.W. Vaandrager. Verification of an audio control protocol. In Proc. of FTRTFT’94, LNCS 863, pp. 170–192, 1994.

    Google Scholar 

  5. D. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. ACM Distinguished Dissertations. MIT Press, 1988.

    Google Scholar 

  6. E. Dolginova and N.A. Lynch. Safety verification for automated platoon maneuvers: A case study. Proc. of HART’97, LNCS 1201, pp. 154–170, 1997.

    Google Scholar 

  7. C.A. Gunter. Semantics of Programming Languages: Structures and Techniques. MIT Press, Cambridge, Massachusetts, 1992.

    MATH  Google Scholar 

  8. A. Kapur, T.A. Henzinger, Z. Manna, and A. Pnueli. Proving safety properties of hybrid systems. In Proc. of FTRTFT’94, LNCS 863, pp. 431–454, 1994.

    Google Scholar 

  9. C. Livadas, J. Lygeros, and N.A. Lynch. High-level modelling and analysis of TCAS. In Proc. of RTSS’99, 1999.

    Google Scholar 

  10. C. Livadas and N.A. Lynch. Formal verification of safety-critical hybrid systems. In Proc. of HSCC’98, LNCS 1386, pp. 253–272, 1998.

    Google Scholar 

  11. J. Lygeros and N.A. Lynch. On the formal verification of the TCAS conflict resolution algorithms. In Proc. of 36th IEEE Conference on Decision and Control, pp. 1829–1834, 1997. Extended abstract.

    Google Scholar 

  12. J. Lygeros and N.A. Lynch. Strings of vehicles: Modeling and safety conditions. In Proc. of HSCC’98, LNCS 1386, pp. 273–288, 1998.

    Google Scholar 

  13. N.A. Lynch. Modelling and verification of automated transit systems, using timed automata, invariants and simulations. In Hybrid Systems III, LNCS 1066, 1996.

    Google Scholar 

  14. N.A. Lynch. A three-level analysis of a simple acceleration maneuver, with uncertainties. Proc. of 3 rd AMAST Workshop on Real-Time Systems, pp. 1–22, 1996.

    Google Scholar 

  15. N.A. Lynch, R. Segala, F.W. Vaandrager, and H.B. Weinberg. Hybrid I/O automata. In Hybrid Systems III, LNCS 1066, pp. 496–510, 1996.

    Chapter  Google Scholar 

  16. N.A. Lynch, R. Segala, F.W. Vaandrager, and H.B. Weinberg. Hybrid I/O automata. Report CSI-R9907, Computing Science Institute, Univ. of Nijmegen, 1999.

    Google Scholar 

  17. N.A. Lynch and F.W. Vaandrager. Action transducers and timed automata. Formal Aspects of Computing, 8(5):499–538, 1996.

    Article  MATH  Google Scholar 

  18. N.A. Lynch and H.B. Weinberg. Proving correctness of a vehicle maneuver: Deceleration. Proc. 2 nd European Workshop on Real-Time and Hybrid Systems, 1995.

    Google Scholar 

  19. O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In Proc. REX Workshop on Real-Time: Theory in Practice, LNCS 600, pp. 447–484, 1992.

    Chapter  Google Scholar 

  20. R. Segala, R. Gawlick, J.F. Søgaard-Andersen, and N.A. Lynch. Liveness in timed and untimed systems. Information and Computation, 141(2):119–171, March 1998.

    Article  MATH  MathSciNet  Google Scholar 

  21. E.D. Sontag. Mathematical Control Theory — Deterministic Finite Dimensional Systems, volume 6 of Texts in Applied Mathematics. Springer-Verlag, 1990.

    Google Scholar 

  22. H.B. Weinberg and N.A. Lynch. Correctness of vehicle control systems: A case study. In Proc. RTSS’96, pp. 62–72, 1996.

    Google Scholar 

  23. H.B. Weinberg, N.A. Lynch, and N. Delisle. Verification of automated vehicle protection systems. In Hybrid Systems III, LNCS 1066, pp. 101–113,1996.

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. MIT Laboratory for Computer Science, Cambridge, MA, 02139, USA

    Nancy Lynch

  2. Dipartimento di Matematica, Universitá di Bologna, Piazza di Porta San Donato 5, 40127, Bologna, Italy

    Roberto Segala

  3. Computing Science Institute, University of Nijmegen, P.O. Box 9010, 6500, GL Nijmegen, The Netherlands

    Frits Vaandrager

Authors
  1. Nancy Lynch
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Roberto Segala
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Frits Vaandrager
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Ingegneria Elettrica, Universitá dell’Aquila, Poggio di Roio, 67040, L’Aquila, Italy

    Maria Domenica Di Benedetto

  2. University of California at Berkeley, Berkeley, CA, 94720

    Alberto Sangiovanni-Vincentelli

  3. PARADES, Via San Pantaleo, 66, 00186, Roma, Italy

    Alberto Sangiovanni-Vincentelli

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lynch, N., Segala, R., Vaandrager, F. (2001). Hybrid I/O Automata Revisited. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds) Hybrid Systems: Computation and Control. HSCC 2001. Lecture Notes in Computer Science, vol 2034. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45351-2_33

Download citation

  • DOI: https://doi.org/10.1007/3-540-45351-2_33

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41866-5

  • Online ISBN: 978-3-540-45351-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation