M\"uller games form a well-established class of games for model checking and verification. These games are played on directed graphs $\mathcal G$ where Player 0 and Player 1 play by generating an infinite path through the graph. The winner is determined by the set $X$ consisting of all vertices in the path that occur infinitely often. If $X$ belongs to $\Omega$, a specified collection of subsets of $\mathcal G$, then Player 0 wins. Otherwise, Player 1 claims the win. These games are determined, enabling the partitioning of $\mathcal G$ into two sets $W_0$ and $W_1$ of winning positions for Player 0 and Player 1, respectively. Numerous algorithms exist that decide M\"uller games $\mathcal G$ by computing the sets $W_0$ and $W_1$. In this paper, we introduce two novel algorithms that outperform all previously known methods for deciding explicitly given M\"uller games, especially in the worst-case scenarios. The previously known algorithms either reduce M\"uller games to other known games (e.g. safety games) or recursively change the underlying graph $\mathcal G$ and the collection of sets in $\Omega$. In contrast, our approach does not employ these techniques but instead leverages subgames, the sets within $\Omega$, and their interactions. This distinct methodology sets our algorithms apart from prior approaches for deciding M\"uller games. Additionally, our algorithms offer enhanced clarity and ease of comprehension. Importantly, our techniques are applicable not only to M\"uller games but also to improving the performance of existing algorithms that handle other game classes, including coloured M\"uller games, McNaughton games, Rabin games, and Streett games.

翻译：Müller游戏是一类用于模型检测和验证的经典博弈。这类游戏在有向图$\mathcal G$上进行，玩家0和玩家1通过生成图中的无限路径进行博弈。胜负由路径中无限次出现的所有顶点构成的集合$X$决定：若$X$属于$\Omega$（$\mathcal G$的指定子集族），则玩家0获胜；否则玩家1获胜。这类游戏是确定的，使得$\mathcal G$可划分为玩家0的获胜位置集$W_0$和玩家1的获胜位置集$W_1$。现有多种算法通过计算$W_0$和$W_1$来求解Müller游戏$\mathcal G$。本文提出两种新算法，在处理显式给定的Müller游戏时（尤其在最坏情况下），其性能优于所有已知方法。现有算法要么将Müller游戏转化为其他已知游戏（如安全游戏），要么递归修改底层图$\mathcal G$及$\Omega$中的子集族。相比之下，我们的方法不采用这些技术，而是利用子游戏、$\Omega$中的子集及其交互关系。这种独特的求解方法论使我们提出的算法区别于所有先前的Müller游戏求解方法。此外，我们的算法具有更优的清晰度和易理解性。更重要的是，这些技术不仅适用于Müller游戏，还可用于改进处理其他博弈类（包括着色Müller游戏、McNaughton游戏、Rabin游戏和Streett游戏）的现有算法性能。