## Real-time Logics: Complexity and Expressiveness

*Rajeev Alur and
Thomas A. Henzinger*
The theory of the natural numbers with linear order and monadic predicates
underlies propositional linear temporal logic.
To study temporal logics that are suitable for reasoning about real-time
systems, we combine this classical theory of infinite state sequences with a
theory of discrete time, via a monotonic function that maps every state to
its time.
The resulting theory of timed state sequences is shown to be decidable,
albeit nonelementary, and its expressive power is characterized by
omega-regular sets.
Several more expressive variants are proved to be highly undecidable.

This framework allows us to classify a wide variety of real-time logics
according to their complexity and expressiveness.
Indeed, it follows that most formalisms proposed in the literature cannot be
decided.
We are, however, able to identify two elementary real-time temporal logics as
expressively complete fragments of the theory of timed state sequences, and
we present tableau-based decision procedures for checking validity.
Consequently, these two formalisms are well-suited for the specification and
verification of real-time systems.

*Information and Computation* 104:35-77, 1993.
A preliminary version appeared in the
*Proceedings of the
Fifth Annual IEEE Symposium on Logic in Computer Science*
(LICS 1990), pp. 390-401.