Dieses Kapitel untersucht die Synthese von Korrektur-nach-Design-Software in Cyber-Physischen Systemen (CPS) durch die Linse von Zwei-Spieler-Graphen-Spielen, bei denen der eine Spieler als Controller und der andere als gegnerisches Umfeld fungiert. Der Schwerpunkt liegt auf Energie- und Gewinnspielen unter strengen Fairness-Beschränkungen beim Übergang, die über günstige Recheneigenschaften verfügen. Das Kapitel stellt das Konzept der starken Übergangsgerechtigkeit vor und hebt sein natürliches Vorkommen in Bereichen wie Ressourcenmanagement und Controller-Synthese hervor. Außerdem wird die Integration quantitativer Ziele wie Energie oder Mittelwert-Nutzen untersucht, die die Optimierung von Strategien auf der Grundlage von Leistungskennzahlen ermöglichen. Das Kapitel stellt einen einheitlichen Rahmen für die Lösung dieser Spiele mittels eines neuartigen, Gadget-basierten Ansatzes vor, der faire quantitative Spiele in regelmäßige quantitative Spiele auf einem linear größeren Staatsraum übersetzt. Dieser Ansatz verbessert die Rechenkomplexität für 1-faire quantitative Spiele erheblich. Das Kapitel geht auch auf die Bestimmtheit und Komplexität dieser Spiele ein und bietet Einblicke in die Gedächtnisanforderungen für Gewinnstrategien. Darüber hinaus wird das Potenzial zukünftiger Forschung im Bereich doppelt fairer Spiele und allgemeinerer Vorstellungen von Fairness diskutiert. Das Kapitel schließt mit einer detaillierten Analyse der Recheneigenschaften fairer Energie- und Mittelwert-Auszahlungsspiele und zeigt, dass starke Übergangsgerechtigkeit nahtlos in quantitative Spiele ohne nennenswerten Rechenaufwand integriert werden kann.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
We examine two-player games over finite weighted graphs with quantitative (mean-payoff or energy) objective, where one of the players additionally needs to satisfy a fairness objective. The specific fairness we consider is called strong transition fairness, given by a subset of edges of one of the players, which asks the player to take fair edges infinitely often if their source nodes are visited infinitely often. We show that when fairness is imposed on player 1, these games fall within the class of previously studied \(\omega \)-regular mean-payoff and energy games. On the other hand, when the fairness is on player 2, to the best of our knowledge, these games have not been previously studied. We provide gadget-based algorithms for fair mean-payoff games where fairness is imposed on either player, and for fair energy games where the fairness is imposed on player 1. For all variants of fair mean-payoff and fair energy (under unknown initial credit) games, we give pseudo-polynomial algorithms to compute the winning regions of both players. Additionally, we analyze the strategy complexities required for these games. Our work is the first to extend the study of strong transition fairness, as well as gadget-based approaches, to the quantitative setting. We thereby demonstrate that the simplicity of strong transition fairness, as well as the applicability of gadget-based techniques, can be leveraged beyond the \(\omega \)-regular domain.
Hinweise
An extended version of this paper is available at [8].
All authors are partially supported by the DFG project 89792660 as part of TRR 248 – CPEC, and by the Emmy Noether Grant SCHM 3541/1-1.
1 Introduction
Games on graphs serve as a formal and effective framework for automatically synthesizing correct-by-design software in cyber-physical systems (CPS). In this setting, one player represents a controller aiming to ensure a high-level logical specification in response to the actions of an adversarial player representing the external environment. Two-player graph games abstract the strategic reactive behavior of autonomous systems, such as robots [37, 46, 52] or cars [40, 41], and can be employed to synthesize correct-by-design strategies through the algorithmic process of reactive synthesis. Such strategies function as logical controllers to ensure the required behavioral guarantees, ensuring the system meets its safety and performance goals over its strategic interactions with its environment.
In the CPS context, these game-based abstractions have been augmented with additional information, such as assumptions about the players’ strategic behavior induced by the underlying physical processes [5, 34], and quantitative objectives that allow to optimize strategies w.r.t. given performance metrics [9]. These enhancements enable reactive synthesis algorithms to compute control strategies that are more aligned with the specific requirements of CPS applications. However, these extensions typically come with increased computational costs, hindering their practical applicability. In this paper, we show that a particular subclass of such games – namely, energy and mean-payoff games under strong-transition-fairness constraints – distinctly posses favorable computational properties. We refer to these games as fair energy and fair mean-payoff games.
Anzeige
1.1 Background
Strong Transition Fairness. Strong transition fairness [10, 34, 44] is defined over specific edges, referred to as fair edges, and restricts strategies to use a fair edge infinitely often if its source vertex is visited infinitely often. Strong transition fairness constraints are less expressive than general fairness, typically expressed via a qualitative objective called the Streett objective [48]. Yet, they naturally arise in areas such as resource management [19], abstractions of continuous-time physical processes for planning [6, 26, 31] and controller synthesis [38, 42, 50]. At the same time, games with strong transition fairness conditions offer more favorable computational properties compared to those with Streett fairness, making them a compelling subject of study.
Despite their strong motivation from CPS applications and their favorable computational properties, strong transition fairness has so far been considered only in the context of qualitative objectives, such as parity [35, 45] or Rabin [11, 49], where it is shown to be computationally inexpensive, preserving the overall complexity of the game and inducing negligible computational cost. This paper shows that these property carry over to quantitative games.
Energy & Mean-Payoff Games. Quantitative objectives, such as energy or mean-payoff, allow capturing strategic limitations induced by constrained resources, such as the power usage of embedded components, the buffer size of a networking element [28], or string selections with limited storage [53].
Mean-payoff games, introduced in [33], assign integer weights to edges, representing the payoffs received by player 1 (the controller) and paid by player 2 (the environment) when an edge is taken. These games are played over infinitely many rounds, with player 1 aiming to maximize the long run average value of the edges traversed, while player 2 aims to minimize this value.
Anzeige
Energy games, introduced more recently in [18], also assign integer weights to edges, this time representing energy gains or losses. In this setting, the controller’s goal is to construct an infinite path where the total energy in every prefix remains non-negative, while the environment aims to prevent this.
It is known that determining the winner in both energy and mean-payoff games is in \({\textsf{NP}}\,\cap \,{\textsf{coNP}}\) [54]. The state-of-the-art algorithms for mean-payoff games have runtime \(\mathcal {O}(n^2mW)\) (and a runtime of \(\mathcal {O}(nmW)\) for the threshold problem), where n is the number of nodes, m is the number of edges and W is the maximum absolute weight in the game arena [29]. For energy games, the best algorithms are either deterministic with the run time \(\mathcal {O}(\min (mnW, mn2^{n/2}\log W))\) [16, 32] or randomized with the run time \(2^{\mathcal {O}(\sqrt{n \log n})}\) [12].
Combining Quantitative & Qualitative Objectives. Conceptually, fair energy and fair mean-payoff games considered in this paper combine quantitative (i.e., energy or mean-payoff) with qualitative (i.e. strong transition fairness) obligations to constrain the moves of the players in the resulting game.
Combinations of quantitative and qualitative objectives have been studied for several variants of mean-payoff and energy objectives combined with general \(\omega \)-regular goals [13, 14, 18, 21‐24, 30, 36]. In particular, energy parity games were introduced in [21], demonstrating these games’ inclusion in \({\textsf{NP}}\,\cap \,{\textsf{coNP}}\) and polynomial equivalence to mean-payoff parity games, previously studied in [24]. Additionally, the interplay between quantitative objectives (in both optimization and threshold variants) and Boolean constraints has been investigated in a broad range of settings [1‐4, 14, 15, 17, 22, 23, 27, 51], highlighting the richness and diversity of approaches in this area.
It is known that strong transition fairness conditions can be translated into a classical Streett condition, i.e., a subclass of (qualitative) \(\omega \)-regular objectives, by transforming each fair edge \(e=(u,v)\) into a Streett pair \((\{u\},\{e\})\) in the original game arena. If only player 1 (the controller) is constrained by the fairness, this transformation results in an energy (resp. mean-payoff) Streett game. Following [7], Energy Streett games1 can be solved in one of the following ways:
\(\triangleright \)
Encode the Streett energy objective as a \(\mu \)-calculus formula and solve the formula using symbolic fixed-point computations: The computation takes \(\mathcal {O}(n\cdot [b+1]^{\left\lfloor \frac{d}{2}+1 \right\rfloor })\) symbolic steps, where \(b= (d+1) \cdot \left( ((n^2+n)\frac{n}{2}! -1)W\right) \) is an upper bound on the credit a Streett energy game requires, where d is the number of Streett pairs, which in our case corresponds to the number of fair edges. This complexity can be simplified to \(\mathcal {O}\left( (\frac{n}{2}! \cdot W)^{\frac{m}{2}}\right) \) by omitting the polynomial factors where m is the number of edges; which is super-exponential.
\(\triangleright \)
Translate the energy Streett game into a Streett game by encoding the domain of energy levels in the state space. This explodes the state space by multiplying the number of states with the above-mentioned upper-bound b. Using state-of-the-art algorithms for Streett games [43], this gives an algorithm with worst-case super-exponential runtime of \(\mathcal {O}((\frac{n}{2}!W)^{m+1}m!)\).
If, however, player 2 (the environment) is constrained by strong-transition fairness, the above reduction to energy (resp. mean-payoff) Streett games does not apply as the energy or mean-payoff objectives are not symmetric for both players. In this case, the given energy (resp. mean payoff) game is enhanced with a fairness assumption weakening the opponent. While such games have been investigated for qualitative objectives [35], this paper is the first to consider quantitative games under such fairness assumptions.
1.2 Contributions
Based on the above discussion, we distinguish between 1-fair and 2-fair energy (resp. mean-payoff) games, emphasizing which player is additionally constrained by the strong transition fairness condition. We provide a unified framework to solve both classes of games via a novel, gadget-based approach. Our gadgets enable the translation of fair quantitative games into regular quantitative games on a linearly larger state space. This allows solving these games in pseudo-polynomial time, significantly improving the computational complexity for 1-fair quantitative games, compared to the naive approaches outlined above. The origins of these gadget-based techniques can be traced back to the works in [25] and [20], where similar gadgets were employed to convert stochastic parity and Rabin games with almost-sure winning conditions into regular parity and Rabin games. In [35], a gadget-based technique was developed that reduces fair parity games to (linearly larger) regular parity games, demonstrating a quasi-polynomial run time for these games. Our work extends this approach to fair games with quantitative objectives. Concretely, our contributions are as follows.
Fair Mean-Payoff Games:
\(\triangleright \)
Complexity. Using gadgets, we reduce (1- and 2-) fair mean-payoff games to regular mean-payoff games on a game arena with linearly larger number of nodes and edges, and a maximum absolute weight of \(\mathcal {O}(n^2W)\), where n is the number of nodes and W is the maximum absolute weight in the fair game arena. Following the state-of-the-art algorithm of [29], we obtain a complexity of \(\mathcal {O}(n^4mW)\) for solving the fair mean-payoff games for optimal value problem, and a complexity of \(\mathcal {O}(n^3mW)\) for threshold problem.
\(\triangleright \)
Determinacy. The above reduction establishes that fair mean-payoff games are determined irrespective of which player has fairness constraints.
\(\triangleright \)
Strategies. We show that, in 1-fair mean-payoff games, player 1 in general needs infinite memory strategies to win, although finite memory suffices for achieving suboptimal values. Memoryless strategies suffice for player 2. In 2-fair mean-payoff games, player 2 has finite memory winning strategies, whereas memoryless strategies suffice for player 1.
Fair Energy Games:
\(\triangleright \)
Determinacy. In contrast to fair mean-payoff games, we show that fair energy games (with unknown initial credit) are not determined in general. In particular, 2-fair energy games are not determined, whereas 1-fair energy games are. We argue that the lack of determinacy prevents us from constructing similar gadgets to reduce 2-fair energy games to regular energy games.
\(\triangleright \)
Complexity. We introduce a gadget that reduces 1-fair energy games to regular energy games on an arena with linearly larger number of nodes and edges, and a maximum absolute weight of \(\mathcal {O}(n^3W)\). Using the state-of-the-art algorithm of [32], we obtain a complexity of \(\mathcal {O}(n^4mW)\) for solving these games. For 2-fair energy games, we provide simple algorithms to compute the winning regions separately for both players. We show that in 2-fair energy games, player 1’s winning region is the same as in the corresponding energy game where fair edges are treated as regular edges. Meanwhile, player 2’s winning region is the same as in the corresponding 2-fair mean-payoff games with threshold 0. These reductions yield an \(\mathcal {O}(n^3mW)\) algorithm for solving 2-fair energy games.
\(\triangleright \)
Strategies. We show that in fair energy games, the player restricted by transition fairness has finite memory winning strategies whereas memoryless strategies suffice for the respective other player.
In summary, our results show that strong transition fairness can be seamlessly incorporated into quantitative games without significant computational overhead. In fact, just as in the qualitative setting, this simple form of fairness comes virtually for free in the quantitative setting. Our key conceptual insight is that both the simplicity of strong transition fairness, and the effectiveness of gadget-based approaches extend beyond the \(\omega \)-regular domain.
2 Preliminaries
In this section, we introduce the basic notations used throughout the paper. We write \(\mathbb {Q}\) and \(\mathbb {N}\) to denote the set of rational numbers and the set of natural numbers including 0, respectively.
2.1 Weighted Game Arena
A two-player weighted game arena is a tuple \(G= (Q, E, w)\), where \(Q= Q_1 \uplus Q_2\) is a finite set of nodes, \(E \subseteq Q \times Q\) is a set of edges, and \(w: E \rightarrow [-W, W]\) is a weight function that assigns an integer weight to each edge in G, where \(W \in \mathbb {N}\) is the maximum absolute weight appearing in G. The nodes are partitioned into two sets, \(Q_1\) and \(Q_2\), where \(Q_i\) is the set of nodes controlled by Player i for \(i \in \{1,2\}\) and \(Q_1 \cap Q_2 = \emptyset \). For a node q, we write qE to denote the set \(\{e \in E \mid e = (q, q') \text { for } q' \in Q\}\) of all outgoing edges from q and E(q) to denote all successors of q. W.l.o.g., we assume that all nodes have out-degree at least one, i.e., \(E(q) \ne \emptyset \) for all \(q \in Q\). In rest of the paper, we use circles and squares in a figure to denote nodes controlled by player 1 and player 2, respectively.
Plays. A play\(\tau = q_0 q_1 \ldots \in Q^\omega \) on G is an infinite sequence of nodes starting from \(q_0\) such that, \(\forall i \ge 0, (q_i, q_{i+1}) \in E\). We use notations \(\tau [0 ;i] = q_0 \ldots q_i\), and \(\tau [i;j] = q_i \ldots q_j\) to denote the finite prefix and infix of the play \(\tau \), respectively. A node q is said to appear infinitely often in \(\tau \), i.e., \(q \in \texttt{Inf}(\tau )\) if \(\forall i, \exists j \ge i\), such that \(q_j =q\). We naturally extend the notion of appearing infinitely often in a play for the edges. We let \(\texttt{plays}(G)\) denote the set of all plays on G, and let \(\texttt{plays}(G,q)\) denote the set of all plays starting from node q.
Strategies. A strategy\(\sigma \) for player \(i \in \{1, 2\}\) (or, a player i-strategy) is a function \(\sigma : Q^* \cdot Q_i \mapsto E\) where for all \(H \cdot q \in Q^* \cdot Q_i\), \(\sigma (H \cdot q) \in qE\). Intuitively, from every node \(q \in Q_i\), a strategy for player i assigns an outgoing edge of that node based on a history \(H \in Q^*\).
For a player i strategy \(\sigma \), a play \(\tau = q_0 q_1 \ldots \) is called a \(\sigma \)-play if it conforms with \(\sigma \), i.e., for all \(j \in \mathbb {N}\) with \(q_j \in Q_i\), it holds that \(\sigma (q_0 \ldots q_j) = (q_j,q_{j+1})\). Given a strategy \(\sigma \) we denote the restriction of sets \(\texttt{plays}(G)\) and \(\texttt{plays}(G,q)\) to \(\sigma \)-plays with \(\texttt{plays}_{\sigma }(G)\) and \(\texttt{plays}_{\sigma }(G,q)\). Similarly, \(\texttt{play}_{\sigma , \pi }(G, q)\) denotes the unique play from q conforming with player 1 and player 2 strategies \(\sigma \) and \(\pi \).
Let M be a set called memory. A player i strategy \(\sigma \) with memory M can be represented as a tuple \((M, m_0, \alpha , \beta )\), where \(m_0 \in M\) is the initial memory value, \(\alpha : M \times Q \rightarrow M\) is the update function, and \(\beta : M \times Q_i \rightarrow Q\) is the function prescribing next state. Intuitively, if the current node is a player i node q and m is the current memory value, the strategy \(\sigma \) selects \(q' = \beta (m, q)\) as the next node and updates the memory to \(\alpha (m, q)\). If M is finite, then we call \(\sigma \) a finite memory strategy; otherwise it is an infinite memory strategy. Formally, given a history \(H\cdot q\in Q^*\cdot Q_i\), \(\sigma (H\cdot q) = \beta (\hat{\alpha }(m_0, H), q)\), where \(\hat{\alpha }\) extends \(\alpha \) to sequences of nodes canonically. A strategy is called memoryless or positional if \(|M| = 1\). For such memoryless strategy \(\sigma \), it holds that \(\sigma (H_1 \cdot q) = \sigma (H_2 \cdot q)\) for every history \(H_1,H_2 \in Q^*\). We denote it as \(\sigma (q)\) for convenience. For any positional strategy \(\sigma \) of player i, we define \(G_\sigma \) to be the subgame arena \((Q,E',w)\) of G, where \(E' = \{(q, \sigma (q)) \mid q \in Q_i\} \cup \{qE \mid q \in Q_{3-i}\}\). Note that in this subgame arena, each player i node has exactly one successor according to the strategy \(\sigma \).
Weighted Games and Objectives. A weighted game is a tuple \((G, \varphi )\), where G is a weighted game arena and \(\varphi \subseteq Q^\omega \) is an objective for player 1. A play \(\tau \) is winning for player 1 if \(\tau \in \varphi \), else it is winning for player 2. A player i strategy \(\sigma \) is winning from some node q, if all \(\sigma \)-plays starting from q are winning for player i. We denote the winning regions of player i by \(\texttt{Win}_i(G, \varphi )\), or shortly \(\texttt{Win}_i\), when \((G, \varphi )\) is clear from the context. Formally, the winning regions are defined as follows where \(\varSigma _i\) is the set of all player i strategies:
A game \((G, \varphi )\) is called determined, if \(Q = \texttt{Win}_1 \cup \texttt{Win}_2\).
Given a finite infix \(H= q_0 \ldots q_k\) of a play in G, we denote the (total) weight and the average weight of \(H\) by \(w(H) = \sum _{i=0}^{k-1} w(q_i,q_{i+1})\) and \(\texttt{avg}(H) = \frac{w(H)}{k}\), respectively. Furthermore, we denote the (limit) average weight of a play \(\tau \) by \(\texttt{avg}(\tau ) = \liminf _{i \rightarrow \infty } \texttt{avg}(\tau [0;i])\).
Mean-Payoff Games. A mean-payoff game is a weighted game with a mean-payoff objective for a given threshold value \(v \in \mathbb {Q}\), which is defined as \(\texttt{MP}_v = \{\tau \in Q^\omega \mid \texttt{avg}(\tau ) \ge v\}\). Intuitively, a play is winning for player 1 if the average weight of the play is above a certain threshold value v. Note that, mean-payoff games are prefix independent as any finite prefix of a play \(\tau \) does not affect the limit average weight of \(\tau \).
In this work, without loss of generality, we focus on mean-payoff objective \(\texttt{MP}_0\) with threshold value \(v = 0\). It is easy to see that for any value v, the weighted mean-payoff game \((G, \texttt{MP}_v)\) with \(G = (Q,E,w)\) can be reduced to a mean-payoff game \((G', \texttt{MP}_0)\) by subtracting v from the weights of all edges in G, i.e., \(G' = (Q,E,w')\) where \(w'(q,q') = w(q,q') - v\) for all \((q,q') \in E\).
The optimal value of a mean-payoff game is the maximum value v for which player 1 has a winning strategy with threshold v. A winning strategy of player 1 that achieves this optimal value is called an optimal value strategy. The optimal value problem is to compute the optimal values in a mean-payoff game.
Energy Games. An energy objective w.r.t. a given initial credit \(c \in \mathbb {N}\) is defined as \(\texttt{En}_c = \{\tau \in Q^\omega \mid c+ w(\tau [0;i]) \ge 0,\ \forall i \in \mathbb {N}\}\). Intuitively, a play belongs \(\texttt{En}_c\) if the total weight (‘energy level’ starting from c) of the play remains non-negative along the play. An energy game is a weighted game with an energy objective with unknown initial credit, denoted by \(\texttt{En}\), where player 1 wins from some node q if there exists an initial credit \(c \in \mathbb {N}\) such that she can ensure the objective \(\texttt{En}_c\) from q. Formally, the winning regions are defined as follows, for \(\varphi _c = \texttt{En}_c\):
Note that, in contrast to mean-payoff games, the energy objective is not a prefix-independent objective as the total weight of each prefix has to be non-negative along any play. However, it is known that such energy games are log-space equivalent to mean-payoff games [16]. Furthermore, it is known that both energy games and mean-payoff games are positionally determined [18, 33] i.e., \(Q = \texttt{Win}_1 \cup \texttt{Win}_2\) and both players have positional winning strategies.
2.2 Fair Game Arena
A fair game arena is a tuple \((G, E_f)\), where G is a weighted game arena as defined above and \(E_f \subseteq E\) is a given set of ‘fair edges’. We call the non-fair edges \(E\setminus E_f\) ‘regular’, and a node q ‘fair’ if it is the source node of a fair edge, i.e., \(qE\cap E_f \ne \emptyset \). Let \(Q_f\) be the set of all fair nodes in G. We investigate the scenario where all fair nodes are owned by the same player. If \(Q_f \subseteq Q_1\), we call the game arena 1-fair and if \(Q_f \subseteq Q_2\), we call it 2-fair. For brevity, we sometimes denote the fair game arena \((G,E_f)\) by G and keep the set of fair edges \(E_f\) implicit. Given a fair node q, we write \(qE_f\) to denote the set \(\{e \in E_f \mid e = (q, q') \text { for } q' \in Q\}\) of all fair outgoing edges from q and \(E_f(q) = \{q' \mid (q,q')\in E_f\}\) to denote the set of successors of q via fair edges.
A play \(\tau \) is fair if for all nodes \(q \in \texttt{Inf}(\tau )\) and for all edges \(e \in qE\), if \(e \in E_f\), then \(e \in \texttt{Inf}(\tau )\). We let \(\texttt{plays}^f(G)\) denote the set of all fair plays on \((G, E_f)\). We say a strategy \(\sigma \) for player i is fair if \(\texttt{plays}_{\sigma }(G) \subseteq \texttt{plays}^f(G)\).
Fair Mean-Payoff/Energy Games. An i-fair mean-payoff game with objective \(\varphi = \texttt{MP}_v\) is a tuple \((G, E_f, \varphi ^f)\), where \((G, E_f)\) is an i-fair game arena, and \(\varphi ^f\) is the objective with the respective fairness condition defined as follows:
$$\begin{aligned} \varphi ^f = {\left\{ \begin{array}{ll}\varphi \cap \texttt{plays}^f(G) & \text { if } (G, E_f) \text { is 1-fair} \\ \varphi \cup \texttt{plays}(G) \setminus \texttt{plays}^f(G) & \text { if } (G, E_f) \text { is 2-fair}\end{array}\right. } \end{aligned}$$
(5)
Intuitively, a play is winning for player i in i-fair game if it satisfies both the fairness condition and the player’s corresponding objective, i.e., \(\varphi \) for player 1 and \(\lnot \varphi \) for player 2.
Similarly, an i-fair energy game with energy objective \(\texttt{En}\) is a tuple \((G, E_f, \texttt{En}^f)\) where the winning regions are defined as in (3)-(4) for \(\varphi _c = \texttt{En}^f_c\).
3 Example: Mean-Payoff vs Fair Mean-Payoff Games
In this section, we depict the intricacy of fair mean-payoff games in comparison to regular mean-payoff games via the following example:
Consider the game arena depicted in Fig. 1 with both the nodes belonging to player 1. With regular mean-payoff objective with threshold 0, player 1 has a simple optimal positional strategy: at q, play the self-loop (q, q) and from p play the edge (p, q). This strategy is winning for player 1 because the limit average weight of any play conforming to this strategy is 1. Note that the strategy is also an optimal value strategy as the optimal value of the game is 1.
Fig. 1.
.
Now let us consider the game arena to be 1-fair with a fair edge (q, p). Now the fair mean-payoff objective \(\texttt{MP}_0^f\) for player 1 is to ensure that the limit average weight of the play is \(\ge 0\) along with the fairness condition that says if q appears infinitely often in a play, so does the edge (q, p).
First note that there is no positional strategy that can ensure both fairness and mean-payoff objective and hence winning for player 1. Now, consider the following finite memory strategy for player 1: the strategy takes the self-loop (q, q) for k times before taking (q, p) once, and this sequence of \(k+1\) choices is repeated forever. The resulting play uses the fair edge (q, p) infinitely often and hence it is fair. For \(k \ge 4\), this strategy is winning as the limit average of the plays conforming to this strategy is at least 0. In fact, we can show that for all \(\epsilon > 0\), it is possible to choose a large enough k, such that player 1 ensures a limit average weight of at least \(1-\epsilon \).
Finally, consider the following infinite-memory strategy for player 1: the strategy is played in rounds; in round \(i\ge 0\), the strategy plays (q, q) for i times, then plays (q, p) once and progresses to round \(i + 1\). This fair strategy ensures player 1 achieves a limit average weight of value 1, and it is therefore an optimal value strategy. However, it is not hard to see that there is no finite-memory optimal value strategy for player 1 in this game. In the following sections, we formally present how to solve fair mean-payoff games and discuss the memory requirements for each player to achieve these winning strategies.
4 Solving Fair Mean-Payoff Games
In this section, we present algorithms for solving fair mean-payoff games. The algorithms transform a fair mean-payoff game into a ‘regular’ mean-payoff game using gadgets. We introduce two gadgets depending on which player owns the fair edges as depicted in Fig. 2. Given an i-fair mean-payoff game G, we replace all fair nodes with the corresponding i-fair gadgets and obtain an equivalent mean-payoff game \(G'\) such that \((G, E_f, \texttt{MP}^f_0)\) is winning for player i if the mean-payoff game \((G', \texttt{MP}_0)\) is winning for player i. In particular, we prove the following.
Theorem 1
Let \((G, E_f, \texttt{MP}^f_0)\) be a fair mean-payoff game with threshold 0, where \(G = (Q, E, w)\), \(w : E \rightarrow [-W, W]\), and \(|Q|=n\). Then there exists a mean-payoff game \(G'= (Q',E',w')\) where \(Q' \supseteq Q\), \(|Q'|\le 6n\) and \(w' : E' \rightarrow [-W', W']\) with \(W' = n^2W + n\) such that \(\texttt{Win}_i(G) = \texttt{Win}_i(G') \cap Q\) for \(i \in \{1, 2\}\).
Standard algorithms for mean-payoff games [29] with Thm. 1 gives an \(\mathcal {O}(n^3mW)\) time algorithm (with \(\left|{E}\right| = m\)) for solving fair mean-payoff games with threshold and an \(\mathcal {O}(n^4mW)\) time algorithm for the optimal value problem. As regular mean-payoff games are determined, we also get the following from Thm. 1:
Theorem 2
Fair mean-payoff games are determined.
The rest of this section discusses the proof of Thm. 1 for 1-fair mean-payoff games in Sec. 4.1 and for 2-fair mean-payoff games in Sec. 4.2. The detailed proof of Thm. 1 for 2-fair mean-payoff games is provided in [8, App. B]. Finally, Sec. 4.3 discusses the memory requirements of strategies in fair mean-payoff games resulting from the gadget-based reductions.
Gadgets for converting fair mean-payoff games to mean-payoff games. Edges are labeled with their weights. The edges labeled with w represent: an edge from a gadget node to a node \(q' \in E(q)\) or \(E_f(q)\) carry the weight \(w(q, q')\).
Gadget Construction & Intuition. Let \((G, E_f, \texttt{MP}^f_0)\) be a 1-fair mean-payoff game. We construct the gadget game\(G'\) by replacing every fair node in \(q \in Q_f\) in G, with its 3-step gadget presented in Fig. 2a. That is, the incoming edges of q is redirected to node q at the root, and the outgoing edges on the third step lead to \(E_f(q)\) and E(q), the fair successors and successors of q, respectively. The formal construction of \(G'\) can be found in [8, App. A].
For notational convenience, for each \(q \in Q_f\), we denote the leftmost branch \(q \rightarrow q_l \rightarrow q_\text {nW+1}\) of the gadget as fair branch\(\texttt{br}^{q}_{\texttt {fair}}\), the middle branch \(q \rightarrow q_{l} \rightarrow q_{0}\) as the simulation branch\(\texttt{br}^{q}_{\texttt {sim}}\) and the rightmost branch \(q \rightarrow q_r \rightarrow q_{\,\texttt{ESC}} \) as the escape branch\(\texttt{br}^{q}_{\texttt {esc}}\). Intuitively, from a fair node q, player 1 can escape to a part of the game that doesn’t contain q and is player 1 winning (according to the current player 1 strategy) by taking the escape branch and therefore paying a high negative payoff. Since by this escape choice q is guaranteed to be seen only finitely often, the negative payoff associated with the escape edge does not change the winner of the game. Now assume there is no such winning escape choice for player 1 from q. Then from q, all player 1 winning play visits q infinitely often, and thus is forced to visit all of q’s outgoing fair edges infinitely often. If taking one of its fair outgoing edges pushes the game into a player 2 winning region that does not contain q (according to some player 2 strategy), then in the gadget game player 2 can pay a high positive payoff and choose the fair branch with the correct successor to escape to a player 2 winning region. So, in a way “fair branch is the escape branch for player 2”. However, player 2 can take this escape branch to win from q, only if player 1 cannot take her escape branch to win. The difference in the amplitude of weights between the escape branches of the two players (i.e. \(\texttt{br}^{q}_{\texttt {esc}}\) and \(\texttt{br}^{q}_{\texttt {fair}}\)) stems from this hierarchy between the escape choices of the players. If neither player has an escape choice, then the middle branch \(\texttt{br}^{q}_{\texttt {sim}}\) faithfully simulates the fair mean-payoff game without adding any additional weights to the play via the gadget edges to alter the winner.
Using this intuition, we now prove both directions of Thm. 1 separately for 1-fair mean-payoff games.
1. Proof of \(\mathbf {(\texttt{Win}_1(G') \, \cap \,Q \, \subseteq \,\texttt{Win}_1(G))}\): Let \(\sigma '\) be a positional player 1 strategy that wins q in \(G'\) for the regular mean-payoff objective. We construct a player 1 strategy \(\sigma \) that wins q in G.
Consider the subgame arena \(G'_{\sigma '}\) of \(G'\). All cycles in \(G'_{\sigma '}\) are non-negative; else player 2 can force to eventually only visit a negative cycle and therefore construct a play in \(G'_{\sigma '}\) with negative mean-payoff value.
Using \(\sigma '\), we construct \(\sigma \) in G as follows:
a.
If \(q' \not \in Q_f\), then set \(\sigma \) to be positional at \(q'\) with \(\sigma (q') = \sigma '(q')\).
b.
If \(\sigma '(q') = q_r\) for some fair node \(q' \in Q_f\), then set \(\sigma \) to be positional at \(q'\) with \(\sigma (q') = \sigma '(q'_{\,\texttt{ESC}})\). Intuitively this says if for a fair node \(q'\), \(\sigma '\) asks to choose the escape branch of the gadget, then \(\sigma \) follows \(\sigma '\) to choose that branch and moves to the corresponding ‘escape node’ in G.
c.
If \(\sigma '(q') = q_l\) for some fair node \(q' \in Q_f\), then we set \(\sigma \) to be an infinite memory strategy at \(q'\) that is played in rounds: consider an order on the fair successors of \(q'\). In round \(i \ge 0\), \(\sigma \) chooses the ‘preferred successor’ \(\sigma '(q'_0)\) exactly i times and then chooses the \(i^\text {th}\) (modulo \(|E_f(q')|\)) fair successor.
Now we prove that all \(\tau \in \texttt{plays}_\sigma (G)\) are winning for player 1 in G. In particular, we will show that \(\tau \) is fair and \(\texttt{avg}(\tau ) \ge 0\).
For a play \(\tau = q^0 q^1 \ldots \in \texttt{plays}_\sigma (G)\), we construct its extension\(\tau '\) in \(G'\) inductively as follows: we start with \(q^0\) and \(i=0\) and with increasing i,
If \(q^i \not \in Q_f\), append \(\tau '\) with \(q^{i+1}\);
If \(\sigma (H\cdot q^i)\) is defined using Item b. i.e., \(\sigma '(q^i) = q^i_r\) then append \(\tau '\) with \(\texttt{br}^{q^i}_{\texttt {esc}} \rightarrow q^{i+1}\). In particular, we append \(\tau '\) with \(q^i_r \cdot q^i_{\,\texttt{ESC}}\cdot q^{i+1}\).
If \(\sigma (H \cdot q^i)\) is defined using Item c., then
if \(q^{i+1} = \sigma '(q^i_{0})\), append \(\tau '\) with \(\texttt{br}^{q^i}_{\texttt {sim}}\rightarrow q^{i+1}\) i.e., with \(q^i_l \cdot q^i_{0} \cdot q^{i+1}\) ;
else, append \(\tau '\) with \(\texttt{br}^{q^{i}}_{\texttt {fair}} \rightarrow q^{i+1}\), i.e. \(q^i_l \cdot q^i_\text {nW+1} \cdot q^{i+1}\).
Clearly, \(\tau '\) is a play in \(G'_{\sigma '}\); hence it contains only non-negative cycles. Further, the restriction of \(\tau '\) to the nodes Q of G, denoted by \(\tau '|_Q\), is exactly \(\tau \).
Let a ‘tail’ of \(\tau \) denote an infinite suffix \(\hat{\tau }\) of \(\tau \) that contains only the nodes and edges visited infinitely often in \(\tau \); and let \(\hat{\tau }'\) be the extension of \(\tau \) in \(G'\). We denote the subgraph of \(G'_{\sigma '}\) restricted to the nodes and edges in \(\hat{\tau }'\) by \(G'_{\hat{\tau }'}\).
We first show that \(\tau \) is fair. It is sufficient to show that \(\hat{\tau }\) does not contain fair nodes p for which \(\sigma (p)\) is defined via Item b., because for all the other fair nodes in \(\hat{\tau }\), \(\tau \) visits all their fair successors infinitely often (Item c.). Let p be a node for which \(\sigma (p)\) is defined via Item b.. Then \(\sigma '(p) = p_r\). As \(\sigma '\) is positional, only the escape branch of p exists in \(G'_{\sigma '}\), carrying the weight \(-n^2W - n\). Since p is visited infinitely often, there is a (simple) cycle in \(G'_{\sigma '}\) that passes through p, and thus sees the weight \(-n^2W -n\). In order to maintain a non-negative weight, the cycle needs to contain n-many fair branches (carrying weight \(nW+1\)), which is not possible since there are at most \(n-1\) many fair branches in \(G'_{\sigma '}\). With this we conclude that \(\tau \) is fair.
Now we prove that \(\texttt{avg}(\tau ) \ge 0\). First let us make an observation about the cycles in \(G'_{\sigma '}\) that use only simulation branches.
Observation (sim-cycles)
We call cycles \(\mathbf {c'}\) in \(G'_{\sigma '}\) that do not contain any fair or escape branches sim-cycles. That is, \(\mathbf {c'}\) contains only simulation branches. Being part of \(G'_{\sigma '}\), \(\textbf{c}\) has non-negative weight. Since all the gadget branches in \(\mathbf {c'}\) carry 0 weight, the restriction \(\textbf{c} = \mathbf {c'}|_Q\) is a non-negative weight cycle in G.
We saw that \(\hat{\tau }\) does not contain nodes defined using Item b.. I.e., for all fair nodes p in \(\hat{\tau }\), \(\sigma \) is defined via Item c., and \(G'_{\hat{\tau }'}\) contains the branches \(\texttt{br}^{p}_{\texttt {fair}}\) and/or \(\texttt{br}^{p}_{\texttt {sim}}\). Thus, all cycles in \(\hat{\tau }'\) are either sim-cycles, or visit a fair branch.
If \(\hat{\tau }\) does not contain any fair nodes, \(\hat{\tau }= \hat{\tau }'\), and \(\texttt{avg}(\tau ) \ge 0\) easily follows. Now we assume \(\hat{\tau }\) contains at least one fair node, and use the following easy-to-verify remark to show \(\texttt{avg}(\tau ) \ge 0\):
Remark 1
Given a play \(\rho \) and \(\epsilon >0\), if there exists a \(k \in \mathbb {N}\) and a tail \(\hat{\rho }\) of \(\rho \) such that every k-length infix \(\hat{\rho }_k\) of \(\hat{\rho }\) satisfies \(\texttt{avg}(\hat{\rho }_k) \ge -\epsilon \), then \(\texttt{avg}(\rho ) \ge -\epsilon \).
Let \(\epsilon > 0\) be arbitrary. Let \(k\in \mathbb {N}\) such that \(\frac{n^2W}{k} < \epsilon \). Since \(\hat{\tau }\) has at least one fair node, Item c. is triggered infinitely often to construct the strategy \(\sigma \). Therefore, the round (in the sense of Item c.) will grow unboundedly bigger. Thus, for any k, we can get a tail \(\hat{\tau }\) of \(\tau \) that is in round k. In \(\hat{\tau }\), for every fair node, their edge to their preferred successor is taken at least k-many times between any two occurrences of their other (fair) outgoing edges. Then in \(\hat{\tau }'\), the simulation branches of fair nodes are visited at least k-many times in between two occurrences of fair branches. Therefore, in \(\hat{\tau }'\) each infix \(\hat{\tau }'_k\) of length k visits the fair branch of each node at most once. Consequently, there are at most n-many simple cycles in \(\hat{\tau }'_k\) that visits a fair branch, and all its other simple cycles are sim-cycles. Now, total weight of n-many simple cycles that are not sim-cycles are \(\ge -n^2W\), and since all the sim-cycles have non-negative weight, \(\texttt{avg}(\tau _k) \ge \frac{-n^2W}{k} \ge - \epsilon \). Using the fact from the previous paragraph, we get that \(\texttt{avg}(\tau ) \ge -\epsilon \). This implies that for any \(\epsilon > 0\), \(\texttt{avg}(\tau ) \ge -\epsilon \). Hence, \(\texttt{avg}(\tau ) \ge 0\).
This concludes the proof of the first direction.
2. Proof of \(\mathbf {(\texttt{Win}_2(G') \, \cap \,Q \, \subseteq \,\texttt{Win}_2(G))}\): Analogous to the previous part, we consider a positional winning strategy \(\pi '\) of player 2 in \(G'\) and construct, this time, a positional winning strategy \(\pi \) for player 2 in G. Note that, none of the fair nodes in G belong to player 2 and hence the construction of \(\pi \) is quite straight forward: for all \(q \in Q_2\), we set \(\pi (q) = \pi '(q)\). We define \(G'_{\pi '}\) as the subgame restricted to \(\pi '\), as before.
For a play \(\tau = q^0 q^1 \ldots \in \texttt{plays}_\pi (G)\), we define its extension\(\tau '\) in \(G'\) inductively as follows: we start from with \(q^0\) and \(i = 0\), and with increasing i,
If \(q^i \not \in Q_f\), append \(\tau '\) with \(q^{i+1}\); Otherwise,
If \(\texttt{br}^{q^i}_{\texttt {sim}}\) exists in \(G'_{\pi '}\), append \(\tau '\) with \(q^i_l \cdot q^i_{0} \cdot q^{i+1}\);
If \(\texttt{br}^{q^i}_{\texttt {sim}}\) does not exist in \(G'_{\pi '}\):
If \(q^{i+1} = \pi '(q^i_\text {nW+1})\), append \(\tau '\) with the fair branch i.e. \(q^i_l \cdot q^i_\text {nW+1} \cdot q^{i+1}\),
Otherwise, append it with the escape branch, i.e. \(q^i_r \cdot q^i_{\,\texttt{ESC}} \cdot q^{i+1}\).
We define the tail of \(\tau \) as \(\hat{\tau }\) and its extension \(\hat{\tau }'\), analogous to the previous part. We denote the subgraph of \(G'_{\pi '}\) restricted to the nodes and edges in \(\hat{\tau }'\) by \(G'_{\hat{\tau }'}\).
Let \(\tau \in \texttt{plays}_\pi (G)\) be a play in G that conforms with \(\pi \). If \(\tau \) is not fair, it is automatically won by player 2. Therefore, assume that \(\tau \) is fair. We show that all the simple cycles in \(\hat{\tau }\) has negative weight. For this, we use the fact that its extension \(\tau '\) is a play in \(G'_{\pi '}\) and hence all the cycles in \(G'_{\hat{\tau }'}\) have negative weight. Since the length of simple cycles are bounded by n, this gives us \(\texttt{avg}(\tau ) < 0\).
The main argument is the absence of fair branches in \(G'_{\hat{\tau }'}\), introduced in Claim 1.
Claim 1
If \(\tau \) is fair, there exist no fair branches \((\texttt{br} _{\texttt {fair}})\) in \(G'_{\hat{\tau }'}\).
Before proving the claim, we discuss how it implies that all simple cycles in \(\hat{\tau }\) are negative, resulting \(\texttt{avg}(\tau ) < 0\). From the definition of extension, absence of fair branches in \(G'_{\hat{\tau }'}\) implies that either (i) for all \(q \in Q_f\) only \(\texttt{br}^{q}_{\texttt {sim}}\) exists in \(G'_{\hat{\tau }'}\), or (ii) for some \(q \in Q_f\), only \(\texttt{br}^{q}_{\texttt {esc}}\) exists in \(\hat{\tau }'\). By construction of \(\tau '\), case (ii) above implies the existence of a fair node \(q \in Q_f\) that appears infinitely often in \(\tau \) but does not take all its fair outgoing edges, in particular \(q \rightarrow \pi '(q_\text {nW+1}) \in E_f(q)\) infinitely often. This makes \(\tau \) unfair, contradicting our assumption. In case of (i), since all simple cycles \(\textbf{c}'\) in \(\hat{\tau }'\) are negative and none of the gadget nodes contribute any weight due to only \(\texttt{br} _{\texttt {sim}}\) existing in \(\hat{\tau }'\), we conclude that the cycles \(\textbf{c} = \mathbf {c'}|_{Q}\) in \(\hat{\tau }\) have negative weight. This implies that \(\texttt{avg}(\tau ) < 0\).
By the above-mentioned argument, proving Claim 1 concludes the second direction of the proof.
Proof of Claim 1. As discussed above, whenever \(\texttt{br}^{q}_{\texttt {esc}}\) is in \(G'_{\hat{\tau }'}\) for a node q, \(\texttt{br}^{q}_{\texttt {fair}}\) is also in it. Now we remove all the escape branches from \(G'_{\hat{\tau }'}\) and obtain the subgraph S. Note that S has no dead-ends, since for all q for which \(\texttt{br}^{q}_{\texttt {esc}}\) got removed from \(G'_{\hat{\tau }'}\), \(\texttt{br}^{q}_{\texttt {fair}}\) was also in \(G'_{\hat{\tau }'}\).
For all nodes q in S, either \(\texttt{br}^{q}_{\texttt {fair}}\) or \(\texttt{br}^{q}_{\texttt {sim}}\) is in S. As a subgraph of \(G'_{\pi '}\), all cycles in S have negative weight. It is easy to see that a fair branch cannot lie on a simple cycle in S, because fair branches carry weight \(nW+1\) and the other edges come either from \(\texttt{br} _{\texttt {sim}}\) carrying weight 0, or from G carrying weight \(\ge -W\). Hence, a simple cycle containing a fair branch would have positive weight.
Now assume fair branches exist in \(\hat{\tau }'\), but not on cycles of S. Then all cycles in S consist only of simulation branches. However, nodes with simulation branches have the same outgoing edges in \(G'_{\hat{\tau }'}\) and in S. Since every node in S is visited infinitely often in \(\tau \), \(\tau \) will eventually enter cycles of S and never leave them, since these nodes have the same outgoing edges in \(G'_{\hat{\tau }'}\). This implies fair branches are not infinitely often visited in \(\tau \), and concludes the proof of Claim 1. \(\square \)
Observing page constrains, we provide the proof of Thm. 1 for 2-fair mean-payoff games in [8, App. B] and only discuss its differences to Sec. 4.1 here.
Interestingly, the player 2 gadget for 2-fair games (Fig. 2b) is exactly the dual of the player 1 gadget for 1-fair games (Fig. 2a). This is surprising, as the winning objectives of player 1 and 2 are not exactly dual in these games. While player 1 in 1-fair games is expected to win the vertices with optimal value 0 (that is, the best value a player 1 strategy can achieve from these nodes is 0, and getting \(\epsilon \)-close to the best possible value isn’t sufficient to win); for player 2 to win a vertex in a 2-fair game, it is sufficient for him to get \(\epsilon \)-close to the best possible value he can achieve from this vertex. As we will see in the next chapter, these differences in the objectives’ behavior w.r.t. optimal values reflect drastically in the required strategy sizes. Namely, in 2-fair games finite strategies are sufficient whereas in 1-fair games infinite strategies are required to win.
It is therefore surprising that this imbalance in objectives does not demand any changes in the gadget’s structure for proving Thm. 1 in the case of 2-fair mean-payoff games. The main difference w.r.t. the proof form Sec. 4.1 lies in the construction of winning strategies for the fair player. In particular, the proof for 1-fair games (in Sec. 4.1) is slightly more complicated due to the required infinite strategy construction for player 2. On the other hand, the proof of 2-fair games (in [8, App. B]) reveals that a finite memory is sufficient for a winning player 2 strategy in 2-fair games.
4.3 Strategy Complexity for Fair Mean-Payoff Games
We list an overview of results on strategy requirements for fair mean-payoff games. Most of these results follow from the proofs of Thm. 1. We discussed in Sec. 3 that player 1 may need infinite memory to achieve an optimal value in a 1-fair mean-payoff game. Lem. 1 shows that player 1 can reach \(\epsilon \)-close to the optimal value with finite memory strategies.
Lemma 1
Given a 1-fair mean-payoff game \((G,E_f,\texttt{MP}^f)\), let the optimal value from some node \(q_0\) is v. Then, for all \(\epsilon > 0\), there exists a finite-memory strategy of player 1 that is winning from \(q_0\) in fair mean-payoff game \((G,E_f,\texttt{MP}(v-\epsilon ))\).
Proof
W.l.o.g, we show this for \(v=0\). In the proof of Thm. 1, we construct an infinite memory strategy \(\sigma \) for player 1 where at \(i^\text {th}\) round, player 1 plays the preferred successor i times and then plays a fair successor. Any \(\sigma \) play has the following property: for any \(\epsilon \), there exists a tail of the play such that the average weight of every k-length infix of the tail is at least \(-\epsilon \). We fix this k and modify the strategy construction in Item c. to play the preferred successor k times and then play a fair successor in every round. By Rem. 1, this finite memory strategy ensures the mean-payoff value of any play is at least \(-\epsilon \). \(\square \)
The above lemma entails that in a 1-fair mean-payoff game with threshold value 0, player 1 has a finite memory strategy from a node \(q \in \texttt{Win}_1\) if the optimal value is strictly larger than 0. On the other hand, in 2-fair mean-payoff games getting \(\epsilon \)-close to the best value achievable from a vertex is always sufficient to ensure winning for player 2. Intuitively, for this reason, player 2 has finite memory winning strategies in 2-fair mean-payoff games.
Lemma 2
Given a 2-fair mean-payoff game \((G,E_f,\texttt{MP}^f)\), for all \(q \in \texttt{Win}_2\), there exists a finite-memory strategy of player 2 that is winning from q.
Finally, the proofs of Thm. 1 from Sec. 4.1 (resp. [8, App. B]) reveal the existence of memoryless winning player 2 (resp. player 1) strategies in 1-fair (resp. 2-fair) mean-payoff games.
Lemma 3
For all fair mean-payoff games, memoryless strategies are sufficient for the player who does not own the fair nodes.
5 Solving Fair Energy Games
In this section, we aim to extend our gadget-based approach to solve fair energy games. Intuitively, gadget-based approaches transfer the determinacy of regular (qualitative or quantitative) objectives to their fair variants, as demonstrated in [35] for fair parity games and by the proofs of Thm. 1 for fair mean-payoff games. Conceptually, these techniques build on finding winning strategies for either player in the fair game – based on their winning strategies in the gadget game – with similar infinite behavior. Therefore, before attempting a gadget-based approach for fair games, we need to ensure that these games are determined.
In this section, we show that 2-fair energy games are not determined, whereas 1-fair energy games are. While due to the above-mentioned reason we cannot construct gadgets for 2-fair energy games, we give simple algorithms to compute both \(\texttt{Win}_1\) and \(\texttt{Win}_2\). For 1-fair energy games, we observe that the gadget in Fig. 2b falls short, and we present new gadgets.
5.1 Discussion on Determinacy of Energy Games
Whenever \(\varphi _c\) is a Borel set, the following holds due to Borel determinacy [39]:
As \(\texttt{En}_c\) and \(\texttt{En}^f_c\) are Borel sets, the equation holds, showing that energy and fair energy games are determined under a fixed credit c. Furthermore, this equality combined with the negation of Eq. (1) defining \(\texttt{Win}_1\), yields the following formulation of \(Q \setminus \texttt{Win}_1\):
Again, this formulation holds for both energy and fair energy games. Clearly it follows that a (fair) energy game is determined if and only if Eq. (4) is equivalent to Eq. (6). In fact, if we can restrict the quantification over c in Eq. (6) to a finite set, then we can swap \(\forall c \in \mathbb {N}\) and \(\exists \pi \in \varSigma _2\), which yields the desired equivalence, showing the game is determined. This is indeed the case in energy games: Whenever player 1 wins from a node, it wins with initial credit nW. Dually, whenever player 2 wins w.r.t. initial credit nW, it wins against every initial credit. That is, the quantification over the c can be restricted to [0, nW].
Using this trick, we show in Sec. 5.3 that 1-fair energy games are determined. However, we demonstrate in the next section that this does not hold for 2-fair energy games and that these games are not determined.
5.2 2-fair Energy Games
We start by showing that 2-fair energy games are not determined.
Theorem 3
2-fair energy games are not determined.
Proof
Recall that energy games are determined if and only if Eq. (4) is equivalent to Eq. (6). We provide a counterexample to this equivalence by the game graph in Fig. 3. Any fair strategy \(\pi \) for player 2 takes the edge \((q,q')\) after finitely many steps, say after c steps. Then, the unique strategy \(\sigma \) for player 1, which takes the self-loop on \(q'\), wins the play \(\texttt{play}_{\sigma }(G,q)\) with respect to the initial credit c. Thus, player 2 has no winning strategy. However, player 1 has no winning strategy either since for any initial credit c, there exists a player 2 strategy that ensures the energy of every play drops below 0. Namely, any strategy that takes the self-loop of q more than c times achieves this. \(\square \)
Fig. 3.
.
This occurs as player 2 can delay taking his fair edges enough to violate any given c while still satisfying fairness condition in the suffix. Hence, if player 2 can force a negative cycle, then he can use it to violate any initial credit. In contrast, player 1’s objective remains the same as in the regular energy game: she wins from a node iff she can prevent player 2 from forcing a negative cycle from that node. This leads to the following result, which is proven in [8, App. C].
Theorem 4
Given a 2-fair energy game \((G,E_f,\texttt{En})\), the set of winning nodes for player 1 is the same as the set of winning nodes for player 1 in the (regular) energy game \((G,\texttt{En})\).
Lemma 4
In 2-fair energy games, player 1 has memoryless winning strategies.
We note that Lem. 4 is a corollary of Thm. 4. As 2-fair energy games are not determined, \(\texttt{Win}_2 \ne Q \setminus \texttt{Win}_1\). We present a simple reduction to compute \(\texttt{Win}_2\) and resulting memory requirements of strategies as a corollary of its proof.
Lemma 5
Given a 2-fair energy game \((G,E_f,\texttt{En})\), the set of winning nodes for player 2 is the same as the set of winning nodes for player 2 in the 2-fair mean-payoff game \((G,E_f, \texttt{MP}^f_0)\).
Proof
Take a player 2 strategy \(\pi \) that wins from q in the 2-fair mean-payoff game. Then, for any \(\tau \in \texttt{plays}_{\pi }(G, q)\), \(\texttt{avg}(\tau ) = - \epsilon \) for some positive \(\epsilon \). That is, there exists an infinite subsequence I of \(\mathbb {N}\) such that for all \(i \in I\), \(w(\tau [0;i]) < - i \cdot \epsilon \). Thus, the energy of \(\tau \) drops unboundedly. For the opposite direction, due to the determinacy of mean-payoff games and Lem. 3, it suffices to show that for each positional player 1 strategy \(\sigma \), there exists a player 2 strategy \(\pi \) such that \(\tau = \texttt{play}_{\sigma , \pi }(G, q)\) has negative limit average weight. Let \(\sigma \) be a positional player 1 strategy and \(\pi \) a player 2 strategy that wins q in the 2-fair energy game. Consider \(\tau = \textbf{p}\cdot \hat{\tau }\), where \(\hat{\tau }\) is a tail of \(\tau \) consisting of infinitely often visited nodes and edges of \(\tau \). Since the energy of \(\hat{\tau }\) drops unboundedly, there exists a negative cycle \(\textbf{c}\) in \(\hat{\tau }\) that visits all nodes and (fair) edges of \(\hat{\tau }\). Let \(\pi _{\sigma }\) be a player 2 strategy that mimics \(\pi \) until \(\textbf{c}\) is seen, and then repeats \(\textbf{c}\). Then \(\rho = \texttt{play}_{\sigma , \pi _{\sigma }}(G, q)\) has a tail \(\textbf{c}^\omega \), and since \(w(\textbf{c})< 0\), we have \(\texttt{avg}(\rho ) < 0\). \(\square \)
Lemma 6
Player 2 has finite memory winning strategies in 2-fair energy games.
5.3 1-fair Energy Games
In this section, we prove that 1-fair energy games are determined and using that introduce a gadget to reduce 1-fair energy games to regular energy games.
The determinacy of 1-fair energy games does not follow from prior work on \(\omega \)-regular energy games [7] as the definition of \(\texttt{Win}_2\) there uses Eq. (6) instead of Eq. (4). We establish determinacy by showing that, as in energy games, one can restrict the quantification over \(c \in \mathbb {N}\) to a finite set (namely to \(c \in [0, nW]\)) in Eq. (6). That is, if there exists a player 2 strategy \(\pi \) that satisfies \(\forall \sigma \in \varSigma _1, \texttt{play}_{\sigma , \pi }(G, q) \not \in \texttt{En}^f_{nW}\), then there exists a winning player 2 strategy \(\pi ^{\texttt{ext}}\) (winning against all c) as the energy level of plays conforming to this strategy \(\pi ^{\texttt{ext}}\) drops unboundedly. It then follows from the discussion in Sec. 5.1 that 1-fair energy games are determined. The proof of Thm. 5 can be found in [8, App. D].
Theorem 5
1-fair energy games are determined.
Next we will show that the gadget in Fig. 4 turns 1-fair energy games into regular energy games. The difference of this gadget from Fig. 2a mostly lies in the different treatment of the zero-weight-cycles. We first discuss briefly why such cycles are important, and then introduce this gadget.
The importance of 0-cycles in 1-fair energy games. It is known that the winning regions of a player in energy games and mean-payoff games (with objective \(\texttt{MP}_0\)) coincide [16]. This is not true for the 1-fair variants of these games, as player 1 may need infinite memory to win in 1-fair mean-payoff games (see Sec. 3 and 4.1), but not in 1-fair energy games. However, the equivalence of winning regions still holds in fair games without 0-cycles. Intuitively, if there are no 0-cycles, for a winning player 1 (player 2) strategy \(\sigma \) (\(\pi \)) in the fair energy game, the energy of each play \(\tau \) that conforms with \(\sigma \) (\(\pi \)) grows (drops) unboundedly, which makes \(\tau \) also winning in the fair mean-payoff game. For instance, in a 1-fair energy game with a player 1 node with a single fair edge with 0 weight is winning for player 1; but if we add another fair edge to this node with weight \(-1\), it becomes losing for player 1. However, when we consider the graph under the mean-payoff objective, both nodes remain in \(\texttt{Win}_1\).
Fig. 4.
1-fair energy gadget where \(\epsilon = 1/(n+1)\)
Therefore, a 1-fair energy gadget should distinguish between two kinds of nodes, A and B, both of which achieve mean-payoff value 0 but node A (in \(\texttt{Win}_1\)) achieves value 0 due to a strategy that visits only 0-cycles while node B (in \(\texttt{Win}_2\)) achieves it due to an infinite memory strategy that sees a 0-cycle more and more often. The middle branch of the gadget in Fig. 4 serves this purpose. The gadget matches Fig. 2a on the leftmost (\(\texttt{br} _{\texttt {fair}}\)) and rightmost (\(\texttt{br} _{\texttt {esc}}\)) branches, which still serve as the escape branches for player 1 and player 2, as in Sec. 4.1. The middle branch, called the value branch\(\texttt{br}^{q}_{\texttt {val}}\) distinguishes nodes of type A and B. Intuitively, if both players do not have escape strategies from q, then the value branch is taken. If player 1 can visit a positive cycle from q, then she wins from q since intuitively she can take this cycle enough times before visiting its fair edges. In this case, she chooses the left successor \(q_\texttt {pos}\) of \(q_\texttt {val}\), which is called the positive value branch\(\texttt{br}^{q}_{\texttt {pos}}\) and visits the weight \(- \epsilon \). The game is won by player 1 despite the weight \(-\epsilon \), due to the positive cycle. On the other hand, if player 1 is winning from q but not by visiting a positive cycle, then she is winning as all the live edges lead to 0-cycles (Node A). In this case, player 1 takes the right successor \(q_\texttt {0}\) of \(q_\texttt {val}\), which is called the zero value branch\(\texttt{br}^{q}_{\texttt {0}}\), and wins. If neither of these cases holds for a node q (Node B), player 2 wins from both successors of the value branch.
Theorem 6
Let \((G, E_f, \texttt{MP}^f_0)\) be a 1-fair energy game where \(G = (Q, E, w)\), \(w : E \rightarrow [-W, W]\), and \(|Q|=n\). Then there exists an energy game \(G'= (Q',E',w')\) where \(Q' \supseteq Q\), \(|Q'|\le 8n\) and \(w' : E' \rightarrow [-W', W']\) with \(W' = (n^2W+n)(n+1)\) such that \(\texttt{Win}_i(G) = \texttt{Win}_i(G') \cap Q\) for \(i \in \{1, 2\}\).
We obtain the game \(G'\) in Thm. 6 by replacing each fair node in the 1-fair energy game G via the gadget in Fig. 4, as in Sec. 4.1. We note that the size of the game given in Thm. 6 is w.r.t. the equivalent energy game on integer weights, obtained by multiplying every weight in the game with \(1 / \epsilon = n+1\). The state-of-the-art algorithm for energy games [16] and Thm. 6 imply that 1-fair energy games can be solved in time \(O(n^4mw)\). Furthermore, the proof reveals that player 1 has finite memory strategies (a local memory of \(log(n^3W + n)\) each node) and player 2 has positional strategies.
Unlike fair mean-payoff games, the determinacy of 1-fair energy games does not follow from Thm. 6. Instead, the proof hinges on the determinacy result itself, as detailed in [8, App. D]. Below, we outline the key ideas.
Recall that in the first direction of the proof of Thm. 1, we derive a player 1 strategy \(\sigma \) in G from a positional winning strategy \(\sigma '\) in \(G'\), reasoning about the tails \(\hat{\tau }\) of plays \(\tau \in \texttt{plays}_{\sigma }(G)\). We use the fact that in a mean-payoff (and similarly, in an energy) game, all cycles in \(G'_{\sigma '}\) are non-negative. This gives us that the cycles \(\mathbf {c'}\) using only simulation branches in \(G'_{\sigma '}\) have projections \(\textbf{c} = \mathbf {c'}|_G\) with non-negative weight. In the 1-fair mean-payoff case, with infinite memory we let \(\sigma \) take these cycles increasingly often to ensure that the projection play \(\tau = \tau '|_Q\) has non-negative mean-payoff.
Now, in 1-fair energy games, the cycles \(\mathbf {c'}\) in \(G'_{\sigma '}\) that visit a positive-value branch have positive weight projections \(\textbf{c} = \mathbf {c'}|_Q\), due to the \(-\epsilon \) weights. We refer to the choice of the positive-value branch, \(\sigma '(q_{\texttt {pos}})\) as the ‘preferred successor’ of q that induces positive weight cycles in G. Thus, player 1 can adopt a strategy \(\sigma \) in G that repeatedly selects the preferred successors at fair nodes to accumulate sufficient positive weight before traversing the fair edges to satisfy fairness. As a result, the weight of every tail \(\hat{\tau }\) of all plays \(\tau \in \texttt{plays}_{\sigma }(G)\) is monotonically increasing, and bounded below by some \(-d\). However, unlike mean-payoff games, energy games require reasoning about prefixes of plays. Specifically, we need to ensure that the weight of every prefix of each play conforming to \(\sigma \) is bounded below by \(-c\) for some \(c \in \mathbb {N}\). This is challenging, as the prefix lengths are unbounded, making the determinacy result crucial.
As these games are determined, player 2 wins from a node q if and only if it has a winning strategy \(\pi \) that wins against all initial credits c and all player 1 strategies (Eq.(4)). Therefore, the weight of all plays in \(\texttt{plays}_\pi (G)\) drops unboundedly. Dually, a player 1 strategy \(\lambda \) is winning if all plays in \(\texttt{plays}_\lambda (G)\) are fair with weights bounded below (not necessarily by the same c). Then for all \(\tau = \textbf{u}\cdot \hat{\tau }\), the length of the finite prefix \(\textbf{u}\), together with the lower bound \(-d\) of the tail \(\hat{\tau }\) naturally yields a lower bound of \(-d -W\cdot |\textbf{u}|\) for the weight of \(\tau \).
The proof of the second direction is similar to the case of 1-fair mean-payoff, where we construct a positional winning player 2 strategy \(\pi \) in G based on a positional winning strategy \(\pi '\) in \(G'\). This shows that memoryless strategies suffice for player 2. We give an alternative, simpler proof of this in [8, App. D].
Theorem 7
In 1-fair energy games, player 1 has finite memory and player 2 has memoryless winning strategies.
6 Conclusion
In this work, we study the complexity of solving mean-payoff and energy games under strong transition fairness assumptions. We show that when combined with quantitative goals, fairness comes for free in the sense that the complexity of solving these games do not become computationally expensive. We discussed the determinacy and strategy complexity of these games and provided gadget-based techniques to solve them.
A possible future direction is to study the complexity of solving the doubly fair counterpart of these games, where both players are restricted by fairness constraints on their moves, similar to the extension of fair \(\omega \)-regular games in [35].
In the \(\omega \)-regular setting, a slight extension of strong transition fairness called group fairness is sufficient to make the problem \({\textsf{NP}}\)-hard, even when combined with the reachability objective [47]. Group fairness is defined via tuples \((G_1, E_1), \ldots ,(G_k, E_k)\) where for each \(i \in [1, k]\), \(G_i\) is a subset of player 2 nodes, and \(E_i\) is a subset of edges such that the source node of each edge \(e \in E_i\) belongs to \(G_i\). A play \(\tau \) is called group fair if, for each \(v \in V\) and \(i \in [1, k]\), whenever \(v \in \texttt{Inf}(\tau ) \cap G_i\), there exists an \(e \in E_i\) that is taken infinitely often in \(\tau \).
In a group fair game with an \(\omega \)-regular objective \(\varphi \) and tuples \((G_1, E_1), \ldots \)\(, (G_k, E_k)\) defining the group fairness, player 1 wins a play \(\tau \) if \(\tau \) satisfies \(\varphi \) or is not group fair. Being a subclass of Streett fairness (or, strong fairness), group fairness already unravels the full complexity of Streett fairness2. Since reachability can be expressed as a mean-payoff/energy objective, this \({\textsf{NP}}\)-hardness result carries over to 2-group-fair3 mean-payoff games, making these games \({\textsf{NP}}\)-complete. 2-group-fair energy games again suffer from a lack of determinacy, since they subsume 2-fair energy games. Similarly, as the dual of reachability, the safety objective can be expressed as a mean-payoff/energy objective. This allows us to derive a \({\textsf{coNP}}\) lower bound for 1-group-fair4 mean-payoff and 1-group-fair energy games, making these games \({\textsf{coNP}}\)-complete. However, the exploration of more general notions of fairness – such as other subclasses of Streett fairness – that could provide better complexity bounds or lead to elegant solution algorithms for qualitative or quantitative games remains a significant open area of research.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Note that in a game where fairness is inflicted on player 2 (as in the group fairness definition), the fairness condition is a subclass of Rabin objective rather than Streett. Thus, the derived complexity lower bound is \({\textsf{NP}}\) rather than \({\textsf{coNP}}\).
By this, we indicate a game with group fairness where all \(G_i\) are player 1 nodes. player 1 wins a play \(\tau \) of a 1-group-fair game with objective \(\varphi \) if \(\tau \) satisfies \(\varphi \) and is group fair.
