Hybrid I/O Automata (extended abstract)

Abstract. We propose a new hybrid I/O automaton model that is ca-pable 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 compo-nents using both shared variables and shared actions. The main contri-butions of this paper are: (1) the definition of hybrid I/O automata nd of an implementation relation based on hybrid traces, (2) the definition of a simulation between hybrid I/O automata nd a proof that existence of a simulation implies the implementation relation, (3) a definition of composition ofhybrid I/O automata nd a proof that it respects the im-plementation relation, and (4) a definition of receptiveness for hybrid I/O automata nd a proof that, assuming certain compatibility conditions, receptiveness i preserved by composition.