{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T23:33:44Z","timestamp":1768347224796,"version":"3.49.0"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2023,2,24]],"date-time":"2023-02-24T00:00:00Z","timestamp":1677196800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We consider fixpoint algorithms for two-player games on graphs with\n$\\omega$-regular winning conditions, where the environment is constrained by a\nstrong transition fairness assumption. Strong transition fairness is a widely\noccurring special case of strong fairness, which requires that any execution is\nstrongly fair with respect to a specified set of live edges: whenever the\nsource vertex of a live edge is visited infinitely often along a play, the edge\nitself is traversed infinitely often along the play as well. We show that,\nsurprisingly, strong transition fairness retains the algorithmic\ncharacteristics of the fixpoint algorithms for $\\omega$-regular games -- the\nnew algorithms have the same alternation depth as the classical algorithms but\ninvoke a new type of predecessor operator. For Rabin games with $k$ pairs, the\ncomplexity of the new algorithm is $O(n^{k+2}k!)$ symbolic steps, which is\nindependent of the number of live edges in the strong transition fairness\nassumption. Further, we show that GR(1) specifications with strong transition\nfairness assumptions can be solved with a 3-nested fixpoint algorithm, same as\nthe usual algorithm. In contrast, strong fairness necessarily requires\nincreasing the alternation depth depending on the number of fairness\nassumptions. We get symbolic algorithms for (generalized) Rabin, parity and\nGR(1) objectives under strong transition fairness assumptions as well as a\ndirect symbolic algorithm for qualitative winning in stochastic\n$\\omega$-regular games that runs in $O(n^{k+2}k!)$ symbolic steps, improving\nthe state of the art. Finally, we have implemented a BDD-based synthesis engine\nbased on our algorithm. We show on a set of synthetic and real benchmarks that\nour algorithm is scalable, parallelizable, and outperforms previous algorithms\nby orders of magnitude.<\/jats:p>","DOI":"10.46298\/theoretics.23.4","type":"journal-article","created":{"date-parts":[[2023,2,27]],"date-time":"2023-02-27T19:15:37Z","timestamp":1677525337000},"source":"Crossref","is-referenced-by-count":10,"title":["Fast Symbolic Algorithms for Omega-Regular Games under Strong Transition Fairness"],"prefix":"10.46298","volume":"Volume 2","author":[{"given":"Tamajit","family":"Banerjee","sequence":"first","affiliation":[]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[]},{"given":"Kaushik","family":"Mallik","sequence":"additional","affiliation":[]},{"given":"Anne-Kathrin","family":"Schmuck","sequence":"additional","affiliation":[]},{"given":"Sadegh","family":"Soudjani","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2023,2,24]]},"container-title":["TheoretiCS"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/theoretics.episciences.org\/9876\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/theoretics.episciences.org\/9876\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T10:12:17Z","timestamp":1687255937000},"score":1,"resource":{"primary":{"URL":"https:\/\/theoretics.episciences.org\/9088"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,2,24]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/theoretics.23.4","relation":{"has-preprint":[{"id-type":"arxiv","id":"2202.07480v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2202.07480","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2202.07480","asserted-by":"subject"}]},"ISSN":["2751-4838"],"issn-type":[{"value":"2751-4838","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,2,24]]},"article-number":"9088"}}