Fair $\omega$-Regular Games

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 node of e is visited infinitely often. Otherwise, they play unfair. We equip such games with two $\omega$-regular winning conditions $\alpha$ and $\beta$ 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 $\alpha /\beta$ games.

We formalize fair $\alpha /\beta$ games and show that they are determined. For fair parity/parity games, i.e., fair $\alpha /\beta$ games where $\alpha$ and $\beta$ 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 in which only one player is restricted by fair moves.

Supported by the ERC Consolidator grant D-SynMA (No. 772459).

Supported by the DFG project SCHM 3541/1-1.

1 Introduction

Omega-regular games are a popular abstract modelling formalism for many core computational problems in the context of correct-by-construction synthesis of reactive software or hardware. This abstract view was initiated by the seminal work of Church [8] and its independent solutions by Büchi and Landweber and Rabin [5, 18]. Since then these ideas have been refined and extended for solving the reactive synthesis problems [14, 17, 20].

However, before using any such synthesis technique, the reactive software design problem at hand needs to be abstractly modelled as a two-player game. In order for the subsequently synthesized software to be ‘correct-by-construction’ this game graph needs to reflect all possible interactions between involved components in an abstract manner. Building such a game graph with the ‘right’ level of abstraction is a known severe challenge, in particular, if the synthesized software is interacting with existing components that already possess certain behavior. Here, part of the modelling challenge amounts to finding the ‘right’ power of both players in the resulting abstract game to ensure that winning strategies do not fail to exist due to an unnecessarily conservative overapproximation of modeling uncertainty (or the dual problem due to underapproximation).

In this context, fairness has been adopted as a notion to abstractly model known characteristics of the involved components in a very concise manner. Fairness assumptions have been used in model checking [1] and scheduler synthesis for the classical AMBA arbiter [16] or shared resource management [6]. Notably, fairness assumptions have also gained attention in cyber-physical system design [11, 15, 21] and robot motion planning [2, 9]. In all these applications, fairness is used as an assumption that the synthesized (or verified) component can rely on. In particular, if these assumptions are modelled by transition fairness over a two-player game arena¹ $(V_\forall ,V_\exists ,E)$ – i.e., by a set of fair environment moves $E_f\subseteq E$ (i.e., with $V_\forall$ as their domain) that need to be taken infinitely often if the source node is seen infinitely often along a play – the resulting synthesis games can be solved efficiently [4, 19].

While most existing work has only looked at fairness as an assumption to weaken the opponent in the synthesis game, all mentioned applications also naturally allow for scenarios where multiple components with intrinsically fair behavior are interacting with each other in a non-trivial manner. For example, the ability of a concurrent process to eventually free a shared resource might depend on how fair re-allocation is implemented in other threads. On an abstract level, the formal reasoning about such scenarios requires to understand how the interactive decision making of two dependent processes is influenced by intrinsic fairness constraints imposed on their decisions. Algorithmically, these synthesis questions require fairness restrictions on both players in a game, i.e., do not restrict the domain of fair moves $E_f$ to one player only. We refer to such games simply as fair games.

Motivating Example. In order to better illustrate the challenges arising from solving such fair games, consider two robots in a shared workspace with narrow passages between adjacent regions that only one robot can pass at a time. One robot (say the green one) has an $\omega$-regular objective $\alpha$ that specifies desired sequences of visited regions in the workspace. The other (red) robot tries to prevent the green robot from achieving this sequence. In order to rule out trivial spoiling strategies of the red robot, both robots need to implement a tie-breaking mechanism for obstacle avoidance, i.e., they must eventually move left or right if an obstacle blocks their way.

Now consider the scenario where both robots are facing each other at a gate, as depicted in Fig. 1. While both robots block the gate from one side, neither of them can move forward, but if the green robots moves left or the red robot moves right, the other robot can take the gate to reach region A. With the mentioned requirement for tie-breaking, none of the robots is allowed to block the gate forever and both eventually have to move to the side.

Fig. 1.

Deadlock caused by fairness constraints of two robots facing a door.

Now let us assume that region A is important for both robots, hence, both robots have an incentive to enter region A first, to then move the game to an area preferable to them. However, the robot who breaks the tie first, (i.e., fulfills its fairness condition first) allows the other robot to enter region A first, which gives both robots the incentive to behave unfair. While it is very intuitive to make a player lose when she plays unfair and the other player plays fair, it is unclear who wins the game if both players play unfair.

To resolve this issue, we can make the objectives of the robots completely adversarial by assigning one of the players (say, green) the winner in a play where both players play unfair. In the above example, this would give the red robot the incentive to break the tie first. While this makes it harder for the red robot to spoil the objective of the green one, we might be interested in a more symmetric game which does not favor the green robot in all non-determined states of the graph. We therefore consider a second $\omega$-regular objective $\beta$ that determines the winner of (mutually) unfair plays. This results in fair games $G=(A,\alpha ,\beta )$ which are determined (as shown in Sec. 3).

Contribution. Motivated by the above mentioned examples where interactive decision making of two dependent processes is influenced by intrinsic fairness constraints imposed on their decisions, this paper studies fair games $G=(A,\alpha ,\beta )$ as their abstraction. In particular, we give solution algorithms for these games when both $\alpha$ and $\beta$ are parity conditions induced by two different priority functions over the node set. We call such games fair parity/parity games.

Obviously, the previously discussed one-sided version of fair games, which we call $\forall$-fair games (as only the $\forall$-player (i.e., the environment) is restricted by strong transition fairness), is a special case of fair games. Both enumerative [19] and symbolic solution algorithms [4] have recently been proposed for $\forall$-fair games, showing that strong transition fairness can be handled efficiently in both types of algorithms. This observation is closely related to a result for stochastic games, i.e., two-player games with an additional ‘half’ player that takes all its moves uniformly at random. For the purpose of qualitative analysis, such stochastic parity games have been shown in [7] to be reducible to (standard) parity games by the use of “gadgets” that turn stochastic nodes into a small sequence of $\forall$- and $\exists$-player nodes. While it is known that stochastic games can be reduced to $\forall$-fair games (and hence, fair games), it was not investigated how the different solution approaches compare. The main conceptual contribution of this paper is a unified understanding of all these solution approaches for the general class of fair games.

Concretely, our contribution is three-fold:

• (1) We formalize fair games as a generalization of $\forall$-fair games and stochastic games such that they are determined.

• (2) We show a reduction of fair parity/parity games to (standard) parity games, inspired by the gadget-based reduction of stochastic parity games to parity games in [7]. This reduction enables the use of parity game solvers over the reduced game (in particular enumerative ones such as Zielonka’s algorithm [24]) and gives a gadget-based reduction of $\forall$-fair parity games to parity games as a corollary.

• (3) We then show how our gadget construction can be used to define a symbolic fixpoint algorithm to solve fair parity/parity games directly (without the need for a reduction). We show the direct symbolic algorithm for $\forall$-fair parity games in [4] coinciding with our algorithm for this particular subclass of fair games.

With this, we believe that this paper uncovers the underlying similarities of solution algorithms for fair, $\forall$-fair and stochastic parity games. Further, we show how these conceptual similarities can be used to build both enumerative and direct symbolic algorithms. This is of interest as both are known to have complementary strengths, depending on how the synthesis instance is provided, and this connection was, to the best of our knowledge, not known before.

All omitted proofs are available in the extended version of this paper [10].

2 Preliminaries

We introduce infinite-duration $\omega$-regular two-player games over finite graphs with additional strong transition fairness conditions on both players. For readability, we call the considered games (and their respective notions) simply fair.

Infinite Sequences. We denote the set of infinite sequences over a set U by $U^\omega$. We often view sequences $\tau =u_1u_2\ldots \in U^\omega$ as functions $\tau :\mathbb {N}\rightarrow U$, writing $\tau (i)=u_i$. Furthermore, we let $\textsf{Inf}(\tau ):=\{u\in U\mid \forall i.\, \exists j>i.\, \tau (j)=u\}$ denote the set of elements of U that occur infinitely often in $\tau$. Given a function $f:U \rightarrow W$, we denote by $f(\tau )\in W^\omega$ the pointwise application of f to $\tau$. Given a natural number n, we write $[n]:=\{1,\ldots ,n\}$.

