Rabin Games Revisited

Rabin games have their roots in Michael Rabin's seminal work on automata over infinite trees and form a classical model for infinite-round games with ω-regular winning conditions.They play a central role in automata theory and temporal synthesis: translating an LTL specification into an equivalent deterministic Rabin automaton reduces synthesis to solving a Rabin game.In practice, however, Rabin games are typically solved indirectly, via parity games.One possible reason is that many direct algorithms have a factorial dependence on the Rabin index k, the number of Rabin pairs.In this work, we revisit Rabin's 1972 recursive algorithm.The algorithm is implicit in Rabin's proof and intertwined with finite-state determinacy.First, we "excavate" it as an explicit arenabased solver using standard reachability-and Büchi-game solving as basic building blocks, thus avoiding the exponential dependence on the alphabet in Rabin's original presentation.Second, we show that memoization removes the factorial term from the recursion-tree analysis.Finally, we introduce a variation that recurses on the Rabin index.These results provide a modern analysis of Rabin's recursive method and a basis for studying direct Rabin-game solvers for temporal synthesis.