pith. sign in

arxiv: 2310.13612 · v3 · submitted 2023-10-20 · 💻 cs.GT

Doubly Fair Parity Games

Daniel Hausmann , Nir Piterman , Irmak Sa\u{g}lam , Anne-Kathrin Schmuck This is my paper

Pith reviewed 2026-05-24 06:32 UTC · model grok-4.3

classification 💻 cs.GT
keywords fair gamesparity gamesdeterminacygame reductiontwo-player gamesomega-regular conditionssymbolic algorithms
0
0 comments X

The pith

Fair α/β games are determined, and fair parity/parity games reduce polynomially to ordinary parity games by a gadget construction.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper defines games on finite graphs where each player must select fair moves infinitely often whenever their source vertex is visited infinitely often. If one player meets this constraint and the other does not, the fair player wins; otherwise the outcome is decided by one of two given ω-regular conditions α and β. The authors prove all such fair α/β games are determined. When both conditions are parity conditions they supply a polynomial reduction to ordinary parity games that uses a gadget modeled on the known stochastic-parity reduction, and they also give a direct symbolic fixpoint algorithm. The work shows how the gadget reduction and the symbolic algorithm translate into each other and highlights shared structure with stochastic parity games and with games that constrain only one player.

Core claim

Fair α/β games are determined for any ω-regular α and β. Fair parity/parity games admit a polynomial reduction to standard parity games via a gadget construction that encodes the fairness constraints for both players; the same games are also solved by a direct symbolic fixpoint algorithm. The two solution methods are inter-translatable and expose the common algorithmic skeleton shared with stochastic parity games.

What carries the argument

A gadget construction, modeled on the stochastic-parity reduction, that augments the original graph so fairness constraints are encoded as ordinary parity conditions while preserving the winner.

If this is right

  • Existing parity-game solvers can be reused for fair parity/parity games after the polynomial gadget reduction.
  • The determinacy result extends immediately to any pair of ω-regular conditions α and β.
  • The direct symbolic algorithm provides an alternative route that avoids explicit graph transformation.
  • The translation between gadget and fixpoint methods applies to the one-sided fairness variant as well.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same gadget technique may extend to other ω-regular conditions beyond parity.
  • Implementation of the reduction on small benchmark graphs would allow direct verification that the winner is unchanged.
  • The shared structure with stochastic games suggests possible transfer of approximation or learning algorithms between the two settings.

Load-bearing premise

The gadget construction preserves the winner of the original fair parity game without adding or removing strategies for either player.

What would settle it

A concrete fair parity game instance whose winner differs from the winner of the game obtained after applying the described gadget reduction.

Figures

Figures reproduced from arXiv: 2310.13612 by Anne-Kathrin Schmuck, Daniel Hausmann, Irmak Sa\u{g}lam, Nir Piterman.

