@INCOLLECTION{alur90:_real,
author = {R. Alur and T. Henzinger},
title = {Real-time logics: complexity and expressiveness},
booktitle = {Fifth Annual IEEE Symposium on Logic in Computer Science (Philadelphia,
PA, 1990)},
publisher = {IEEE Comput. Soc. Press},
year = {1990},
pages = {390--401},
address = {Los Alamitos, CA},
abstract = {
A theory of timed state sequences is introduced as a symbiosis of
a theory of discrete time and of the theory of the natural numbers
with linear order and monadic predicates, put together via a monotone
function that maps every state (natural number) to its "time".
The theory is shown to be (nonelementarily) decidable, and its expressive
power is characterized by $\omega$-regular sets, in contrast to many
more expressive variants that are shown to be highly undecidable
(with the validity problem being $\Pi\sp 1\sb 1$-complete). This
implies that most real-time logics proposed in the literature cannot
be decided.
Further, however, two elementary (EXPSPACE-complete) real-time temporal
logics, the so-called TPTL and MTL$\sb {\rm P}$, are identified as
expressively complete fragments of the theory of timed state sequences.
Out of that the authors conclude that these two logics are well suited
for the specification and verification of real-time systems. }
}