---
_id: '12508'
abstract:
- lang: eng
  text: "We explore the notion of history-determinism in the context of timed automata
    (TA). History-deterministic 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 history-deterministic
    specifications allow for game-based verification without an expensive determinization
    step.\r\nWe show yet another characterisation of history-determinism in terms
    of fair simulation, at the general level of labelled transition systems: a system
    is history-deterministic precisely if and only if it fairly simulates all language
    smaller systems.\r\nFor timed automata over infinite timed words it is known that
    universality is undecidable for Büchi TA. We show that for history-deterministic
    TA with arbitrary parity acceptance, timed universality, inclusion, and synthesis
    all remain decidable and are ExpTime-complete.\r\nFor the subclass of TA with
    safety or reachability acceptance, we show that checking whether such an automaton
    is history-deterministic is decidable (in ExpTime), and history-deterministic
    TA with safety acceptance are effectively determinizable without introducing new
    automata states."
acknowledgement: "Thomas A. Henzinger: This work was supported in part by the ERC-2020-AdG
  101020093.\r\nPatrick Totzke: acknowledges support from the EPSRC, project no. EP/V025848/1.\r\n"
alternative_title:
- LIPIcs
article_processing_charge: No
author:
- 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: Patrick
  full_name: Totzke, Patrick
  last_name: Totzke
citation:
  ama: 'Henzinger TA, Lehtinen K, Totzke P. History-deterministic timed automata.
    In: <i>33rd International Conference on Concurrency Theory</i>. Vol 243. Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik; 2022:14:1-14:21. doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2022.14">10.4230/LIPIcs.CONCUR.2022.14</a>'
  apa: 'Henzinger, T. A., Lehtinen, K., &#38; Totzke, P. (2022). History-deterministic
    timed automata. In <i>33rd International Conference on Concurrency Theory</i>
    (Vol. 243, p. 14:1-14:21). Warsaw, Poland: Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik. <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2022.14">https://doi.org/10.4230/LIPIcs.CONCUR.2022.14</a>'
  chicago: Henzinger, Thomas A, Karoliina Lehtinen, and Patrick Totzke. “History-Deterministic
    Timed Automata.” In <i>33rd International Conference on Concurrency Theory</i>,
    243:14:1-14:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2022.14">https://doi.org/10.4230/LIPIcs.CONCUR.2022.14</a>.
  ieee: T. A. Henzinger, K. Lehtinen, and P. Totzke, “History-deterministic timed
    automata,” in <i>33rd International Conference on Concurrency Theory</i>, Warsaw,
    Poland, 2022, vol. 243, p. 14:1-14:21.
  ista: 'Henzinger TA, Lehtinen K, Totzke P. 2022. History-deterministic timed automata.
    33rd International Conference on Concurrency Theory. CONCUR: Conference on Concurrency
    Theory, LIPIcs, vol. 243, 14:1-14:21.'
  mla: Henzinger, Thomas A., et al. “History-Deterministic Timed Automata.” <i>33rd
    International Conference on Concurrency Theory</i>, vol. 243, Schloss Dagstuhl
    - Leibniz-Zentrum für Informatik, 2022, p. 14:1-14:21, doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2022.14">10.4230/LIPIcs.CONCUR.2022.14</a>.
  short: T.A. Henzinger, K. Lehtinen, P. Totzke, in:, 33rd International Conference
    on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022,
    p. 14:1-14:21.
conference:
  end_date: 2022-09-16
  location: Warsaw, Poland
  name: 'CONCUR: Conference on Concurrency Theory'
  start_date: 2022-09-13
date_created: 2023-02-05T17:24:23Z
date_published: 2022-09-06T00:00:00Z
date_updated: 2023-02-06T09:23:31Z
day: '06'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2022.14
ec_funded: 1
file:
- access_level: open_access
  checksum: 9e97e15628f66b2ad77f535bb0327dee
  content_type: application/pdf
  creator: dernst
  date_created: 2023-02-06T09:21:09Z
  date_updated: 2023-02-06T09:21:09Z
  file_id: '12520'
  file_name: 2022_LIPICs_Henzinger2.pdf
  file_size: 717940
  relation: main_file
  success: 1
file_date_updated: 2023-02-06T09:21:09Z
has_accepted_license: '1'
intvolume: '       243'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '09'
oa: 1
oa_version: Published Version
page: 14:1-14:21
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: 33rd International Conference on Concurrency Theory
publication_identifier:
  isbn:
  - '9783959772464'
  issn:
  - 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
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: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 243
year: '2022'
...