## Logics and Models of Real Time: A Survey

*Rajeev Alur and
Thomas A. Henzinger*
We survey logic-based and automata-based languages and techniques for the
specification and verification of real-time systems.
In particular, we discuss three syntactic extensions of temporal logic:
time-bounded operators, freeze quantification, and time variables.
We also discuss the extension of finite-state machines with clocks and the
extension of transition systems with time bounds on the transitions.
All of the resulting notations can be interpreted over a variety of different
models of time and computation, including linear and branching time,
interleaving and true concurrency, discrete and continuous time.
For each choice of syntax and semantics, we summarize the results that are
known about expressive power, algorithmic finite-state verification, and
deductive verification.

*Real Time: Theory in Practice*,
Lecture Notes in Computer Science 600,
Springer-Verlag, 1992, pp. 74-106.