AI 中文总结
本研究阐释通用树与Zielonka树在Streett、Emerson-Lei博弈求解中的作用，改进其复杂度，生成内存最优策略，并优化Zielonka-McNaughton算法的符号实现。
AI 中文摘要
近十年前，Calude等人证明了奇偶博弈可在拟多项式时间内求解，该结果如今可通过通用树（universal trees）来阐释。通过归约到奇偶博弈，这一拟多项式结果可推广至所有ω-正则博弈。然而，除这类归约及Rabin博弈外，学界对通用树在直接求解博弈中的作用仍知之甚少。本研究反驳了通用树仅与存在无记忆获胜策略的博弈相关的普遍观点，全面阐释了通用树与Zielonka树在求解Streett博弈和Emerson-Lei博弈中的相互作用。据此，我们证明：顶点数为n、边数为m、对偶数为k的Streett博弈，其获胜区域与策略可在时间O(mk log(k)k!|U(n,k)|)内计算，其中U(n,k)为具有n个叶节点、深度为k的通用树，该结果优于此前依赖归约到奇偶博弈及其拟多项式求解的最优复杂度结果。进一步地，顶点数为n、边数为m、颜色数为c的Emerson-Lei博弈，其获胜区域与策略可在时间O(mc log(c)c!|U(n,c/2)|)内计算，同样优于归约到奇偶博弈的方法。值得注意的是，与归约到奇偶博弈得到的策略不同，本方法可生成内存最优策略。最后，我们展示了如何利用通用树约束求解Emerson-Lei博弈的Zielonka-McNaughton算法的递归树，从而得到一种符号算法，将现有符号方法时间复杂度中的因子n^c替换为|U(n,c)|。
英文摘要
Nearly a decade ago, Calude et al. showed that parity games can be solved in quasi-polynomial time. This result is now understood in terms of universal trees. By reduction to parity games, the quasi-polymonial result can benefit all omega-regular games. However, beyond such reductions, and with the exception of Rabin games, our understanding of the role of universal trees in direct solutions is still quite limited. In this work, we refute the common view that universal trees are relevant only for games that admit memoryless winning strategies. We contribute a full understanding of how universal trees interact with Zielonka trees for the solution of Streett and Emerson-Lei games. As a consequence, we show that winning regions and strategies in Streett games with $n$ vertices, $m$ edges, and $k$ pairs can be computed in time $O(mk\log(k)k!|U(n,k)|)$, where $U(n,k)$ is a universal tree for $n$ leaves and depth $k$. This improves upon the best previously known complexity result for Streett games, which relied on reduction to parity games and their quasi-polynomial solution. Furthermore, we show that winning regions and strategies for Emerson-Lei games with $n$ vertices, $m$ edges, and $c$ colors can be computed in time $O(mc\log(c)c!|U(n,c/2)|)$, again improving over reductions to parity games. Notably, our approach yields memory-optimal strategies, in contrast to those obtained via reductions to parity games. Finally, we show how universal trees can be used to bound the recursion tree of the Zielonka-McNaughton algorithm for Emerson-Lei games. This leads to a symbolic algorithm that replaces the factor $n^c$ in the time complexity of existing symbolic approaches with $|U(n,c)|$.
