Deciding regular games: a playground for exponential time algorithms

TL;DR

This paper explores general principles for designing uniform algorithms to decide all regular games, using recursive and dynamic programming techniques that improve or match existing algorithms' performance.

Contribution

It introduces a unified approach leveraging recursive and dynamic programming methods to decide regular games efficiently across various types.

Findings

Techniques improve existing algorithms for many regular game instances.

Unified principles enable decision-making for all regular games.

Performance matches or exceeds current algorithms.

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 $\rho$ through the graph. The winner is determined by specifications put on the set $X$ of vertices in $\rho$ 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.