## Back to the Future: Towards a Theory of Timed Regular Languages

*Rajeev Alur and
Thomas A. Henzinger*

*Timed Automata* are finite-state machines constrained by timing
requirements so that they accept timed words--words in which every
symbol is labeled with a real-valued time. These automata were
designed to lead to a theory of finite-state real-time properties with
applications to the automatic verification of real-time systems.
However, both deterministic and nondeterministic versions suffer from
drawbacks: several key problems, such as language inclusion, are
undecidable for nondeterministic timed automata, whereas deterministic
timed automata lack considerable expressive power when compared to
decidable real-time logics.

This is why we introduce *two-way* timed automata--timed automata
that can move back and forth while reading a timed word. Two-wayness
in its unrestricted form leads, like nondeterminism, to the
undecidability of language inclusion. However, if we restrict the
number of times an input symbol may be revisited, then two-wayness is
both harmless and desirable. We show that the resulting class of
bounded two-way deterministic timed automata is closed under all
boolean operations, has decidable (PSPACE-complete) emptiness and
inclusion problems, and subsumes all decidable real-time logics we
know.

We obtain a strict hierarchy of real-time properties: deterministic
timed automata can accept more languages as the bound on the number of
times an input symbol may be revisited is increased. This hierarchy
is also enforced by the number of alternations between past and future
operators in temporal logic. The combination of our results leads to
a decision procedure for a real-time logic with past operators.

*Proceedings of the
33rd Annual Symposium on Foundations of Computer Science*
(FOCS), IEEE Computer Society Press, 1992, pp. 177-186.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1992 IEEE.