AI summaryⓘ
The authors study the role of universal trees in solving complex types of games called Streett and Emerson-Lei games, which are used in computer science for modeling decision making. They challenge the previous belief that universal trees only help with games where players don’t need memory to win. By combining universal trees with another concept called Zielonka trees, they develop faster algorithms that improve upon earlier methods, especially compared to approaches based on reducing these games to parity games. Their new algorithms also produce strategies that use the least amount of memory possible. Additionally, they create a more efficient symbolic algorithm for solving Emerson-Lei games using universal trees.
parity gamesuniversal treesStreett gamesEmerson-Lei gamesZielonka treesmemoryless strategiesomega-regular gamesalgorithm complexitysymbolic algorithm
Abstract
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)|$.