Exponential time algorithms for deciding regular games

Regular games constitute a fundamental class used in the analysis and synthesis of reactive systems. This class includes 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 construct an infinite path ρ through G. The outcome is determined by the set X of vertices visited infinitely often along ρ. Regular games are determined, meaning the graph G can be partitioned into two sets, W i n 0 ( G ) and W i n 1 ( G ), representing the winning positions for Player 0 and Player 1, respectively. Various algorithms exist for specific types of regular games that compute these sets. In this paper, we seek general principles for designing algorithms that solve all regular games. Our approach relies on recursive and dynamic programming techniques that make use of standard concepts such as subgames and traps. We demonstrate that our methods match or improve upon the performance of existing algorithms for all regular games mentioned above.

Authors

• Zihui Liang
• Bakh Khoussainov University of Electronic Science and Technology of China
• Mingyu Xiao

Keywords

• Regular games
• Colored Muller games
• Rabin games
• McNaughton games
• Muller games
• Deciding games