Abstract
We propose a new hybrid I/O automaton model that is capable of describing both continuous and discrete behavior. The model, which extends the timed I/O automaton model of [12, 7] and the phase transition system models of [15, 2], allows communication among components using both shared variables and shared actions. The main contributions of this paper are: (1) the definition of hybrid I/O automata and of an implementation relation based on hybrid traces, (2) the definition of a simulation between hybrid I/O automata and a proof that existence of a simulation implies the implementation relation, (3) a definition of composition of hybrid I/O automata and a proof that it respects the implementation relation, and (4) a definition of receptiveness for hybrid I/O automata and a proof that, assuming certain compatibility conditions, receptiveness is preserved by composition.
Supported by NSF Grant 9225124-CCR, U.S. Department of Transportation Contract DTRS95G-0001-YR.8, AFOSR-ONR Contract F49620-94-1-0199, and ARPA Contracts F19628-95-C-0118 and N00014-92-J-4033.
Research partially supported by a National Science Foundation Graduate Fellowship.
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi and L. Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 1(15):73–132, 1993.
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.
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 Grossman et al. [8], pages 209–229.
J.C.M. Baeten and W.P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990.
D.J.B. Bosscher, I. Polak, and F.W. Vaandrager. Verification of an audio control protocol. In Proc. FTRTFT'94, LNCS 863, pages 170–192. Springer-Verlag, 1994.
D. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. ACM Distinguished Dissertations. MIT Press, 1988.
R. Gawlick, R. Segala, J.F. Søgaard-Andersen, and N. Lynch. Liveness in timed and untimed systems. In Proceedings 21th ICALP, LNCS 820. Springer-Verlag, 1994. A full version appears as MIT Technical Report number MIT/LCS/TR-587.
R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors. Hybrid Systems, LNCS 736. Springer-Verlag, 1993.
L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, March 1994.
N.A. Lynch. Modelling and verification of automated transit systems, using timed automata, invariants and simulations, 1996. This volume.
N.A. Lynch and M.R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings 6th PODC, pages 137–151, August 1987. A full version is available as MIT Technical Report MIT/LCS/TR-387.
N.A. Lynch and F.W. Vaandrager. Forward and backward simulations — part II: Timing-based systems. Report CS-R9314, CWI, Amsterdam, March 1993. To appear in Information and Computation.
N.A. Lynch and F.W. Vaandrager. Forward and backward simulations. part I: Untimed systems. Information and Computation, 121(2):214–233, September 1995.
N.A. Lynch and H.B. Weinberg. Proving correctness of a vehicle maneuver: Deceleration. In Proceedings Second European Workshop on Real-Time and Hybrid Systems, Grenoble, France, June 1995.
O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In Proceedings REX Workshop, LNCS 600, pages 447–484. Springer-Verlag, 1992.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
A. Nerode and A. Yakhnis. Concurrent programs as strategies in games. In Y. Moschovakis, editor, Logic from Computer Science. Springer-Verlag, 1992.
A. Pnueli and J. Sifakis, editors. Special Issue on Hybrid Systems of Theoretical Computer Science, 138(1). Elsevier Science Publishers, February 1995.
E.D. Sontag. Mathematical Control Theory — Deterministic Finite Dimensional Systems, TAM 6. Springer-Verlag, 1990.
H.B. Weinberg, N.A. Lynch, and N. Delisle. Verification of automated vehicle protection systems, 1996. This volume.
Author information
Authors and Affiliations
Corresponding author
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lynch, N., Segala, R., Vaandrager, F., Weinberg, H.B. (1996). Hybrid I/O automata. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds) Hybrid Systems III. HS 1995. Lecture Notes in Computer Science, vol 1066. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0020971
Download citation
DOI: https://doi.org/10.1007/BFb0020971
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61155-4
Online ISBN: 978-3-540-68334-6
eBook Packages: Springer Book Archive