## 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 Symposium on Logic in Computer Science*
(LICS), IEEE Computer Society Press, 1990, pp. 390-401.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1990 IEEE,
1993 Academic Press.