Deciding regular games: a playground for exponential time algorithms

正则游戏是一类已经被广泛研究的反应式系统分析和合成的游戏。它包括彩色Muller游戏、McNaughton游戏、Muller游戏、Rabin游戏和Streett游戏。这些游戏是在有向图 $\mathcal G$ 上进行的，玩家0和玩家1通过在图中生成一个无限路径 $\rho$ 进行游戏。胜者由对出现无限次的 $\rho$ 中的顶点集合 $X$ 施加的规范来确定。这些游戏是确定的，可以将 $\mathcal G$ 分成两个集合 $W_0$ 和 $W_1$，分别表示玩家0和玩家1的获胜位置。存在许多算法来决定特定实例的正则游戏，例如Muller游戏，通过计算 $W_0$ 和 $W_1$。在本文中，我们旨在找到设计统一算法以决定所有正则游戏的通用原则。为此，我们利用各种递归和动态规划算法，利用子游戏和陷阱等标准概念。重要的是，我们展示了我们的技术在许多正则游戏实例的性能方面要么提高了要么与现有算法相匹配。

设计一种通用算法来决定所有正则游戏，这是否是一个新问题？

通过利用子游戏和陷阱等标准概念，利用各种递归和动态规划算法来解决正则游戏，提出通用算法的设计原则。

论文展示了如何设计通用算法来解决正则游戏，并且证明了这些技术可以提高现有算法的性能。实验设计合理，使用了多个数据集，并且开源了代码。

最近的相关研究包括颜色Muller游戏、McNaughton游戏、Muller游戏、Rabin游戏和Streett游戏。