We consider 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 clocks. A timed automaton accepts 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 discuss the application of this theory to automatic verification of real-time requirements of finite-state systems. Finally, we give an overview of the heuristics employed by different tools to alleviate the computational complexity of the verification algorithm.
Formal Methods for Real-Time Computing, Trends in Software Series, John Wiley & Sons Publishers, pp. 55-82, 1996.