Fair Game Arenas. A fair game arena $A=(V_\exists ,V_\forall ,E,E_f)$ consists of a set of nodes $V=V_\exists \cup V_\forall$ that is partitioned into the sets of existential nodes $V_\exists$ and universal nodes $V_\forall$, together with a set $E\subseteq V\times V$ of moves that is partitioned into the set $E_f\subseteq E$ of fair moves and the set $E\setminus E_f$ of normal moves. If $E_f=\emptyset$, then we sometimes omit this component for brevity. Given a node $v\in V$ and a binary relation $R\subseteq V\times V$, we write R(v) to denote the set $\{w\in V\mid (v,w)\in R\}$. We assume that E is right-total, that is, $E(v)\ne \emptyset$ for all $v\in V$. We call a node v fair, if it is the source node of a fair edge, i.e., $E_f(v)\ne \emptyset$ and collect all fair nodes in the set $V^{\textsf{fair}}=\{v \in V~|~ E_f(v)\ne \emptyset \}$ and define $V^{\textsf{n}}=V\setminus V^{\textsf{fair}}$ to be the set of nodes that are not fair (‘normal nodes’). We denote $V^{\textsf{fair}}_\exists =V^{\textsf{fair}}\cap V_\exists$ and $V^{\textsf{fair}}_\forall = V^{\textsf{fair}}\cap V_\forall$.

Plays. A play $\tau =v_0v_1\ldots$ on A is an infinite sequence of nodes s.t. $v_{i+1}\in E(v_i)$ for all $i\ge 0$. Given a play $\tau =v_0v_1\ldots$, we define the associated sequence of moves $\tau _m=(v_0,v_1)(v_1,v_2)\ldots$. Additionally, if i is a player in $\{\exists , \forall \}$, we denote the other player by $1-i$. We let $\textsf{plays}(A)$ denote the set of all plays on A.

