Deciding regular games: a playground for exponential time algorithms
Zihui Liang, Bakh Khoussainov, Mingyu Xiao
TL;DR
The paper addresses the challenge of designing uniform, efficient algorithms for deciding all regular games (including coloured Muller, Rabin, Streett, Muller, and McNaughton games) on arenas. It introduces the full-win concept and key structural lemmas, then develops two algorithmic families: recursive solvers and dynamic programming (DP) approaches. The DP framework yields concrete algorithms (Algorithm 1 and Algorithm 2) for coloured Muller games and extends to Muller and McNaughton games, via efficient representations and an Enumeration Lemma to support KL-to-Muller transformations. It also shows how Rabin/Streett/KL games can be reduced to Muller form or handled directly within the DP scheme, producing competitive time/space bounds and revealing regimes where these uniform DP methods outperform traditional instance-specific algorithms. The work thus provides uniform, scalable techniques for a broad class of regular games with practical implications for verification and synthesis of reactive systems.
Abstract
Regular games form a well-established class of games for analysis and synthesis of reactive systems. They include coloured Muller games, McNaughton games, Muller games, Rabin games, and Streett games. 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 specifications put on the set $X$ of vertices in $ρ$ that occur infinitely often. 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 specific instances of regular games, e.g., Muller games, by computing $W_0$ and $W_1$. In this paper we aim to find general principles for designing uniform algorithms that decide all regular games. For this we utilise various recursive and dynamic programming algorithms that leverage standard notions such as subgames and traps. Importantly, we show that our techniques improve or match the performances of existing algorithms for many instances of regular games.