We consider two-player games over finite graphs in which both players are restricted by fairness constraints on their moves. Given a two player game graph $G=(V,E)$ and a set of fair moves $E_f\subseteq E$ a player is said to play "fair" in $G$ if they choose an edge $e \in E_f$ infinitely often whenever the source vertex of $e$ is visited infinitely often. Otherwise, they play "unfair". We equip such games with two $ω$-regular winning conditions $α$ and $β$ deciding the winner of mutually fair and mutually unfair plays, respectively. Whenever one player plays fair and the other plays unfair, the fairly playing player wins the game. The resulting games are called "fair $α/β$ games". We formalize fair $α/β$ games and show that they are determined. For fair parity/parity games, i.e., fair $α/β$ games where $α$ and $β$ are given each by a parity condition over $G$, we provide a polynomial reduction to (normal) parity games via a gadget construction inspired by the reduction of stochastic parity games to parity games. We further give a direct symbolic fixpoint algorithm to solve fair parity/parity games. On a conceptual level, we illustrate the translation between the gadget-based reduction and the direct symbolic algorithm which uncovers the underlying similarities of solution algorithms for fair and stochastic parity games, as well as for the recently considered class of fair games where only one player is restricted by fair moves.
翻译:我们考虑有限图上的双人博弈,其中双方玩家的行动均受公平性约束。给定一个双人博弈图 $G=(V,E)$ 和一个公平移动集 $E_f\subseteq E$,若玩家在源顶点被无限次访问时,无限频繁地选择边 $e \in E_f$,则称其在 $G$ 中"公平"游戏;否则称为"不公平"游戏。我们为这类博弈配备两个 $\omega$-正则获胜条件 $\alpha$ 和 $\beta$,分别决定双方公平博弈与双方不公平博弈的胜者。当一方公平另一方不公平游戏时,公平方获胜。由此产生的博弈称为"公平 $\alpha/\beta$ 博弈"。我们形式化定义了公平 $\alpha/\beta$ 博弈,并证明其具有确定性。针对公平奇偶/奇偶博弈(即 $\alpha$ 和 $\beta$ 均由 $G$ 上的奇偶条件给出的公平 $\alpha/\beta$ 博弈),我们通过受随机奇偶博弈向奇偶博弈归约启发的小工具构造,给出了到(标准)奇偶博弈的多项式归约。进一步地,我们设计了直接求解公平奇偶/奇偶博弈的符号化不动点算法。在概念层面,我们阐释了基于小工具的归约与直接符号算法之间的转换关系,揭示了公平博弈与随机奇偶博弈求解算法以及近期提出的仅单方受公平移动约束的公平博弈之间的内在相似性。