## 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.

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