Speaker:

Zihui Liang (University of Electronic Science and Technology of China)

Time:

• 16:20-17:20 (Time in Beijing)
• March 22, 2024 (Friday)

Venue:

518, Research Building 4

Abstract:

Muller 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 Muller 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 Muller games, especially in the worst-case scenarios. The previously known algorithms either reduce Muller 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 Muller games. Additionally, our algorithms offer enhanced clarity and ease of comprehension. Importantly, our techniques are applicable to improving the performance of existing algorithms that handle other game classes, including coloured Muller games, McNaughton games, Rabin games, and Streett games..