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 source 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 $\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.

翻译：我们研究了图上的两人博弈的不动点算法，其环境受强过渡公平性假设约束，获胜条件为ω-正则性质。强过渡公平性是强公平性的一种广泛存在的特例，要求任意执行关于指定活边集是强公平的：若一条活边的源顶点在博弈路径中被无限多次访问，则该边本身也需在路径中被无限多次遍历。令人惊讶的是，我们证明强过渡公平性保留了ω-正则博弈不动点算法的算法特性——新算法与经典算法具有相同的交替深度，但引入了新型前驱算子。对于含k对条件的Rabin博弈，新算法的复杂度为O(n^{k+2}k!)个符号步骤，该复杂度与强过渡公平性假设中的活边数量无关。进一步，我们证明含强过渡公平性假设的GR(1)规范可通过3层嵌套的不动点算法求解，与常规算法一致。相比之下，强公平性必然需要根据公平性假设数量增加交替深度。我们针对强过渡公平性假设下的（广义）Rabin、Parity和GR(1)目标提出了符号算法，并给出随机ω-正则博弈的定性胜符号算法，时间复杂度为O(n^{k+2}k!)个符号步骤，改进了现有最优结果。最后，我们基于所提算法实现了BDD综合引擎，在合成基准与真实基准上的实验表明，该算法具有可扩展性与可并行性，且性能较以往算法提升数个数量级。