Nancy Lynch, Roberto Segala, Frits Vaandrager, and H.B.
Weinberg. Hybrid I/O Automata. Information and Computation, 185(1):105-157, August 2003. Also, MIT Technical Report
MIT-LCS-TR-827d, MIT Laboratory for Computer Science, Cambridge, MA 02139, January 13, 2003. .pdf
Earlier version in R. Alur,
T. Henzinger, and E. Sontag, editors, Hybrid Systems III: Verification
and Control (DIMACS/SYCON Workshop on Verification and Control of
Hybrid Systems, New Brunswick, New Jersey, October 1995), volume 1066
of Lecture Notes in Computer Science, pages 496-510. Springer-Verlag
1996. Also, Technical Memo MIT/LCS/TM-544, Laboratory for Computer
Science, Massachusetts Institute of Technology.
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 [LV93b,GSSL94] and the phase transition system models of [MMP92,AlurEtAl95], 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 em 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.