---
_id: '18067'
abstract:
- lang: eng
  text: "An automaton \U0001D49C is history-deterministic if its nondeterminism can
    be resolved on the fly, only using the prefix of the word read so far. This mild
    form of nondeterminism has attracted particular attention for its applications
    in synthesis problems. An automaton \U0001D49C is guidable with respect to a class
    C of automata if it can fairly simulate every automaton in C, whose language is
    contained in that of \U0001D49C. In other words, guidable automata are those for
    which inclusion and simulation coincide, making them particularly interesting
    for model-checking. We study the connection between these two notions, and specifically
    the question of when they coincide. For classes of automata on which they do,
    deciding guidability, an otherwise challenging decision problem, reduces to deciding
    history-determinism, a problem that is starting to be well-understood for many
    classes. We provide a selection of sufficient criteria for a class of automata
    to guarantee the coincidence of the notions, and use them to show that the notions
    coincide for the most common automata classes, among which are ω-regular automata
    and many infinite-state automata with safety and reachability acceptance conditions,
    including vector addition systems with states, one-counter nets, pushdown-, Parikh-,
    and timed-automata. We also demonstrate that history-determinism and guidability
    do not always coincide, for example, for the classes of timed automata with a
    fixed number of clocks."
acknowledgement: "Udi Boker: Israel Science Foundation grant 2410/22\r\nThomas A.
  Henzinger: ERC-2020-AdG 101020093 (VAMOS)\r\nKaroliina Lehtinen: ANR QUASY 23-CE48-0008-01\r\nAditya
  Prakash: Chancellors’ International Scholarship from the University of Warwick and
  Centre for Discrete Mathematics and Its Applications (DIMAP)"
alternative_title:
- LIPIcs
article_number: '12'
article_processing_charge: No
arxiv: 1
author:
- first_name: Udi
  full_name: Boker, Udi
  id: 31E297B6-F248-11E8-B48F-1D18A9856A87
  last_name: Boker
- 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: Aditya
  full_name: Prakash, Aditya
  last_name: Prakash
citation:
  ama: 'Boker U, Henzinger TA, Lehtinen K, Prakash A. History-determinism vs fair
    simulation. In: <i>35th International Conference on Concurrency Theory</i>. Vol
    311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2024.12">10.4230/LIPIcs.CONCUR.2024.12</a>'
  apa: 'Boker, U., Henzinger, T. A., Lehtinen, K., &#38; Prakash, A. (2024). History-determinism
    vs fair simulation. In <i>35th International Conference on Concurrency Theory</i>
    (Vol. 311). Calgary, Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
    <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2024.12">https://doi.org/10.4230/LIPIcs.CONCUR.2024.12</a>'
  chicago: Boker, Udi, Thomas A Henzinger, Karoliina Lehtinen, and Aditya Prakash.
    “History-Determinism vs Fair Simulation.” In <i>35th International Conference
    on Concurrency Theory</i>, Vol. 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2024. <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2024.12">https://doi.org/10.4230/LIPIcs.CONCUR.2024.12</a>.
  ieee: U. Boker, T. A. Henzinger, K. Lehtinen, and A. Prakash, “History-determinism
    vs fair simulation,” in <i>35th International Conference on Concurrency Theory</i>,
    Calgary, Canada, 2024, vol. 311.
  ista: 'Boker U, Henzinger TA, Lehtinen K, Prakash A. 2024. History-determinism vs
    fair simulation. 35th International Conference on Concurrency Theory. CONCUR:
    Conference on Concurrency Theory, LIPIcs, vol. 311, 12.'
  mla: Boker, Udi, et al. “History-Determinism vs Fair Simulation.” <i>35th International
    Conference on Concurrency Theory</i>, vol. 311, 12, Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 2024, doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2024.12">10.4230/LIPIcs.CONCUR.2024.12</a>.
  short: U. Boker, T.A. Henzinger, K. Lehtinen, A. Prakash, in:, 35th International
    Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2024.
conference:
  end_date: 2024-09-13
  location: Calgary, Canada
  name: 'CONCUR: Conference on Concurrency Theory'
  start_date: 2024-09-09
corr_author: '1'
date_created: 2024-09-15T22:01:40Z
date_published: 2024-09-01T00:00:00Z
date_updated: 2025-12-02T13:44:54Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2024.12
ec_funded: 1
external_id:
  arxiv:
  - '2407.08620'
  isi:
  - '001556847400012'
file:
- access_level: open_access
  checksum: 66db11ef8e600a434079c278050c3f09
  content_type: application/pdf
  creator: dernst
  date_created: 2024-09-17T07:31:18Z
  date_updated: 2024-09-17T07:31:18Z
  file_id: '18080'
  file_name: 2024_LIPICS_Boker.pdf
  file_size: 766902
  relation: main_file
  success: 1
file_date_updated: 2024-09-17T07:31:18Z
has_accepted_license: '1'
intvolume: '       311'
isi: 1
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: 35th International Conference on Concurrency Theory
publication_identifier:
  isbn:
  - '9783959773393'
  issn:
  - 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: History-determinism vs fair simulation
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: 311
year: '2024'
...