For a player $i\in \{\exists ,\forall \}$, a play $\tau$ is i-fair if for all nodes $v\in V_i\cap \textsf{Inf}(\tau )$ holds that ${E_f}|_v \subseteq \textsf{Inf}(\tau _m)$, where ${E_f}|_v=\{(v,v')\in E_f\mid v'\in V\}$ denotes the set of fair edges that start at $v\in V$. Given a play $\tau$, we write $\textsf{fair}_i(\tau )$ to indicate that $\tau$ is i-fair. We call a play mutually fair if it is both $\exists$- and $\forall$-fair and mutually unfair if it is neither $\exists$- nor $\forall$-fair.

Strategies. A strategy for player $i \in \{\exists , \forall \}$ (or, an i-strategy) is a function $p : V^*\cdot V_i \rightarrow V$ where for each $u \cdot v \in V^* \cdot V_i$ it holds that $p(u \cdot v) \in E(v)$. A strategy p is called positional if $p(u\cdot v) = p(w \cdot v)$ for all $u, w \in V^*$ and $v \in V_i$.

A strategy p for player i is said to admit a play $\tau =v_0v_1\ldots$ if for all $k \in \mathbb {N}$, $v_k \in V_i$ implies $p(v_0 \ldots v_k) = v_{k+1}$. Alternatively, $\tau$ is said to be compliant with p. We write $\varSigma$ for the set of $\exists$-strategies and $\varPi$ for the set of $\forall$-strategies. Starting from a node $v \in V$, any two strategies $s\in \varSigma$ and $t\in \varPi$ induce a unique play $\textsf{play}_v(s,t)$ in the game arena. If we do not care about the initial node of the play, we simply write $\textsf{play}(s,t)$.

A strategy for player $i \in \{\exists , \forall \}$ is an i-fair strategy if every play it admits is i-fair. We write $\varSigma ^\textsf{fair}$ (resp. $\varPi ^\textsf{fair}$) for the set of $\exists$-fair (resp. $\forall$-fair) strategies.

Omega-regular Winning Conditions. We consider winning conditions given by an $\omega$-regular [13, 22] language $\varphi \subseteq V^\omega$ over the node set V. In particular, we write $\varphi =\bot$ and $\varphi =\top$ to denote the trivial winning conditions $\emptyset$ and $V^\omega$, respectively. In particular, we focus our attention to parity winning conditions. For a priority function $\lambda : V \rightarrow [k]$ that maps nodes of a game arena to the natural numbers bounded by k for some $k \in \mathbb {N}$, the Parity$(\lambda )$ condition is given via $\varphi = \{\tau \in V^\omega \mid \max (\textsf{Inf}(\lambda (\tau ))) \text { is even}\}$.

Omega-regular Games. An $\omega$-regular game is traditionally defined via a tuple $G = (A, \alpha )$ where A is a game arena without fair edges, i.e. $E_f = \emptyset$ and $\alpha \subseteq V^\omega$ an $\omega$-regular winning condition. An $\exists$-strategy $s \in \varSigma$ is said to be winning (for $\exists$) from a node $v \in V$, if for all $t \in \varPi$, $\textsf{play}_v(s, t) \in \alpha$. Dually, a $\forall$-strategy $t \in \varPi$ is said to be winning (for $\forall$) from a node $v \in V$, if for all $s \in \varSigma$, $\textsf{play}_v(s, t) \not \in \alpha$. In $\omega$-regular games, every node $v\in V$ is won by one and only one of the players [12, 13]. This property of a game is called determinacy, and $\omega$-regular games are determined. We denote the nodes from which $\exists$ (resp. $\forall$) has a winning strategy in G by $\textsf{Win}_\exists (G)$ (resp. $\textsf{Win}_\forall (G)$). When G is clear from the context, we drop the parenthesis and write $\textsf{Win}_\exists$ and $\textsf{Win}_\forall$ instead. Determinacy then amounts to $\textsf{Win}_\exists \cup \textsf{Win}_\forall =V$ and $\textsf{Win}_\exists \cap \textsf{Win}_\forall =\emptyset$.

Node Conventions for Figures. Throughout this paper, in all figures, the rectangular nodes represent $\forall$-player nodes and the nodes with round corners represent $\exists$-player nodes.

3 Fair Games

As already outlined in the motivating example in Sec. 1, the interpretation of winning conditions over fair games influences the characteristics of resulting winning strategies. To formalize this intuition, we will first recall a particular subclass of fair games, namely those where only one player is restricted by an additional fairness condition, in Subsec. 3.1. We will then use these games to motivate winning semantics for the general class of fair games.

3.1 Determinacy of $\forall$-Fair Games

A $\forall$-fair game is a tuple $G = (A, \alpha )$ where A is a game arena with $V^{\textsf{fair}}\subseteq V_\forall$ (called a $\forall$-fair game arena), and $\alpha$ is an $\omega$-regular winning condition.

In $\forall$-fair games, fairness constraints typically model known behavior of existing components that the $\exists$-player (i.e., the to be synthesized system) can rely on. This is formalized by defining that the $\exists$-player wins a $\forall$-fair game with winning condition $\alpha$ from node v if

$$\begin{aligned} \exists s \in \varSigma .\, \forall t \in \varPi ^\textsf{fair}. \, \textsf{play}_v(s, t) \in \alpha . \end{aligned}$$

(1a)

That is, $\exists$-player (or shortly, $\exists$) wins if they have a strategy that can win against all $\forall$-fair $\forall$-strategies.

Our intuition tells us that this can be converted to reasoning about general strategies for $\forall$-player (or shortly, $\forall$) by allowing $\exists$ to win whenever $\forall$ plays unfairly. In order to see this, we can look at the complement of Eq. (1a), i.e., the description of when $\forall$ wins; namely, $\forall s \in \varSigma . \, \exists t\in \varPi ^\textsf{fair}. \, \textsf{play}_v(s,t) \notin \alpha$. We can replace the quantification over fair strategies with a quantification over all strategies but require that, in addition to refuting $\alpha$, the resulting play be fair: $\forall s \in \varSigma .\,\exists t\in \varPi . \, \textsf{fair}_\forall (\textsf{play}_v(s,t)) \wedge \textsf{play}_v(s,t)\notin \alpha$. Indeed, as we show in the extended version of this paper [10, App. A - Lem. 2], if strategy $t\in \varPi$ satisfies $\textsf{fair}_\forall (\textsf{play}_v(s,t))$ then we can find a fair strategy $t'\in \varPi ^\textsf{fair}$ with which $\textsf{play}_v(s,t)$ is compliant. This $\forall$-fair strategy would also stop s from winning. Due to determinacy of $\omega$-regular games, we know that the last condition is equivalent to $\exists t\in \varPi .\, \forall s \in \varSigma .\,\textsf{fair}_\forall (\textsf{play}_v(s,t)) \wedge \textsf{play}_v(s,t)\notin \alpha$. In particular, this implies that t is fair. We conclude that the complement of Eq. (1) is the following equation:

$$\begin{aligned} \exists t \in \varPi ^\textsf{fair}.\, \forall s \in \varSigma . \, \textsf{play}_v(s, t) \not \in \alpha . \end{aligned}$$

(1b)

This statement is equivalent to the determinacy of $\forall$-fair games: either $\exists$-player has a winning strategy or $\forall$-player has a winning $\forall$-fair strategy, and the two cannot be true simultaneously.

3.2 From $\forall$-Fair Games to Defining Determined Fair Games

Given a fair game arena A and an $\omega$-regular objective $\alpha$, a natural attempt to define winning regions in fair games would be to generalize Eq. (1) to

$$\begin{aligned} v \in \textsf{Win}_\exists \, \text { if } &\, \exists s \in \varSigma ^\textsf{fair}.\, \forall t \in \varPi ^\textsf{fair}. \, \textsf{play}_v(s, t) \in \alpha , \text { and } \end{aligned}$$

(2a)

$$\begin{aligned} v\in \textsf{Win}_\forall \, \text { if } &\, \exists t \in \varPi ^\textsf{fair}.\, \forall s \in \varSigma ^\textsf{fair}. \, \textsf{play}_v(s, t) \not \in \alpha . \end{aligned}$$

(2b)

However, in this case, $\textsf{Win}_\exists \, \cup \, \textsf{Win}_\forall \ne V$. Indeed, equations (2a) and (2b) are not complements of each other, that is,

$$\begin{aligned} \exists s\in \varSigma ^\textsf{fair}.\,\forall t\in \varPi ^\textsf{fair}.\,\textsf{play}(s,t)\in \alpha \qquad \not \Leftrightarrow \qquad \forall t\in \varPi ^\textsf{fair}.\,\exists s\in \varSigma ^\textsf{fair}.\,\textsf{play}(s,t)\in \alpha . \end{aligned}$$

This observation makes a fair game in which winning regions are defined via Eq. (2) undetermined. The undetermined nodes $O\subseteq V$ – nodes from which none of the players has a fair winning strategy – form a separate partition of nodes, i.e., . To see this, consider the following example.

Example 1

Consider the fair game arena depicted in Fig. 2 where fair edges are shown by dashed lines, $\alpha =$ Parity$(\lambda )$ and each node is labeled by its priority assigned by $\lambda$. We observe that the existential player cannot enforce reaching the even node with a $\exists$-fair strategy from the two middle nodes. Every $\exists$-fair $\exists$-strategy s has a counter $\forall$-fair $\forall$-strategy: choose the fair edge outgoing from the square node after s chooses the fair edge outgoing from the node with round corners. On the other hand, the universal player cannot prevent the play from reaching the even node with a $\forall$-fair strategy from these nodes for exactly the same reason. Hence, the middle two nodes are neither in $\textsf{Win}_\exists$ nor in $\textsf{Win}_\forall$. That is, these two nodes are undetermined; therefore they form $O$.

Fig. 2.

A simple fair game arena discussed in Ex. 1.

In order to better understand the distinction between Equations 2a and 2b, we rely again on translation to $\omega$-regular games. Consider the following reformulation of Eq. (2a):

$$\begin{aligned} \exists s\in \varSigma .\forall t\in \varPi .\textsf{fair}_\exists (\textsf{play}_v(s,t))\wedge (\textsf{fair}_\forall (\textsf{play}_v(s,t)) \Rightarrow \textsf{play}_v(s,t)\in \alpha ). \end{aligned}$$

(3a)

Similarly, the following is a reformulation of Eq. (2b):

From determinacy of $\omega$-regular games, the negation of the latter is:

$$\begin{aligned} \exists s\in \varSigma .\forall t\in \varPi .\textsf{fair}_\forall (\textsf{play}_v(s,t))\Rightarrow (\textsf{fair}_\exists (\textsf{play}_v(s,t)) \wedge \textsf{play}_v(s,t)\in \alpha ). \end{aligned}$$

(3b)

We formally prove the equivalences of Eqs. (2a) and (3a) and Eqs. (2b) and (3b) in [10]. It is not hard to see that the difference between Eq. (3a) and Eq. (3b) is in the way fairness is handled. Namely, in Eq. (3a) $\exists$ loses whenever she plays unfairly regardless of how $\forall$ plays. Dually, in Eq. (3b) $\exists$ wins immediately when $\forall$ plays unfairly regardless of how $\exists$ plays. It follows that determinacy can be regained by deciding the winner of the four different combinations of fairness with an $\omega$-regular winning condition each, as summarized in the following table.

	$\textsf{fair}_\exists (\tau )$	$\lnot \textsf{fair}_\exists (\tau )$
$\textsf{fair}_\forall (\tau )$	$\tau \in \alpha$	$\tau \in \gamma$
$\lnot \textsf{fair}_\forall (\tau )$	$\tau \in \delta$	$\tau \in \beta$

With this generalization, we obtain (3a) if $\beta =\gamma =\bot$ and $\delta =\top$, and (3b) if $\gamma =\bot$ and $\beta =\delta =\top$.

We note that the discussion of determinacy has crucial importance to the analysis of games and the decision of how to model particular scenarios. For example, if fairness of $\forall$-player arises from physical constraints (as, e.g., in [4]) then it might make sense to consider Eq. (2b), which corresponds to $\beta =\top$. Dually, if fairness of $\exists$-player must be adhered to, then it makes sense to consider Eq. (2a), which corresponds to $\beta =\bot$. Our formulation allows to further fine tune what happens when both act unfairly by adjusting $\beta$.

Given the intuition that fairness constraints are actually additional obligations for both players, the choice of $\gamma =\bot$ and $\delta =\top$ assumed in Equations (2)-(3) is very natural. However, allowing mutually unfair plays to be decided by a different $\omega$-regular winning condition $\beta$, allows games with more symmetric winning semantics e.g., by setting $\beta =\alpha$. We therefore restrict our attention in this paper to fair games with two winning conditions $\alpha$ and $\beta$ while if i-player plays fairly but $(1-i)$-player plays unfairly, i-player wins, i.e., $\gamma :=\bot$ and $\delta :=\top$. This is formalized next.

Definition 1 (Fair Games)

[Fair Games] A fair game $G=(A,\alpha ,\beta )$ consists of a fair game arena A together with two ($\omega$-regular) winning conditions $\alpha ,\beta \subseteq \textsf{plays}(A)$ where $\alpha$ and $\beta$ determine the winner of mutually fair and mutually unfair plays, respectively. In fair games, a play that is i-fair and $(1-i)$-unfair is won by player i. Formally, in the fair game $G=(A,\alpha ,\beta )$, $v \in \textsf{Win}_\exists$ if and only if,

$$\begin{aligned} \exists s\in \varSigma .\forall t\in \varPi .\,&\textsf{fair}_\exists (\textsf{play}_v(s,t))\wedge (\textsf{fair}_\forall (\textsf{play}_v(s,t)) \Rightarrow \textsf{play}_v(s,t)\in \alpha )\nonumber \\ \vee (&\lnot \textsf{fair}_\exists (\textsf{play}_v(s,t))\wedge \lnot \textsf{fair}_\forall (\textsf{play}_v(s,t)) \wedge \textsf{play}_v(s,t)\in \beta ) \end{aligned}$$

(4)

The determinacy of fair games follows trivially from the formulation. It follows that the complement of Eq. (4) is the $\forall$ winning region, defined symmetrically by $v\in \textsf{Win}_\forall$ if and only if

$$\begin{aligned} \exists t\in \varPi .\forall s\in \varSigma .\,&\textsf{fair}_\forall (\textsf{play}_v(s,t))\wedge (\textsf{fair}_\exists (\textsf{play}_v(s,t)) \Rightarrow \textsf{play}_v(s,t)\not \in \alpha )\nonumber \\ \vee (&\lnot \textsf{fair}_\forall (\textsf{play}_v(s,t))\wedge \lnot \textsf{fair}_\exists (\textsf{play}_v(s,t)) \wedge \textsf{play}_v(s,t)\not \in \beta ) \end{aligned}$$

Notation. We call a fair game $G=(A,\alpha ,\beta )$ a fair $\alpha / \beta$ game. Further, if $\alpha$ or $\beta$ are given by mentioned winning conditions (e.g. $\alpha =$ Parity$(\lambda )$, $\beta =\bot$), with slight abuse of notation, we refer to the game with the name of the objectives (e.g. fair parity/$\bot$ game).

Remark 1

Stochastic games allow for an additional set $V_s$ of stochastic game nodes that belong to neither $\exists$ nor $\forall$, and for which the stochasticity is resolved uniformly at random. It is known that for purposes of qualitive analysis (i.e., the computation of almost-sure winning strategies), stochastic games can be seen as the special case of $\forall$-fair games in which $E(v)\subseteq E_f$ holds for all stochastic nodes $v\in V_s$, and $E_f\cap E(v)=\emptyset$ for all non-stochastic nodes $v\in V_\exists \cup V_\forall$, that is, all stochastic edges are fair edges, but no non-stochastic edges are fair edges. This encoding treats stochastic branching as adversarial for the system ($\exists$-player).

3.3 Mutually Fair Strategies in Fair Parity Games

In Subsec. 3.2 and in particular in Ex. 1 we have discussed the mutually unfair plays and strategies that take such plays into account in fair $\alpha /\beta$ games. In this section, we start restricting our attention to fair parity/$\beta$ games (as this will be our focus for the rest of the paper) and discuss the particularities of mutually fair strategies in such games. We will do this with the help of the games $G_1-G_4$ depicted in Fig. 3. No mutually unfair plays exist in any of these games. This is because on all given arenas the unfair behaviour of one player makes the play trivially fair for the other. Therefore, the winning regions are independent of $\beta$.

In game $G_1$, both nodes are won by $\exists$. $\forall$-player loses node 3 since taking the self loop on 3 makes the play visit 3 infinitely often, however, it forces $\forall$ to play fairly, implying that they must take the edge to 4 infinitely often. Therefore, any $\forall$-fair play is won by $\exists$ since the priority 4 is seen infinitely often. Also note that if $\forall$-player decides not to play fairly, they immediately lose since all plays are trivially $\exists$-fair. The trivial winning $\exists$-strategy is depicted by red edges.

To get to game $G_2$, we append node 1 to the left of $G_1$. Here, all the nodes are won by $\forall$. This is because $\forall$-player wins node 3 by eventually taking the outgoing edge to 1 and then staying in 1 forever with the self-loop. By doing so $\forall$ evades his obligation to take the fair edges by forcing each play to see node 3 a finite number of times. One winning $\forall$-strategy is depicted by blue edges.

To get to game $G_3$, we append node 5 to the right of game $G_1$. Again, all the nodes are won by $\forall$ even though this time he cannot evade taking his fair edges. In this game $\forall$ wins due to the obligation of $\exists$ to play fairly. In a play starting from 3, $\forall$ must eventually take the outgoing edge to 4. From there on, the play will visit node 4 infinitely often, forcing $\exists$ to take his outgoing edge to 5 infinitely often. As a consequence, in every mutually fair play 5 is seen infinitely often. Therefore, the game is won by $\forall$. A winning $\forall$-strategy is depicted by blue edges on the figure, with the interpretation that blue edges from node 3 are taken alternatingly (in every sequence).

Finally, to get to game $G_4$, we append two nodes to game $G_3$. This time, all the nodes are won by $\exists$. $\exists$-player still needs to take their fair outgoing edges to 5 (and this time, also to the new node 1) infinitely often. But this time she can also take the outgoing edge to 6 infinitely often and thereby win the game. A winning $\exists$-strategy is depicted by red edges on the figure, again with the interpretation that red edges from node 4 are taken alternatingly (in every sequence).

Fig. 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 all its colored outgoing edges are taken alternatingly.

4 Reduction to Parity Games

In this section, we show how fair parity games can be reduced to parity games without fairness constraints. We show that there is a linear reduction to parity games in the case that $\alpha$ is a parity objective and $\beta =\top$ or $\beta =\bot$; for the case that $\beta$ is a non-trivial parity objective, we show that there still is a quadratic reduction. Our reductions work by replacing each fair node in the fair game with a 3-step parity gadget. This construction is inspired by the work of Chatterjee et al. [7] where the qualitative analysis of stochastic parity games is reduced to solving parity games.

We give the formal reduction for fair parity/$\bot$ games in Subsec. 4.1 and extend it to fair parity/parity games in Subsec. 4.2. The extended version contains a discussion of the reduction for a restricted case of fair parity/$\bot$ games (fair Büchi/$\bot$ games), which can serve as a hand-holding introduction to the section.

4.1 Reduction of Fair Parity/$\bot$ Games

Let $G=(A, \text {Parity}(\lambda ), \bot )$ where $A = (V_\exists ,V_\forall ,E,E_f)$ is a fair game arena, and $\lambda : V \rightarrow [2k]$ is the priority function.

The reduction to parity games replaces fair nodes $v \in V^{\textsf{fair}}$ in G with the gadgets given in Fig. 4. Nodes $v \in V^{\textsf{fair}}_\exists$ in G are replaced with one of the gadgets on the top (i.e. the incoming edges to v are redirected to v in the root, and the outgoing edges on the third level lead to E(v) and $E_f(v)$, which are the outgoing edges and outgoing fair edges of v in G, resp.) and nodes $v \in V^{\textsf{fair}}_\forall$ in G are replaced with one of the gadgets at the bottom. The gadgets on the left are called existential gadgets and the ones on the right are called universal gadgets, referring to the player picking the first move. Nodes in $V^{\textsf{n}}$ are not altered.

Even though the proof works for all combinations of the gadgets (i.e. one can replace each $v \in V^{\textsf{fair}}_\exists$ ($v \in V^{\textsf{fair}}_\forall$) with any of the gadgets on the top (bottom)), due to space constraints we give the intuition only for the existential gadgets.

Imagine all $v \in V^{\textsf{fair}}$ are replaced with their existential gadgets. Within a subgame that starts at a fair node $v\in V^{\textsf{fair}}$, the two players intuitively interact as follows. The $\exists$-player gets to pick a number i, indicating the priorities ($2i-1$ or 2i) they intend to visit infinitely often in any play that visits v infinitely often. In turn, $\forall$-player gets to either pick an outgoing edge at v (for this, he pays the price of seeing the even priority 2i), or allow $\exists$ to pick an outgoing edge (in which case he is rewarded with a visit to the odd priority $2i-1$). Depending on the owner of v, the edge picked by $\forall$ (if $v\in V^{\textsf{fair}}_\exists$), or the edge picked by $\exists$ (if $v\in V^{\textsf{fair}}_\forall$) is required to be contained in $E_f$. Thus $\forall$ can insist on exploring fair edges at $V^{\textsf{fair}}_\exists$ nodes, but has to pay a price for it; dually, $\forall$ eventually has to allow $\exists$ to explore the fair edges at $V^{\textsf{fair}}_\forall$ nodes to win.

In the full reduced game defined formally in the proof of Thm. 1 below, the owner of a fair node v can fairly win from v by either avoiding v from some point on forever, or eventually allowing the opponent player to explore all fair edges leading out of that node. The owner wins by playing unfairly if and only if the opponent also plays unfairly and the owner is the $\forall$-player.

Fig. 4.

Existential (left) and universal (right) gadgets for $v \in V^{\textsf{fair}}_\exists$ (top) and $v \in V^{\textsf{fair}}_\forall$ (bottom) in fair parity/$\bot$ games. For $i \in [1, k+1]$, priorities of nodes $v_i^\exists$ and $v_i^\forall$ are given below them, priorities of nodes $v_i$ are ignored, and the priority of v is unaltered.

Theorem 1

Let $G=(A,\text {Parity}(\lambda ),\bot )$ where $A = (V_\exists ,V_\forall ,E,E_f)$ is a fair game arena, and $\lambda : V \rightarrow [2k]$ is the priority function. Then there exists a parity game $G'$ on the node set $V'$ with $V\subseteq V'$ and $|V'| \le n(3k+3)$ over $2k+1$ priorities such that for $i \in \{\exists , \forall \}$, $\textsf{Win}_i(G) = \textsf{Win}_i(G') \cap V$.

Proof (Sketch). Let $G'=(V'_\exists ,V'_\forall ,E',\Omega :V'\rightarrow [ 2k+1])$ be the parity game obtained by replacing the fair nodes in G with an arbitrary combination of their corresponding existential and universal gadgets in Fig. 4. Let $V' = V'_\exists \cup V'_\forall = V \cup V^{\textsf{gad}}$ where V represent the nodes coming from G and $V^{\textsf{gad}}$ represent the nodes coming from the gadgets. Note that the maximum priority in $G'$ is $\max _\textsf{odd}= 2k+1$ which comes only from the gadget nodes $V^{\textsf{gad}}$. The maximum even priority in $G'$ is $\max _\textsf{even}= 2k$ which can come from both $V^{\textsf{gad}}$ and V. It is easy to see that $|V'| \le n(3k+3)$ and $G'$ uses priorities $[2k+1]$. To prove the correctness, we recall that the winning regions for fair parity/$\bot$ games are given via Eq. (3a), i.e. $v \in \textsf{Win}_\exists (G)$ if and only if

($\Rightarrow$)We will first show, $v \in \textsf{Win}_\exists (G') \cap V \Rightarrow v \in \textsf{Win}_\exists (G)$. To do so, we will take a (positional) winning $\exists$-strategy $s'$ in $G'$ and construct an $\exists$-strategy s in G such that s is $\exists$-winning in G i.e., s realizes Eq. (3a). That is, for a play $\rho$ in G that starts from v and compliant with s Eq. (3a-s) holds.

For this we will show the two parts of the conjunction separately. We will show (i) $\textsf{fair}_\exists (\rho )$, i.e. $s \in \varSigma ^\textsf{fair}$, (ii) $\textsf{fair}_\forall (\rho ) \Rightarrow \rho \in \alpha$, i.e. every $\forall$-fair play compliant with s is $\exists$-winning w.r.t. the parity condition.

Construction of the $s'$-subgame $G'_{s'}$: Let $s'$ be a positional $\exists$-strategy winning every play from v in $G'$. We will denote the subgame of $G'$ where $\exists$ nodes have only the outgoing edges $u \rightarrow s'(u)$ by $G'_{s'}$, and call it the $s'$-subgame. Recall that all plays that start from v in $G'_{s'}$ are $\exists$-winning.

Notation of $n_u$ and succ(u): For the existential gadgets for both $V^{\textsf{fair}}_\exists$ and $V^{\textsf{fair}}_\forall$, we call the index of the unique successor of u in $G'_{s'}$, $n_u$. That is, $s'(u) = u_{n_u}$. For the same gadgets, we will denote $s'(u_{n_u}^\exists )$ with succ(u). For the universal gadgets for both $V^{\textsf{fair}}_\exists$ and $V^{\textsf{fair}}_\forall$, we will let $n_u$ denote the index of the rightmost child of u that is sent to its right child by $s'$. That is, $n_u$ is the largest index i such that $s'(u_i) = u_i^\exists$. For the same gadgets, we will denote $s'(u_{n_u}^\exists )$ with succ(u).

Construction of s: We define $s: V^*\cdot V_\exists \rightarrow V$ as follows. For $u \in V^{\textsf{fair}}_\exists$: 1. If $n_u = k+1$, we set $s(u)= succ(u)$. 2. Otherwise, s(u) cycles through the set $\{succ(u), E_f(u)\}$ starting from succ(u). For $u \in V_\exists \setminus V^{\textsf{fair}}_\exists$, we set $s(u)=s'(u)$.

Constraining $G'_{s'}$ with $n_u$: Here we will constrain $G'_{s'}$ to its subgame by limiting the choices of $\forall$-player from a u replaced by the universal gadget. For every universal gadget encountered in $G'_{s'}$, we limit the choices of $u \in V^{\textsf{fair}}_\forall$ to only $u \rightarrow u_{n_u}$ and $u \rightarrow u_{n_u +1}$ (if it exists). So, we remove all the other branches of u out of $G'_{s'}$. We call the remaining game $LG'_{s'}$, standing for limited $G'_{s'}$. Note that as $LG'_{s'}$ is a subgame of $G'_{s'}$, it is still $\exists$-winning.

