Deciding Regular Games: a Playground for Exponential Time Algorithms

Regular games form a well-established class of games for analysis and synthesis of reactive systems. They include colored Muller games, McNaughton games, Muller games, Rabin games, and Streett games. These games are played on directed graphs 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 G into two sets Win₀ and Win₁ of winning positions for Player 0 and Player 1, respectively. Numerous algorithms exist that decide instances of regular games, e.g., Muller games, by computing Win₀ and Win₁. In this paper we aim to find general principles for designing uniform algorithms that decide all regular games. For this we utilize 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.

Recommended citation: Zihui Liang, Bakh Khoussainov, and Mingyu Xiao. Deciding Regular Games: a Playground for Exponential Time Algorithms. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 66:1-66:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.MFCS.2025.66
Download Paper