强转移公平下Omega正则游戏的快速符号算法
Fast Symbolic Algorithms for Omega-Regular Games under Strong Transition Fairness
AI总结：
本文提出强转移公平下求解ω-正则游戏的新型不动点符号算法，保持交替深度不变，复杂度O(n^{k+2}k!)，并实现BDD综合引擎，性能优于现有算法。
摘要：
我们考虑在具有$ω$-正则获胜条件的图上的双人游戏的不动点算法，其中环境受到强转移公平假设的约束。强转移公平是强公平的一种广泛出现的特殊情况，它要求任何执行相对于指定的活边集合是强公平的：每当沿着一条博弈路径无限多次访问活边的源顶点时，该边本身也必须沿着该路径无限多次被遍历。我们令人惊讶地表明，强转移公平保留了$ω$-正则游戏的不动点算法的算法特征——新算法与经典算法具有相同的交替深度，但调用了一种新型的前驱算子。对于具有$k$对的Rabin游戏，新算法的复杂度为$O(n^{k+2}k!)$符号步，这与强转移公平假设中的活边数量无关。进一步，我们表明具有强转移公平假设的GR(1)规范可以用3层嵌套的不动点算法求解，与通常的算法相同。相比之下，强公平必然需要根据公平假设的数量增加交替深度。我们得到了在强转移公平假设下针对（广义）Rabin、parity和GR(1)目标的符号算法，以及一个直接用于随机$ω$-正则游戏中定性获胜的符号算法，其运行时间为$O(n^{k+2}k!)$符号步，改进了现有技术水平。最后，我们实现了一个基于BDD的综合引擎，基于我们的算法。我们在一组合成和真实基准上展示了我们的算法是可扩展的、可并行化的，并且比之前的算法快几个数量级。
英文摘要：
We consider fixpoint algorithms for two-player games on graphs with $ω$-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 $ω$-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 $ω$-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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
