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.

翻译：暂无翻译