Doubly Fair Parity Games

TL;DR

The paper introduces and analyzes doubly fair parity-type games where both players are constrained by fairness through a designated set of fair edges and two ω-regular objectives $\alpha$ and $\beta$. It proves determinacy and develops two solution paradigms: a gadget-based reduction turning fair games into standard parity games (with linear or quadratic blow-ups depending on the objectives) and a direct symbolic fixpoint approach that mirrors stochastic parity techniques. The main technical contributions include (i) a polynomial/linear reduction for $\alpha$ Büchi or parity with $\beta$ trivial, (ii) a quadratic reduction for parity/$\beta$ cases, and (iii) a direct symbolic algorithm yielding fixpoint characterizations for fair parity/Parity and similar games. These results unify and extend methods from fair/environmental games and stochastic parity games, enabling both practical solvers and deeper theoretical understanding of how mutual fairness influences strategy structure and memory requirements.

Abstract

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.

Figures (12)

• Figure 1: Deadlock caused by fairness constraints of two robots facing a door.
• Figure 2: A simple fair game arena discussed in \ref{['example:division-of-objectives']}.
• Figure 3: Four fair parity/$\beta$ games: dashed lines represent fair edges. Games $G_1$ and $G_4$ are won by $\exists$-player and $G_2$ and $G_3$ are won by $\forall$-player. In each case, a respective winning strategy is shown by colored edges. A set of colored edges represents a strategy that takes only the colored edges in the game, and whenever a source node is visited infinitely often, all its colored outgoing edges are taken alternatingly.
• Figure 4: Existential gadgets that replace $v \in V^{\mathsf{fair}}_\exists$ (left) and $v \in V^{\mathsf{fair}}_\forall$ (right) in the fair Büchi/$\bot$ game.
• Figure 5: Universal gadgets that replace $v \in V^{\mathsf{fair}}_\exists$ (left) and $v \in V^{\mathsf{fair}}_\forall$ (right) in the fair Büchi/$\bot$ game.

Theorems & Definitions (42)

• lemma 1
• proof
• lemma 2
• proof
• definition 1: Fair Games
• remark 1
• remark 2
• remark 2
• theorem 1
• remark 3