---
DOAJ_listed: '1'
OA_place: publisher
OA_type: gold
_id: '18530'
abstract:
- lang: eng
  text: "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."
acknowledgement: This work has in parts been presented at the 33rd International Conference
  on Concurrency Theory (CONCUR’22) [HLT22] and at the 16th International Workshop
  on Reachability Problems (RP’22) [BHL+22]. This work was supported by the EU (ERC-2020-AdG
  101020093); the EPSRC (EP/V025848/1, EP/X042596/1, EP/X017796/1 and EP/X03688X/1);
  and the ANR (QUASY 23-CE48-0008-01).
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Sougata
  full_name: Bose, Sougata
  last_name: Bose
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000-0002-2985-7724
- first_name: Karoliina
  full_name: Lehtinen, Karoliina
  last_name: Lehtinen
- first_name: Sven
  full_name: Schewe, Sven
  last_name: Schewe
- first_name: Patrick
  full_name: Totzke, Patrick
  last_name: Totzke
citation:
  ama: Bose S, Henzinger TA, Lehtinen K, Schewe S, Totzke P. History-deterministic
    timed automata. <i>Logical Methods in Computer Science</i>. 2024;20(4):1-28. doi:<a
    href="https://doi.org/10.46298/lmcs-20(4:1)2024">10.46298/lmcs-20(4:1)2024</a>
  apa: Bose, S., Henzinger, T. A., Lehtinen, K., Schewe, S., &#38; Totzke, P. (2024).
    History-deterministic timed automata. <i>Logical Methods in Computer Science</i>.
    EPI Sciences. <a href="https://doi.org/10.46298/lmcs-20(4:1)2024">https://doi.org/10.46298/lmcs-20(4:1)2024</a>
  chicago: Bose, Sougata, Thomas A Henzinger, Karoliina Lehtinen, Sven Schewe, and
    Patrick Totzke. “History-Deterministic Timed Automata.” <i>Logical Methods in
    Computer Science</i>. EPI Sciences, 2024. <a href="https://doi.org/10.46298/lmcs-20(4:1)2024">https://doi.org/10.46298/lmcs-20(4:1)2024</a>.
  ieee: S. Bose, T. A. Henzinger, K. Lehtinen, S. Schewe, and P. Totzke, “History-deterministic
    timed automata,” <i>Logical Methods in Computer Science</i>, vol. 20, no. 4. EPI
    Sciences, pp. 1–28, 2024.
  ista: Bose S, Henzinger TA, Lehtinen K, Schewe S, Totzke P. 2024. History-deterministic
    timed automata. Logical Methods in Computer Science. 20(4), 1–28.
  mla: Bose, Sougata, et al. “History-Deterministic Timed Automata.” <i>Logical Methods
    in Computer Science</i>, vol. 20, no. 4, EPI Sciences, 2024, pp. 1–28, doi:<a
    href="https://doi.org/10.46298/lmcs-20(4:1)2024">10.46298/lmcs-20(4:1)2024</a>.
  short: S. Bose, T.A. Henzinger, K. Lehtinen, S. Schewe, P. Totzke, Logical Methods
    in Computer Science 20 (2024) 1–28.
corr_author: '1'
date_created: 2024-11-10T23:02:01Z
date_published: 2024-10-02T00:00:00Z
date_updated: 2026-07-07T13:37:45Z
day: '02'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.46298/lmcs-20(4:1)2024
ec_funded: 1
external_id:
  arxiv:
  - '2304.03183'
  isi:
  - '001332466900002'
file:
- access_level: open_access
  checksum: 26826786a960039b9501cfc5cb4f3fe6
  content_type: application/pdf
  creator: dernst
  date_created: 2024-11-11T08:32:02Z
  date_updated: 2024-11-11T08:32:02Z
  file_id: '18532'
  file_name: 2024_LMCS_Bose.pdf
  file_size: 563394
  relation: main_file
  success: 1
file_date_updated: 2024-11-11T08:32:02Z
fulldoi: https://doi.org/10.46298/lmcs-20(4:1)2024
has_accepted_license: '1'
intvolume: '        20'
isi: 1
issue: '4'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 1-28
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: Logical Methods in Computer Science
publication_identifier:
  eissn:
  - 1860-5974
publication_status: published
publisher: EPI Sciences
quality_controlled: '1'
related_material:
  record:
  - id: '12508'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: History-deterministic timed automata
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 20
year: '2024'
...