---
res:
  bibo_abstract:
  - "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.@eng"
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Tamajit
      foaf_name: Banerjee, Tamajit
      foaf_surname: Banerjee
  - foaf_Person:
      foaf_givenName: Rupak
      foaf_name: Majumdar, Rupak
      foaf_surname: Majumdar
  - foaf_Person:
      foaf_givenName: Kaushik
      foaf_name: Mallik, Kaushik
      foaf_surname: Mallik
      foaf_workInfoHomepage: http://www.librecat.org/personId=0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
    orcid: 0000-0001-9864-7475
  - foaf_Person:
      foaf_givenName: Anne-Kathrin
      foaf_name: Schmuck, Anne-Kathrin
      foaf_surname: Schmuck
  - foaf_Person:
      foaf_givenName: Sadegh
      foaf_name: Soudjani, Sadegh
      foaf_surname: Soudjani
  bibo_doi: 10.46298/theoretics.23.4
  bibo_volume: 2
  dct_date: 2023^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/2751-4838
  dct_language: eng
  dct_publisher: EPI Sciences@
  dct_title: Fast symbolic algorithms for mega-regular games under strong transition
    fairness@
...