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 denition of hybrid I/O automata and of an implementation relation based on hybrid traces, (2) the denition of a simulation between hybrid I/O automata and a proof that existence of a simulation implies the implementation relation, (3) a denition of composition of hybrid I/O automata and a proof that it respects the im-plementation relation, and (4) a denition of receptiveness for hybrid I/O automata and a proof that, assuming certain compatibility conditions, receptiveness is preserved by composition.