---
OA_place: publisher
OA_type: gold
_id: '18068'
abstract:
- lang: eng
  text: "We study the following refinement relation between nondeterministic state-transition
    models: model ℬ strategically dominates model \U0001D49C iff every deterministic
    refinement of \U0001D49C is language contained in some deterministic refinement
    of ℬ. While language containment is trace inclusion, and the (fair) simulation
    preorder coincides with tree inclusion, strategic dominance falls strictly between
    the two and can be characterized as \"strategy inclusion\" between \U0001D49C
    and ℬ: every strategy that resolves the nondeterminism of \U0001D49C is dominated
    by a strategy that resolves the nondeterminism of ℬ. Strategic dominance can be
    checked in 2-ExpTime by a decidable first-order Presburger logic with quantification
    over words and strategies, called resolver logic. We give several other applications
    of resolver logic, including checking the co-safety, co-liveness, and history-determinism
    of boolean and quantitative automata, and checking the inclusion between hyperproperties
    that are specified by nondeterministic boolean and quantitative automata."
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. N.
  Mazzocchi was affiliated with ISTA when this work was submitted for publication.
alternative_title:
- LIPIcs
article_number: '29'
article_processing_charge: Yes
arxiv: 1
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: Nicolas Adrien
  full_name: Mazzocchi, Nicolas Adrien
  id: b26baa86-3308-11ec-87b0-8990f34baa85
  last_name: Mazzocchi
- first_name: Naci E
  full_name: Sarac, Naci E
  id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
  last_name: Sarac
citation:
  ama: 'Henzinger TA, Mazzocchi NA, Sarac NE. Strategic dominance: A new preorder
    for nondeterministic processes. 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.29">10.4230/LIPIcs.CONCUR.2024.29</a>'
  apa: 'Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2024). Strategic dominance:
    A new preorder for nondeterministic processes. 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.29">https://doi.org/10.4230/LIPIcs.CONCUR.2024.29</a>'
  chicago: 'Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Strategic
    Dominance: A New Preorder for Nondeterministic Processes.” 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.29">https://doi.org/10.4230/LIPIcs.CONCUR.2024.29</a>.'
  ieee: 'T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Strategic dominance:
    A new preorder for nondeterministic processes,” in <i>35th International Conference
    on Concurrency Theory</i>, Calgary, Canada, 2024, vol. 311.'
  ista: 'Henzinger TA, Mazzocchi NA, Sarac NE. 2024. Strategic dominance: A new preorder
    for nondeterministic processes. 35th International Conference on Concurrency Theory.
    CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 311, 29.'
  mla: 'Henzinger, Thomas A., et al. “Strategic Dominance: A New Preorder for Nondeterministic
    Processes.” <i>35th International Conference on Concurrency Theory</i>, vol. 311,
    29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2024.29">10.4230/LIPIcs.CONCUR.2024.29</a>.'
  short: T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, 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:45:38Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: GradSch
doi: 10.4230/LIPIcs.CONCUR.2024.29
ec_funded: 1
external_id:
  arxiv:
  - '2407.10473'
  isi:
  - '001556847400029'
file:
- access_level: open_access
  checksum: 555bd343e1fb38adeab8fc465ff4fad8
  content_type: application/pdf
  creator: dernst
  date_created: 2024-09-17T07:48:56Z
  date_updated: 2024-09-17T07:48:56Z
  file_id: '18081'
  file_name: 2024_LIPICS_Henzinger.pdf
  file_size: 964124
  relation: main_file
  success: 1
file_date_updated: 2024-09-17T07:48:56Z
fulldoi: https://doi.org/10.4230/LIPIcs.CONCUR.2024.29
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: 'Strategic dominance: A new preorder for nondeterministic processes'
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'
...