## Automata-theoretic Verification of Real-Time Systems

*Rajeev Alur and
David L. Dill*
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.