Figure 1
Figure 1. Figure 1: Deadlock caused by interacting fairness constraints of two robots facing [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: A simple fair game arena discussed in Ex. 1. [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Four fair parity/β games: dashed lines represent fair edges. Games G1 and G4 are won by ∃-player and G2 and G3 are won by ∀-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. 5 Reduction to Parit… view at source ↗
Figure 4
Figure 4. Figure 4: Gadgets for v ∈ V fair ∃ (top) and v ∈ V fair ∀ (bottom) in fair parity/⊥ games. If λ(v) is odd, then λ↓(v) = λ(v), otherwise, λ↓(v) = λ(v) − 1. The number n is always even. Nodes (v out, i) have priority i. We refer to the subgames in [PITH_FULL_IMAGE:figures/full_fig_p011_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Gadget for v ∈ V fair ∃ 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 ∃ and ∀ 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 … view at source ↗
Figure 6
Figure 6. Figure 6: Gadget for v ∈ V fair ∀ in fair parity/parity games; u abbreviates (v, p, b). and the current priority Γ(v) at v; in Ef (v, p, b), we require (v, w) ∈ Ef instead. In both functions, the argument b is used to explicitely set this component of the memory to either ∃ or ∀. The reduced game consists of subgames that start at annotated nodes u = (v, p, b) ∈ V × [d] × [1]. In case that v ∈ V n , the game just pr… view at source ↗
Figure 7
Figure 7. Figure 7: Existential gadgets that re￾place v ∈ V fair ∃ (left) and v ∈ V fair ∀ (right) in the fair B¨uchi/⊥ game. λ(v) 1 2 1 2 3 E(v) Ef (v) E(v) λ(v) 1 2 1 2 Ef (v) E(v) [PITH_FULL_IMAGE:figures/full_fig_p024_7.png] view at source ↗
Figure 9
Figure 9. Figure 9: Universal gadgets that replace v ∈ V fair ∃ (top) and v ∈ V fair ∀ (bottom) in a fair parity/⊥ game [PITH_FULL_IMAGE:figures/full_fig_p026_9.png] view at source ↗
read the original abstract

We consider two-player games over finite graphs in which both players are restricted by fairness constraints on their moves. Given a two player game graph $G=(V,E)$ and a set of fair moves $E_f\subseteq E$ a player is said to play "fair" in $G$ if they choose an edge $e \in E_f$ infinitely often whenever the source vertex of $e$ is visited infinitely often. Otherwise, they play "unfair". We equip such games with two $\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 where only one player is restricted by fair moves.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper introduces fair α/β games on finite directed graphs, where each player is subject to a fairness constraint (must take fair edges infinitely often from infinitely visited sources) and the winner is decided by α on mutually fair plays, by β on mutually unfair plays, and by the fair player in mixed cases. It proves determinacy for general fair α/β games. Specializing to fair parity/parity games, it supplies a polynomial reduction to ordinary parity games via a gadget construction modeled on the known stochastic-parity reduction, an independent symbolic fixpoint algorithm, and an explicit translation establishing equivalence of the two solution methods at the level of attractors and parity conditions.

Significance. If the claims hold, the work extends the algorithmic theory of parity games to the doubly fair setting while preserving polynomial-time solvability. The explicit equivalence between the gadget reduction and the fixpoint algorithm, together with the connection to both stochastic parity games and one-sided fair games, supplies a conceptual unification that is likely to be useful for future extensions.

minor comments (3)
  1. [Abstract] The abstract refers to 'Section on the reduction' without a number; replace with the actual section number once the manuscript is typeset.
  2. [Reduction section] The description of the gadget is high-level in the abstract; ensure the main text supplies a self-contained diagram or pseudocode for the gadget so that the preservation argument can be checked without external references.
  3. [Conceptual translation subsection] The translation between the gadget reduction and the fixpoint algorithm is described as 'illustrat[ing] the underlying similarities'; add a short table or diagram that directly maps the attractor sets and parity priorities of one method onto the other.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript, accurate summary of the contributions on fair α/β games, and recommendation to accept. We are pleased that the connections to stochastic parity games and one-sided fair games are viewed as providing useful conceptual unification.

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper proves determination of fair α/β games directly and reduces fair parity/parity games to ordinary parity games (known to be solvable in polynomial time) via an explicit gadget construction. The gadget is modeled on a cited external reduction for stochastic parity games rather than any author prior result. An independent symbolic fixpoint algorithm is supplied, with an explicit translation proving equivalence of the two solution methods at the level of attractors and parity conditions. No load-bearing step reduces by definition, by fitted parameter, or by self-citation chain to the paper's own inputs; the target parity games remain independently decidable.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on standard results about parity-game determinacy and the correctness of a gadget modeled on the stochastic-parity reduction; no free parameters or new entities are introduced.

axioms (2)
  • standard math Parity games are determined and solvable in polynomial time
    Target of the reduction; invoked implicitly when the reduction is claimed to solve the fair game.
  • domain assumption The gadget construction preserves winning regions exactly as in the stochastic-parity reduction
    The abstract states the reduction is 'inspired by' that construction; this assumption is load-bearing for the polynomial claim.

pith-pipeline@v0.9.0 · 5818 in / 1314 out tokens · 24003 ms · 2026-05-24T06:32:31.126030+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

25 extracted references · 25 canonical work pages

  1. [1]

    In: Baader, F., Voronkov, A

    Aminof, B., Ball, T., Kupferman, O.: Reasoning about systems with transition fair- ness. In: Baader, F., Voronkov, A. (eds.) Logic for Programming, Artificial Intel- ligence, and Reasoning, 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings. Lecture Notes in Computer Science, vol. 3452, pp. 194–208. Springer (200...

    work page doi:10.1007/978-3-540-32275- 2004

  2. [2]

    In: Beck, J.C., Buffet, O., Hoffmann, J., Karpas, E., Sohrabi, S

    Aminof, B., Giacomo, G.D., Rubin, S.: Stochastic fairness and language- theoretic fairness in planning in nondeterministic domains. In: Beck, J.C., Buffet, O., Hoffmann, J., Karpas, E., Sohrabi, S. (eds.) Proceedings of the Thirtieth International Conference on Automated Planning and Schedul- ing, Nancy, France, October 26-30, 2020. pp. 20–28. AAAI Press ...

    work page 2020

  3. [3]

    Baldan, P., K¨ onig, B., Mika-Michalski, C., Padoan, T.: Fixpoint games on continuous lattices. Proc. ACM Program. Lang. 3(POPL), 26:1–26:29 (2019). https://doi.org/10.1145/3290339, https://doi.org/10.1145/3290339

    work page doi:10.1145/3290339 2019

  4. [4]

    TheoretiCS 2 (2023)

    Banerjee, T., Majumdar, R., Mallik, K., Schmuck, A., Soudjani, S.: Fast symbolic algorithms for omega-regular games under strong transi- tion fairness. TheoretiCS 2 (2023). https://doi.org/10.46298/theoretics.23.4, https://doi.org/10.46298/theoretics.23.4

    work page doi:10.46298/theoretics.23.4 2023

  5. [5]

    B¨ uchi, J., Landweber, L.: Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc. 138, 295–311 (1969)

    work page 1969

  6. [6]

    Formal Methods Syst

    Chatterjee, K., de Alfaro, L., Faella, M., Majumdar, R., Raman, V.: Code aware resource management. Formal Methods Syst. Des. 42(2), 146–174 (2013). https://doi.org/10.1007/s10703-012-0170-4, https://doi.org/10.1007/s10703-012- 0170-4

    work page doi:10.1007/s10703-012-0170-4 2013

  7. [7]

    In: International Workshop on Computer Science Logic

    Chatterjee, K., Jurdzi´ nski, M., Henzinger, T.A.: Simple stochastic parity games. In: International Workshop on Computer Science Logic. pp. 100–113. Springer (2003)

    work page 2003

  8. [8]

    In: In Proceedings of the International Conference for Computer Science Logic (CSL)

    Chatterjee, K., Jurdzinski, M., Henzinger, T.: Simple stochastic parity games. In: In Proceedings of the International Conference for Computer Science Logic (CSL). pp. 100–113 (2003), http://chess.eecs.berkeley.edu/pubs/729.html

    work page 2003

  9. [9]

    Journal of Symbolic Logic 28(4) (1963)

    Church, A.: Application of recursive arithmetic to the problem of circuit synthesis. Journal of Symbolic Logic 28(4) (1963)

    work page 1963

  10. [10]

    D’Ippolito, N., Rodr´ ıguez, N., Sardi˜ na, S.: Fully observable non-deterministic plan- ning as assumption-based reactive synthesis. J. Artif. Intell. Res. 61, 593–621 (2018). https://doi.org/10.1613/jair.5562, https://doi.org/10.1613/jair.5562

    work page doi:10.1613/jair.5562 2018

  11. [11]

    Nonlinear Analysis: Hybrid Systems 51, 101430 (2024)

    Majumdar, R., Mallik, K., Schmuck, A.K., Soudjani, S.: Symbolic control for stochastic systems via finite parity games. Nonlinear Analysis: Hybrid Systems 51, 101430 (2024). https://doi.org/https://doi.org/10.1016/j.nahs.2023.101430

    work page doi:10.1016/j.nahs.2023.101430 2024

  12. [12]

    Annals of Mathematics 65, 363–371 (1975)

    Martin, D.: Borel determinacy. Annals of Mathematics 65, 363–371 (1975)

    work page 1975

  13. [13]

    In: Gr¨ adel, E., Thomas, W., Wilke, T

    Mazala, R.: Infinite games. In: Gr¨ adel, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games: A Guide to Current Research. Lecture Notes in Com- puter Science, vol. 2500, pp. 23–42. Springer (2001)

    work page 2001

  14. [14]

    Lecture Notes in Computer Science, vol

    Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: Explicit reactive synthesis strikes back! In: 30th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 10981, pp. 578–586. Springer (2018)

    work page 2018

  15. [15]

    Nilsson, P., Ozay, N., Liu, J.: Augmented finite transition systems as abstrac- tions for control synthesis. Discret. Event Dyn. Syst. 27(2), 301–340 (2017). https://doi.org/10.1007/s10626-017-0243-z, https://doi.org/10.1007/s10626-017- 0243-z 20 Hausmann, Piterman, Sa˘ glam, Schmuck

    work page doi:10.1007/s10626-017-0243-z 2017

  16. [16]

    In: Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation

    Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. In: Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation. p. 364–380. VMCAI’06, Springer-Verlag, Berlin, Heidelberg (2006)

    work page 2006

  17. [17]

    In: Proc

    Pnueli, A., Rosner, R.: A framework for the synthesis of reactive modules. In: Proc. Intl. Conf. on Concurrency: Concurrency 88. Lecture Notes in Computer Science, vol. 335, pp. 4–17 (1988)

    work page 1988

  18. [18]

    Rabin, M.: Decidability of second order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141, 1–35 (1969)

    work page 1969

  19. [19]

    In: 42th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Sci- ence (2023), (to appear)

    Sa˘ glam, I., Schmuck, A.K.: Solving odd-fair parity games. In: 42th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Sci- ence (2023), (to appear)

    work page 2023

  20. [20]

    In: 4th Int

    Schewe, S., Finkbeiner, B.: Bounded synthesis. In: 4th Int. Symp. on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 4218, pp. 245–259. Springer (2006)

    work page 2006

  21. [21]

    Systems & control letters 33(4), 265–274 (1998)

    Thistle, J.G., Malham´ e, R.: Control of ω-automata under state fairness assump- tions. Systems & control letters 33(4), 265–274 (1998)

    work page 1998

  22. [22]

    Handbook of Formal Language The- ory III, 389–455 (1997)

    Thomas, W.: Languages, automata, and logic. Handbook of Formal Language The- ory III, 389–455 (1997)

    work page 1997

  23. [23]

    Walukiewicz, I.: Monadic second-order logic on tree-like structures. Theor. Com- put. Sci. 275(1-2), 311–346 (2002). https://doi.org/10.1016/S0304-3975(01)00185- 2, https://doi.org/10.1016/S0304-3975(01)00185-2

    work page doi:10.1016/s0304-3975(01)00185- 2002

  24. [24]

    equivalent

    Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1-2), 135–183 (1998). https://doi.org/10.1016/S0304-3975(98)00009-7, https://doi.org/10.1016/S0304- 3975(98)00009-7 Fair ω-Regular Games 21 A Full Proofs for Section 3 In this section we show equivalences of the winning conditi...

    work page doi:10.1016/s0304-3975(98)00009-7 1998

  25. [25]

    full version

    Moreover, this is exactly the reason why in Fig. 4, we start the children of v from (v∀, λ↓(v)) instead of (v∀, 1). We can do the latter as well, but we prefer to have a slightly reduced version of the gadgets by ignoring unnecessary branches. The universal gadgets for fair parity/⊥ are given in Fig. 9 in their “full version” instead of the “reduced versi...

    work page