Nancy Lynch and Frits Vaandrager. Action Transducers and Timed Automata. Formal Aspects of Computing, 8(5):499-538, 1996. Also, Technical Memo MIT/LCS/TM-480.c., Laboratory for Computer Science, Massachusetts Institute of Technology, July 1995. .pdf.

Abstract

The timed automaton model of Lynch, Vaandrager 1991 REX paper and Lynch, Vaandrager timed paper is a general model for timing-based systems. A notion of timed 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.