---
res:
  bibo_abstract:
  - "We explore the notion of history-determinism in the context of timed automata
    (TA) over infinite timed words. History-deterministic (HD) automata are those
    in which nondeterminism can be resolved on the fly, based on the run constructed
    thus far. History-determinism is a robust property that admits different game-based
    characterisations, and HD specifications allow for game-based verification without
    an expensive determinization step. We show that the class of timed ω\r\n-languages
    recognized by HD timed automata strictly extends that of deterministic ones, and
    is strictly included in those recognised by fully non-deterministic TA. For non-deterministic
    timed automata it is known that universality is already undecidable for safety/reachability
    TA. For history-deterministic TA with arbitrary parity acceptance, we show that
    timed universality, inclusion, and synthesis all remain decidable and are EXPTIME-complete.
    For the subclass of TA with safety or reachability acceptance, one can decide
    (in EXPTIME) whether such an automaton is history-deterministic. If so, it can
    effectively determinized without introducing new automaton states.@eng"
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Sougata
      foaf_name: Bose, Sougata
      foaf_surname: Bose
  - 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
  - foaf_Person:
      foaf_givenName: Karoliina
      foaf_name: Lehtinen, Karoliina
      foaf_surname: Lehtinen
  - foaf_Person:
      foaf_givenName: Sven
      foaf_name: Schewe, Sven
      foaf_surname: Schewe
  - foaf_Person:
      foaf_givenName: Patrick
      foaf_name: Totzke, Patrick
      foaf_surname: Totzke
  bibo_doi: 10.46298/lmcs-20(4:1)2024
  bibo_issue: '4'
  bibo_volume: 20
  dct_date: 2024^xs_gYear
  dct_identifier:
  - UT:001332466900002
  dct_isPartOf:
  - http://id.crossref.org/issn/1860-5974
  dct_language: eng
  dct_publisher: EPI Sciences@
  dct_title: History-deterministic timed automata@
...
