Two new algorithms for solving M\"uller games and their applications
arXiv (Cornell University)(2023)
摘要
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.
更多查看译文
关键词
new algorithms
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要