Timed Automata

The timed automaton model, developed by Lynch and Vaandrager, is a labelled transition system model for components in real-time systems. A timed automaton has time-passage actions, in addition to ordinary input, output and internal actions. The nonnegative real numbers are used as the time domain. The admissible executions of a timed automaton are those in which the time approaches infinity. Timed automata include "trajectories", which describe the evolution of the system state during time-passage. The behavior of a timed automaton is describable in terms of timed traces, or alternatively in terms of admissible timed traces. Both types of behavior are compositional.

Timed automata were developed along with various formal simulation proof methods, in the Lynch, Vaandrager 1991 REX paper. Later, we split this material into two separate parts, one for untimed automata, and one for timed automata; the timed results are based on the untimed results. The untimed paper has been accepted to Information and Computation. You can also access an earlier version of this paper. The earlier version contains some material on invariants and reachability that does not appear in the latest version. The timed paper has also been accepted to Information and Computation. You can also access an earlier version of this paper.

A good description of the timed automaton model can also be found in another paper, on timed action transducers. The focus of this latter paper, however, is the development of process algebraic methods for timed automata. An earlier version of this work appeared in CONCUR'92.

Timed automata are also defined in Chapter 23 of Nancy Lynch's book "Distributed Algorithms". They are used in that book to model communication channels and other real-time system components. Timed automata have been used to model a variety of real-time algorithms and systems, including some hybrid systems such as transportation systems. See our work on applications. Also see Vaandrager's work on consumer electronics.

TOC / LCS / MIT
Last modified: Mon Nov 10 11:36:14 1997 		Comments?