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

: 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 s..