Return
Exponential time algorithms for deciding regular games
DOI:10.1016/j.ic.2026.105443.png)
Abstract
En 中文
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 c, where Player 0 and Player 1 construct an infinite path p through c. The outcome is determined by the set X of vertices visited infinitely often along p. Regular games are determined, meaning the graph c can be partitioned into two sets, Win0(c) and Win1(c), 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.
Keywords:
Regular games
Colored Muller games
Rabin games
McNaughton games
Muller games
Deciding games
Journal
I
IF:
1
Papers:
79
Citations:
2.8K

