Action transducers and timed automata

Thetimed automaton model of LyV92, LyV93] is a general model for timing-based systems. A notion oftimed action transducer is here defined as an automata-theoretic way of representing operations on timed automata. It is shown that two timed trace inclusion relations are substitutive with respect to operations that can be described by timed action transducers. Examples are given of operations that can be described in this way, and a preliminary proposal is given for an appropriate language of operators for describing timing-based systems.A preliminary version of this paper appeared in W.R. Cleaveland, editor,Proceedings CONCUR'92, Stony Brook, New York. LNCS 630, pages 436–455. Springer, 1992.Supported by ONR contracts N00014-85-K-0168 and N00014-91-J-1988, by NSF grant CCR-8915206, and by ARPA contracts N00014-89-J-1988 and N00014-92-J-4033.Supported by ESPRIT BRA 7166 CONCUR2 and by the HCM network EXPRESS. Part of the work on this paper was done while the author was at the Ecole des Mines, CMA, Sophia Antipolis, France, and at CWI, Amsterdam, The Netherlands.