Hybrid I/O Automata

Appears: Hybrid Systems III, LNCS 1066, pages 496-510 (Papers from DIMACS Workshop on Verification and Control of Hybrid Systems, October, 1995).

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

Download:
Download the paper from the publisher.

Download an author-created copy of the paper (© Springer-Verlag).