---
_id: '14920'
abstract:
- lang: eng
  text: "We consider fixpoint algorithms for two-player games on graphs with $\\omega$-regular
    winning conditions, where the environment is constrained by a strong transition
    fairness assumption. Strong transition fairness is a widely occurring special
    case of strong fairness, which requires that any execution is strongly fair with
    respect to a specified set of live edges: whenever the\r\nsource vertex of a live
    edge is visited infinitely often along a play, the edge itself is traversed infinitely
    often along the play as well. We show that, surprisingly, strong transition fairness
    retains the algorithmic characteristics of the fixpoint algorithms for $\\omega$-regular
    games -- the new algorithms have the same alternation depth as the classical algorithms
    but invoke a new type of predecessor operator. For Rabin games with $k$ pairs,
    the complexity of the new algorithm is $O(n^{k+2}k!)$ symbolic steps, which is
    independent of the number of live edges in the strong transition fairness assumption.
    Further, we show that GR(1) specifications with strong transition fairness assumptions
    can be solved with a 3-nested fixpoint algorithm, same as the usual algorithm.
    In contrast, strong fairness necessarily requires increasing the alternation depth
    depending on the number of fairness assumptions. We get symbolic algorithms for
    (generalized) Rabin, parity and GR(1) objectives under strong transition fairness
    assumptions as well as a direct symbolic algorithm for qualitative winning in
    stochastic\r\n$\\omega$-regular games that runs in $O(n^{k+2}k!)$ symbolic steps,
    improving the state of the art. Finally, we have implemented a BDD-based synthesis
    engine based on our algorithm. We show on a set of synthetic and real benchmarks
    that our algorithm is scalable, parallelizable, and outperforms previous algorithms
    by orders of magnitude."
acknowledgement: A previous version of this paper has appeared in TACAS 2022. Authors
  ordered alphabetically. T. Banerjee was interning with MPI-SWS when this research
  was conducted. R. Majumdar and A.-K. Schmuck are partially supported by DFG project
  389792660 TRR 248–CPEC. A.-K. Schmuck is additionally funded through DFG project
  (SCHM 3541/1-1). K. Mallik is supported by the ERC project ERC-2020-AdG 101020093.
article_number: '4'
article_processing_charge: Yes
article_type: original
arxiv: 1
author:
- first_name: Tamajit
  full_name: Banerjee, Tamajit
  last_name: Banerjee
- first_name: Rupak
  full_name: Majumdar, Rupak
  last_name: Majumdar
- first_name: Kaushik
  full_name: Mallik, Kaushik
  id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
  last_name: Mallik
  orcid: 0000-0001-9864-7475
- first_name: Anne-Kathrin
  full_name: Schmuck, Anne-Kathrin
  last_name: Schmuck
- first_name: Sadegh
  full_name: Soudjani, Sadegh
  last_name: Soudjani
citation:
  ama: Banerjee T, Majumdar R, Mallik K, Schmuck A-K, Soudjani S. Fast symbolic algorithms
    for mega-regular games under strong transition fairness. <i>TheoretiCS</i>. 2023;2.
    doi:<a href="https://doi.org/10.46298/theoretics.23.4">10.46298/theoretics.23.4</a>
  apa: Banerjee, T., Majumdar, R., Mallik, K., Schmuck, A.-K., &#38; Soudjani, S.
    (2023). Fast symbolic algorithms for mega-regular games under strong transition
    fairness. <i>TheoretiCS</i>. EPI Sciences. <a href="https://doi.org/10.46298/theoretics.23.4">https://doi.org/10.46298/theoretics.23.4</a>
  chicago: Banerjee, Tamajit, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck,
    and Sadegh Soudjani. “Fast Symbolic Algorithms for Mega-Regular Games under Strong
    Transition Fairness.” <i>TheoretiCS</i>. EPI Sciences, 2023. <a href="https://doi.org/10.46298/theoretics.23.4">https://doi.org/10.46298/theoretics.23.4</a>.
  ieee: T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, and S. Soudjani, “Fast
    symbolic algorithms for mega-regular games under strong transition fairness,”
    <i>TheoretiCS</i>, vol. 2. EPI Sciences, 2023.
  ista: Banerjee T, Majumdar R, Mallik K, Schmuck A-K, Soudjani S. 2023. Fast symbolic
    algorithms for mega-regular games under strong transition fairness. TheoretiCS.
    2, 4.
  mla: Banerjee, Tamajit, et al. “Fast Symbolic Algorithms for Mega-Regular Games
    under Strong Transition Fairness.” <i>TheoretiCS</i>, vol. 2, 4, EPI Sciences,
    2023, doi:<a href="https://doi.org/10.46298/theoretics.23.4">10.46298/theoretics.23.4</a>.
  short: T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, S. Soudjani, TheoretiCS
    2 (2023).
date_created: 2024-01-31T13:40:49Z
date_published: 2023-02-24T00:00:00Z
date_updated: 2024-02-05T10:21:51Z
day: '24'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.46298/theoretics.23.4
ec_funded: 1
external_id:
  arxiv:
  - '2202.07480'
file:
- access_level: open_access
  checksum: 2972d531122a6f15727b396110fb3f5c
  content_type: application/pdf
  creator: dernst
  date_created: 2024-02-05T10:19:35Z
  date_updated: 2024-02-05T10:19:35Z
  file_id: '14940'
  file_name: 2023_TheoretiCS_Banerjee.pdf
  file_size: 917076
  relation: main_file
  success: 1
file_date_updated: 2024-02-05T10:19:35Z
has_accepted_license: '1'
intvolume: '         2'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '02'
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: TheoretiCS
publication_identifier:
  issn:
  - 2751-4838
publication_status: published
publisher: EPI Sciences
quality_controlled: '1'
status: public
title: Fast symbolic algorithms for mega-regular games under strong transition fairness
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2
year: '2023'
...