---
res:
  bibo_abstract:
  - "The authors 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
    they restrict the number of times an input symbol may be revisited, then two-wayness
    is both harmless and desirable. The authors 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. They 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 the results leads to a decision procedure
    for a real-time logic with past operators\r\n@eng"
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Rajeev
      foaf_name: Alur, Rajeev
      foaf_surname: Alur
  - foaf_Person:
      foaf_givenName: Thomas A
      foaf_name: Henzinger, Thomas A
      foaf_surname: Henzinger
      foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
    orcid: 0000−0002−2985−7724
  bibo_doi: 10.1109/SFCS.1992.267774
  dct_date: 1992^xs_gYear
  dct_language: eng
  dct_publisher: IEEE@
  dct_title: 'Back to the future: Towards a theory of timed regular languages@'
...
