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.