$\exists$-extension: Let $\rho$ be some play in G compliant with s. We define a play $\rho '$ that is called the $\exists$-extension of $\rho = u^1 u^2 \ldots$ as follows: $\rho '$ is the play on $LG'_{s'}$ that follows $\rho$ while ‘prioritising existential nodes on succ(u)’. What is meant by this is, for a $u^i \in V^{\textsf{fair}}$, if $u^{i+1} = succ(u^i)$, then $\rho '$ takes the unique branch in $LG'_{s'}$ that leads to $u^{i+1}$ while passing through an existential node ${(u^i)}_j^\exists$. That is, regardless of which gadget $u^i$ is replaced by, $\rho '$ takes the branch

On the other hand if $u^{i+1} \ne succ(u^i)$, then $\rho '$ takes the only other branch in $LG'_{s'}$, that is (branch 2) is taken as

• 1. If $u^i \in V^{\textsf{fair}}$ is replaced by an $\exists$-gadget, then $u^i \rightarrow u^i_{n_{u^i}} \rightarrow {(u^i)}^\forall _{n_{u^i}} \rightarrow u^{i+1}$,

• 2. If $u^i \in V^{\textsf{fair}}$ is replaced by a $\forall$-gadget, then $u^i \rightarrow u^i_{n_{u^i}+1} \rightarrow {(u^i)}^\forall _{n_{u^i}+1} \rightarrow u^{i+1}$,

Note that these branches do not leave out any possible transition in $\rho$. That’s because 1. all the successors of a $V^{\textsf{fair}}_\forall$ node are covered by one of the branches since (branch 2) leads the universal node ${(u^i)}^\forall _{n_{u^i}}$ or ${(u^i)}^\forall _{n_{u^i}+1}$, which can pick any successor of $u^i$. 2. all the successors of a $V^{\textsf{fair}}_\exists$ node are covered by one of the branches, since by construction of s, all the successors of $u^i$ in $\rho$ are in the set $\{succ(u^i)\} \cup E_f(u^i)$, where (branch 1) covers the $succ(u^i)$ successors, and (branch 2) covers the $E_f(u^i)$ successors since in this case the universal node ${(u^i)}^\forall _{n_{u^i}}$ or ${(u^i)}^\forall _{n_{u^i}+1}$ can pick any fair successor of $u^i$.

For $u^i \ne V^{\textsf{fair}}$, $\rho '$ just takes $u^i \rightarrow u^{i+1}$.

So $\rho '$ is well defined, and is a play in $LG'_{s'}$ that starts from v. Thus, $\rho '$ is $\exists$-winning. Observe that if we remove the gadget nodes from $\rho '$, we get $\rho$. That is, the restriction of $\rho '$ to V, $\rho ' \mid _{V} = \rho$.

(i) $\textsf{fair}_\exists (\rho )$: Observe that for any $\rho$ in G compliant with s, by construction of s, the only nodes $u \in V^{\textsf{fair}}_\exists$ that $\rho$ may not be fair on, are those for which $n_u = k+1$. So we only need to show that such nodes are seen only finitely often in $\rho$. Since $\rho |_V = \rho '$, that is equivalent to showing such a u cannot be seen infinitely often in its $\exists$-extension, $\rho '$. If it is seen infinitely often in $\rho '$, then regardless of the gadget u is replaced with, the branch $u \rightarrow u_{k+1} \rightarrow u_{k+1}^\exists$ is evoked infinitely often, signalling the largest priority $2k+1$. Therefore, $\rho '$ is won by $\forall$-player, giving a contradiction. Therefore, we conclude $\rho$ is $\exists$-fair.

(ii) $\textsf{fair}_\forall (\rho ) \Rightarrow \rho \in \alpha$: Let $\rho$ be $\forall$-fair. Look at the $\exists$-extension $\rho '$ of $\rho$. Let m be the largest (even) priority in $\textsf{Inf}(\rho ')$. Due to $\rho '\mid _V = \rho$, all we need to show is the existence of a $u \in \textsf{Inf}(\rho '\mid _V)$ that has priority m. Then it automatically implies that the maximum priority in $\textsf{Inf}(\rho )$ is m, and thus $\rho$ is $\exists$-winning.

We will proceed with proof by contradiction and assume that the priority m appears only in $V^{\textsf{gad}} \cap \textsf{Inf}(\rho ')$. Now let F be the subgame of $LG'_{s'}$ that consists of nodes and edges taken infinitely often in $\rho '$. Then, priority m appears in $V^\textsf{gad} \cap F$. These gadget nodes must exist in F due to nodes

• $u \in V^{\textsf{fair}}$ replaced by existential gadgets, and with $n_u = m\backslash 2$ (which corresponds to (branch 2)-1), or

• $u \in V^{\textsf{fair}}$ replaced by universal gadgets, and with $n_u = m\backslash 2-1$ (which corresponds to (branch 2)-2)

Note that for all such nodes u, (branch 1) of u is also in F. This is because $u \rightarrow succ(u)$ is taken infinitely often in $\rho$. For $u \in V^{\textsf{fair}}_\exists$, this is due to the construction of s, for $u \in V^{\textsf{fair}}_\forall$, this is due to $\rho$ being $\forall$-fair (remember, in this case $succ(u) \in E_f(u)$).

Next, we will remove from F all priority m gadget nodes (and everything reachable only from those nodes). That is, we will prune out (branch 2) of all the nodes that bring in m priority gadget nodes to F. Due to the remaining (branch 1)s, this pruning does not cause any dead-ends. Let’s call this pruned subgame of F, H. Observe once more that all plays in H are $\exists$-winning. However, the maximum priority in H is $m-1$. This is due to the remaining (branch 1)s of the pruned nodes having this priority. This implies that all infinite plays starting in H get trapped in a subgame $H'$ of H that doesn’t have nodes with priority $m-1$. Since non of the nodes in $V^{\textsf{fair}}\cap H'$ cause a gadget node with priority m, non of their branches get pruned. That is, all nodes in $H'$ have the same outgoing edges in $H'$ and in F. Then any play that start in $H'$ in F, does not leave $H'$, making $H'$ exactly the set of nodes seen infinitely often in $\rho '$, i.e. $H' = F$. This contradicts our initial assumption that maximum priority seen infinitely often in $\rho '$ being m; therefore proving $\rho$ is $\exists$-winning.

The proof of direction $\mathbf {(\Leftarrow )}$ is similar to the proof of $\mathbf {(\Rightarrow )}$, and can be found in detail in the extended version [10].

Remark 2 (Reduction of parity/$\top$ games)

[Reduction of parity/$\top$ games] In the gadgets from Fig. 4, in order to play unfairly from a $v \in V^{\textsf{fair}}_\exists$, $\exists$-player has to take its rightmost branch and signal priority $\max _\textsf{odd}$, whereas to play unfairly from $v \in V^{\textsf{fair}}_\forall$, $\forall$-player has to take the rightmost branch and signal $\max _\textsf{even}$. Since $\max _\textsf{odd}> \max _\textsf{even}$, this dynamic ensures mutually unfair plays are $\forall$-winning. The gadgets for a fair parity/$\top$ game with $\lambda : V \rightarrow [2k]$ can be constructed as follows with the addition of priority $2k+2$: Take the gadgets from Fig. 4. In the existential gadget for $V^{\textsf{fair}}_\exists$ add another branch $\rightarrow v^\forall _{k+1} \rightarrow E_f(v)$ to $v_{k+1}$ and in the universal gadget for $V^{\textsf{fair}}_\exists$ add a rightmost branch $\rightarrow v_{k+2} \rightarrow v_{k+2}^\forall \rightarrow E_f(v)$. In the existential gadget for $V^{\textsf{fair}}_\forall$ add a rightmost branch $\rightarrow v_{k+1} \rightarrow v^\exists _{k+1} \rightarrow E_f(v)$ and in the universal gadget for $V^{\textsf{fair}}_\forall$ add another branch $\rightarrow v^\exists _{k+1} \rightarrow E_f(v)$ to $v_{k+1}$.

All the newly added gadget nodes have priority $2k+2$ and therefore $\max _\textsf{even}=2k+2 > \max _\textsf{odd}=2k+1$, which ensures that mutually unfair plays are $\exists$-winning. The correctness of the construction follows as a corollary of the reduction of fair parity/parity games given in the next section.

4.2 Reduction of Fair Parity/Parity Games

In this section, we present a quadratic reduction from fair parity/parity to parity games. So let $G=(A, \text {Parity}(\lambda ),\text {Parity}(\Gamma ))$ where $A = (V_\exists ,V_\forall ,E,E_f)$ is a fair game arena with and priority functions $\lambda :V\rightarrow [2k]$, $\Gamma : V\rightarrow [d]$.

The reduction is based on ideas from the previous section, in particular adapting the basic structure of the introduced gadgets. However, in order to correctly treat mutually unfair plays according to the additional parity objective $\Gamma$, we annotate game nodes $v\in V$ with two memory values $p\in [d]$ and $b\in \{\exists ,\forall \}$. The former is used to store the maximal priority according to $\Gamma$ that the play has recently seen; this value is signalled (and reset after signalling) from time to time in the reduced game. The value b is used to decide (at certain nodes) whether the memory value is signalled, or not.

Fig. 5.

Gadget for $v \in V^{\textsf{fair}}_\exists$ in fair parity/parity games; u abbreviates (v, p, b).

It indicates the player that has last taken the rightmost branch in the gadget for one of its fair nodes. If this bit keeps flipping between $\exists$ and $\forall$ forever, then both players intuitively insist on keeping control in one of their respective fair nodes, enabling a mutually unfair play; in the reduced game, the memory content p is signalled (and then reset to 1) whenever the value flips from $\forall$ to $\exists$.

Fig. 6.

Gadget for $v \in V^{\textsf{fair}}_\forall$ in fair parity/parity games; u abbreviates (v, p, b).

Formally, the reduction is as follows. The game is based on the set $V\times [d]\times [1]$ of base nodes, where we use [1] to denote $\{\exists ,\forall \}$; intuitively, a node (v, p, b) from this set corresponds to $v\in V$, annotated with memory values p and b as described above. In order to succinctly refer to the combination of taking a move in G and updating the memory components, we overload notation and put

$$\begin{aligned} E(v,p,b)&=\{(w,p',b)\in V\times [d]\times [1]\mid w\in E(v)\text { and } p'=\max (p,\Gamma (v))\}\\ E_f(v,p,b)&=\{(w,p',b)\in V\times [d]\times [1]\mid w\in E_f(v)\text { and } p'=\max (p,\Gamma (v))\} \end{aligned}$$

for $(v,p,b)\in V\times [d]\times [1]$. Thus a triple $(w,p',b)$ is contained in E(v, p, b) if there is a move $(v,w)\in E$ and $p'$ is the maximum of the previous memory value p and the current priority $\Gamma (v)$ at v; in $E_f(v,p,b)$, we require $(v,w)\in E_f$ instead. In both functions, the argument b is used to explicitly set this component of the memory to either $\exists$ or $\forall$. The reduced game consists of subgames that start at annotated nodes $u=(v,p,b)\in V\times [d]\times [1]$. In case that $v\in V^{\textsf{n}}$, the game just proceeds according to E(v, p, b), with ownership of (v, p, b) determined by whether $v\in V_\exists$ or $v\in V_\forall$; this corresponds to taking a move at a normal node in G, but updating the memory component p, and keeping the component b without modifying it. For fair nodes $v\in V^{\textsf{fair}}$, the subgame consists of three levels, and after these three steps leads back to a node from $V\times [d]\times [1]$. Fig. 5 and 6 show the subgames that start at $(v,b,p)\in V\times [d]\times [1]$ such that $v\in V^{\textsf{fair}}_\exists$ and $v\in V^{\textsf{fair}}_\forall$, respectively, adapting the existential gadget for $v \in V^{\textsf{fair}}_\exists$ and the universal one for $v\in V^{\textsf{fair}}_\forall$.

The rightmost branches in these gadgets overwrite the last component b with $\exists$ and $\forall$, respectively. The colored values in the right-most branch in the Fig. 5 gadget depend on the value of b. If $b=\forall$ (corresponding to $\forall$-player being the one that last has taken the right-most branch), then the priority $2k+2+p$ is signalled and the memory value p is reset to 1; if $b=\exists$ (corresponding to $\exists$-player having taken the right-most branch last), then the priority $2k+1$ is signalled and the memory value p does not change.

Theorem 2

Let $G=(A, \text {Parity}(\lambda ),\text {Parity}(\Gamma ))$ where $A = (V_\exists ,V_\forall ,E,E_f)$ is a fair game arena, and $\lambda :V\rightarrow [2k]$ and $\Gamma : V\rightarrow [d]$ are priority functions. Then there exists a parity game $G'$ with $6 n d(k+2)$ nodes and $2k+2+d$ priorities with set $V\times [d]\times [1]$ of base nodes such that for all $v\in V$, $\exists$-player wins v in G if and only if $\exists$-player wins $(v,1,\exists )$ in $G'$.

Proof (Sketch)

[Sketch] We construct the parity game $G'$ following the above description, using the gadgets from Fig. 5 and 6 to treat fair nodes. The detailed construction and the correctness proof can be found in the extended version [10].

We obtain the following bound on strategy sizes for fair parity/parity games.

Lemma 1

Let G be a fair parity/parity game on n nodes. Then for both players the memory requirement of winning strategies in G is at most $n^2\cdot n^n$. Furthermore, for each player a family of fair parity/$\bot$ games $(G_n)_{n\in \mathbb {N}}$ exists such that for all n, every winning strategy for the respective player requires memory at least $2^n$.

Proof (Sketch)

[Sketch] For the upper bound, we note that in a winning i-strategy for a fair parity/parity game, as constructed in the proof of Thm. 2, the nodes in $V_i \setminus V^{\textsf{fair}}$ have strategies with quadratic memory, but the nodes in $V^{\textsf{fair}}_i$ may have to traverse all their fair successors, and possibly one more successor. In the worst case, this requires an additional local memory of $|E_f(v)| + 1\le n$ for each $v \in V^{\textsf{fair}}_i$, and causes an exponential blowup in the overall memory required.

For the lower bound, we consider the case for $\exists$-player; the result for $\forall$-player is obtained by switching the player’s roles. Define the family $(G_n)_{n\in \mathbb {N}}$ of games by letting $G_n$ (for $n\in \mathbb {N}$) have exactly $n+1$ nodes, one node x owned by $\forall$-player and n nodes $y_i$ owned by $\exists$-player; let there be an edge from x to any node $y_i$ and two fair edges from any node $y_i$ back to x. Let all nodes have priority 0. Then any winning $\exists$-strategy in $G_n$ necessarily is $\exists$-fair. There is a fair $\exists$-strategy s that uses one bit as local memory for each node $y_i\in V^{\textsf{fair}}_\exists$, and therefore uses memory of overall size $2^n$. The claim follows since there is no $\exists$-fair strategy that uses less memory than s, which is shown by induction on n.    $\square$

5 Fixpoint Characterization of Winning Regions

In this section, we will characterize the winning regions in fair games with parity conditions by means of fixpoint expressions. Thereby we provide an alternative, symbolic route to solve such games, rather than by reducing to parity games. We start by briefly recalling details on Boolean fixpoint expressions.

Fixpoint expressions and fixpoint games. Let U be a finite set, let o be a fixed number and let $f:\mathcal {P}(U)^o\rightarrow \mathcal {P}(U)$ be a monotone function, that is, assume that whenever we have sets $X_j,Y_j\subseteq U$ such that $X_j\subseteq Y_j$ for all $1\le j\le o$, then $f(X_1,\ldots ,X_o)\subseteq f(Y_1,\ldots ,Y_o)$. Then f and o induce the fixpoint expression

$$\begin{aligned} e=\eta _o X_o.\,\eta _{o-1} X_{o-1}.\,\ldots .\nu X_2.\,\mu X_1.\,f(X_1,\ldots ,X_o) \end{aligned}$$

(5)

where $\eta _i=\nu$ if i is even and $\eta _i=\mu$ if i is odd. We define the semantics of fixpoint expressions using parity games. Given a fixpoint expression e, the associated fixpoint game $G_{e}=(W_\exists ,W_\forall ,E, \text {Parity}(\kappa ))$ for the priority function $\kappa :W_\exists \cup W_\forall \rightarrow \mathbb [o]$ is the following parity game. We put $W_\exists =U\times \{1,\ldots ,o\}$, $W_\forall =\mathcal {P}(U)^o$. Moves and priorities are defined by

$$\begin{aligned} E(v,i)&=\{\overline{Z}\in W_\forall \mid v\in f(\overline{Z})\} & \kappa (v,i)&=i\\ E(\overline{Z})&=\{(v,i)\mid v\in Z_i\} & \kappa (\overline{Z})&=0 \end{aligned}$$

for $(v,i)\in W_\exists$ and $\overline{Z}=(Z_1,\ldots , Z_o)\in W_\forall$. Then we say that $v\in U$ is contained in e (denoted $v\in e$) if and only if $\exists$-player wins the node (v, 1) in $G_{e}$.

Remark 3

The above game semantics for fixpoint expressions has been shown to be equivalent to the more traditional Knaster-Tarski semantics [3]; the cited work takes place in a more general setting and therefore uses slightly more verbose parity games.

Next we present a fixpoint characterization of the winning regions in fair games of the form $G=(A,\text {Parity}(\lambda ),\bot )$ where $A = (V_\exists ,V_\forall ,E,E_f)$ is a fair game arena, and $\lambda : V \rightarrow [2k]$ a priority function. To be able to write fixpoint expressions over such games we define monotone operators on subsets of V by putting

$$\begin{aligned} \lozenge X &= \{v\in V\mid E(v)\cap X\ne \emptyset \} & \square X &= \{v\in V\mid E(v)\subseteq X\} \\ \lozenge _f X &= \{v\in V\mid E_f(v)\cap X\ne \emptyset \} & \square _f X &= \{v\in V\mid E_f(v)\subseteq X\} \end{aligned}$$

for $X\subseteq V$ and also put $\textsf{Cpre}(X)=(V_\exists \cap \lozenge X)\cup (V_\forall \cap \square X)$. Then $\textsf{Cpre}(X)$ is the set of nodes from which $\exists$-player can force the game to reach a node from X in one step. Also, we define $C_i=\{v\in V\mid \lambda (v)=i\}$ for $1\le i\le 2k$.

Using this notation, we define a function $\textsf{parity}:\mathcal {P}(V)^{2k}\rightarrow \mathcal {P}(V)$ by putting

$$\textsf{parity}(X_1,\ldots , X_{2k}):= (C_1 \cap \textsf{Cpre}(X_1)) \cup \ldots \cup (C_{k} \cap \textsf{Cpre}(X_{2k}))$$

for $(X_1,\ldots ,X_{2k})\subseteq \mathcal {P}(V)^{2k}$. This function is monotone and it is well-known (see e.g [23]) that the fixpoint induced by $\textsf{parity}$ characterizes the winning region in parity games with priorities 1 through 2k. This formula will still apply to ‘normal’ nodes $V^{\textsf{n}}$ in the fixpoint characterization of fair parity games.

We follow the gadget constructions from Fig. 4 (using their existential versions) to define the following additional functions. For $1\le i < k$, put

$$\begin{aligned} \textsf{Apre}_{\exists }(X_i,X_{i+1})&=\lozenge X_i\cap \square _f X_{i+1} & \textsf{Apre}_{\forall }(X_i,X_{i+1})&=\lozenge _f X_i\cap \square X_{i+1}, \end{aligned}$$

encoding nodes $(v^\forall ,2i)$ for $v\in V^{\textsf{fair}}_\exists$ and $v\in V^{\textsf{fair}}_\forall$, respectively (here, $\textsf{Apre}$ stands for alternative predecessor function, as it encodes the additional $\forall$-choice of whether a fair edge is to be taken). Then, we let $I_p=\{ i\mid i \text { odd}, p \le i< 2k\}$ denote the set of odd priorities that lie between p and 2k, and put

$$\begin{aligned} \phi ^\textsf{fair}_{\exists , p}&= {\left\{ \begin{array}{ll} \bigcup _{i\in I_p}\textsf{Apre}_{\exists }(X_{i},X_{i+1})\,\cup \, \lozenge \, X_{2k+1} &{} p\text { is odd} \\ \bigcup _{i\in I_p}\textsf{Apre}_{\exists }(X_{i},X_{i+1})\, \cup \,\lozenge \, X_{2k+1} \cup \square _f \,X_p &{} p\text { is even}, \end{array}\right. }\\ \phi ^\textsf{fair}_{\forall , p}&= {\left\{ \begin{array}{ll} \bigcup _{i\in I_p}\textsf{Apre}_{\forall }(X_{i},X_{i+1}) &{} p\text { is odd} \\ \bigcup _{i\in I_p}\textsf{Apre}_{\forall }(X_{i},X_{i+1})\, \cup \square \,X_p &{} p\text { is even} \end{array}\right. } \end{aligned}$$

Using this notation, the winning region for the existential player in fair parity/$\bot$ games with priorities 1 through 2k can be characterized by the fixpoint expression induced by $2k+1$ and the function $\chi$ that is defined to map $(X_1,\ldots , X_{2k+1})\in \mathcal {P}(V)^{2k+1}\rightarrow \mathcal {P}(V)$ to the set

$$\begin{aligned} \chi (X_1,\ldots , X_{2k+1})= &(V^{\textsf{n}}\,\cap \, \textsf{parity})\,\cup \\ & (V^{\textsf{fair}}_\exists \, \cap \, \bigcup _{i \in [2k+1]}\, C_i \,\cap \,\phi ^\textsf{fair}_{\exists , i})\, \cup \\ {} &(V^{\textsf{fair}}_\forall \, \cap \, \bigcup _{i \in [2k+1]}\, C_i \,\cap \,\phi ^\textsf{fair}_{\forall , i}) \end{aligned}$$

The function $\chi$ therefore treats normal nodes from $V^\textsf{n}$ in the same way as nodes in standard parity games are treated, but for fair nodes with priority i, the functions $\phi ^\textsf{fair}_{\exists ,i}$ and $\phi ^\textsf{fair}_{\forall ,i}$ are used to encode the respective gadget construction. The full fixpoint expression then is

$$\begin{aligned} e=\mu X_{2k+1}.\, \nu X_{2k}.\, \mu X_{2k-1}\,\ldots \,\nu X_2.\,\mu X_1. \,\chi (X_1,\ldots , X_{2k+1}) \end{aligned}$$

(6)

The first result of this section is that the fixpoint expression (6) characterizes the winning region of $\exists$-player in fair parity/$\bot$ games.

Theorem 3

Let $G=(A,\text {Parity}(\lambda ),\bot )$ where $A = (V_\exists ,V_\forall ,E,E_f)$ is a fair game arena, and $\lambda : V \rightarrow [2k]$ is the priority function. Then the fixpoint expression given in (6) characterizes $\textsf{Win}_\exists (G)$.

Proof (Sketch)

[Sketch] The proof is by mutual transformation of winning strategies in G and in the semantic game $G_e$ for (6). The full proof can be found in [10].

We note that for $\forall$-fair parity games ($V^{\textsf{fair}}_\exists =\emptyset$), Eq. (6) instantiates to the fixpoint characterization given in [4]; it follows that the parity game reductions from Sec. 4 apply to the one-sided fair parity games considered in [4] as well.

For fair parity/parity games, we obtain a similar fixpoint characterization, encoding the reduction to parity games presented in Subsec. 4.2 along the lines of Figures 5 and 6. Here, all involved functions work over (subsets of) the set $V\times [d]\times [1]$ of base nodes, consisting of game nodes that are annotated with memory values. The definition of the fixpoint expression for fair parity/parity games is straight-forward but somewhat technical since the updating and resetting mechanisms for the memory values have to be accommodated. For brevity, we refrain from elaborating the required notation and the full fixpoint expression here, and state just the main result that yields a symbolic fixpoint algorithm for fair parity/parity games; full details can be found in the extended version [10].

Theorem 4

Let $G=(A,\text {Parity}(\lambda ),\text {Parity}(\Gamma ))$ where $A = (V_\exists ,V_\forall ,E,E_f)$ is a fair game arena, and $\lambda : V \rightarrow [2k]$, $\Gamma : V \rightarrow [d]$ are priority functions. Then there is a fixpoint expression over $V\times [d]\times [1]$ with alternation depth $2(k+1)+d$ that characterizes $\textsf{Win}_\exists (G)$.

Proof (Sketch)

[Sketch] Again the proof is by mutual transformation of winning strategies in G and in the semantic game $G_e$ for the fixpoint expression. The full proof can be found in the extended version [10].

6 Conclusion

We introduce two-player games with local transition-fairness constraints for both players, allowing two objectives $\alpha$ and $\beta$ to decide the winner of plays in which both players play fair and both players play unfair, respectively. We show the determinacy of this class of games in the case that $\alpha$ and $\beta$ are $\omega$-regular objectives. In the special case that both $\alpha$ and $\beta$ are parity conditions, there is a reduction to standard parity games with blow-up quadratic in the number of priorities used by $\alpha$ and $\beta$; if $\beta =\top$ or $\beta =\bot$, the reduction becomes even linear. We present both enumerative and symbolic methods to realize this reduction; in the process, we also obtain an exponential tight bound on the memory required by winning strategies in fair parity/parity games. We expect that the central idea behind the reduction generalizes from parity objectives to more general settings such as fair games in which $\alpha$ and $\beta$ are Rabin, Streett, or even Emerson-Lei conditions, but leave this issue for future work.