## A Theory of Timed Automata

*Rajeev Alur and
David L. Dill*
We propose {\it timed (finite) automata\/}
to model the behavior of real-time systems over time.
Our definition provides a simple, and yet powerful,
way to annotate state-transition graphs with timing
constraints using finitely many real-valued {\it clocks\/}.
A timed automaton accepts {\it timed words\/} --- infinite sequences
in which a real-valued time of occurrence is associated
with each symbol. We study timed automata from the
perspective of formal language theory: we consider closure
properties, decision problems, and subclasses.
We consider both nondeterministic and deterministic transition structures,
and both \Buchi\ and Muller acceptance conditions.
We show that nondeterministic timed automata are closed under
union and intersection, but not under complementation, whereas
deterministic timed Muller automata are closed under all Boolean operations.
The main construction of the paper is an (PSPACE) algorithm for checking
the emptiness of the language of a (nondeterministic) timed automaton.
We also prove that the universality problem
and the language inclusion problem are solvable only
for the deterministic automata: both problems are undecidable ($\Pi_1^1$-hard)
in the nondeterministic case and PSPACE-complete in the deterministic case.
Finally, we discuss the application of this theory to automatic
verification of real-time requirements of finite-state
systems.

*Theoretical Computer Science* 126:183-235, 1994.
Preliminary versions appeared in
*Automata, Languages, and Programming: Proceedings of the
17th ICALP*, LNCS 443, 1990, and *Real Time: Theory in
Practice*, LNCS 600, 1991.