pith. sign in

arxiv: 1907.06913 · v2 · pith:26SNYJHRnew · submitted 2019-07-16 · 💻 cs.GT

Partial Solvers for Generalized Parity Games

V\'eronique Bruy\`ere , Guillermo A. P\'erez , Jean-Fran\c{c}ois Raskin , Cl\'ement Tamines This is my paper

Pith reviewed 2026-05-24 20:40 UTC · model grok-4.3

classification 💻 cs.GT
keywords parity gamespartial solversZielonka algorithmgeneralized parity gamescontroller synthesisLTL synthesisgame solving algorithmsbenchmark evaluation
0
0 comments X

The pith

Partial solvers combined with Zielonka's algorithm solve most parity games from benchmark suites and extend to generalized parity games.

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

The paper establishes that incomplete but fast partial solvers for parity games can be paired with Zielonka's complete recursive algorithm to resolve the large majority of instances drawn from public benchmark collections used in controller synthesis and verification. It further shows that the partial-solver technique itself can be lifted to generalized parity games whose winning condition is the conjunction of several parity objectives. If these combinations work in practice, synthesis and verification tools gain an efficient route to deciding most games without always invoking full exponential-time procedures on every input.

Core claim

Partial solvers that run in polynomial time yet leave some games unsolved can be integrated with Zielonka's recursive algorithm to produce practical solvers that handle most games in publicly available benchmark suites; the same partial-solver construction extends directly to generalized parity games whose objective is the conjunction of multiple parity conditions.

What carries the argument

The integration of polynomial-time partial solvers with Zielonka's recursive decomposition, lifted to conjunctions of parity objectives.

If this is right

  • Most games appearing in LTL synthesis competition benchmarks become solvable by the hybrid partial-plus-Zielonka procedure.
  • Generalized parity games with multiple parity conditions become amenable to the same practical solving strategy.
  • The overall running time on solvable instances remains polynomial in the size of the partial-solver component.
  • Synthesis tools can therefore default to the hybrid method before falling back to slower complete algorithms.

Where Pith is reading between the lines

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

  • Verification engineers could embed the partial solvers as a fast first pass in existing toolchains to clear the common cases quickly.
  • The same hybrid pattern may apply to other classes of games whose partial solvers already exist but have not yet been paired with complete recursive procedures.
  • New benchmark suites constructed from actual hardware or software controllers would provide a direct test of whether the reported coverage holds outside competition instances.

Load-bearing premise

The benchmark instances drawn from the LTL synthesis competition are representative of the parity games that actually arise in controller synthesis and verification practice.

What would settle it

A set of controller-synthesis instances drawn from industrial or verification practice on which the hybrid solver leaves a large fraction unsolved while a complete solver finishes them all would refute the practical-utility claim.

Figures

Figures reproduced from arXiv: 1907.06913 by Cl\'ement Tamines, Guillermo A. P\'erez, Jean-Fran\c{c}ois Raskin, V\'eronique Bruy\`ere.

Figure 1
Figure 1. Figure 1: The partial solutions Z0, Z1, X before a recursive call to Algorithm 1. 3. by Algorithm Zielonka, the solutions computed on G are thus correct, such that X is part of the solution for some player i0, 4. by Theorem 3, as X is an attractor for player i0, V \ X is a i0-trap in G. We can thus define strategies σi , i ∈ {0, 1}, in the whole game G that are built (in the expected way) from the winning strategies… view at source ↗
Figure 2
Figure 2. Figure 2: Partial order  Second, functions upℓ and downℓ, with ℓ ∈ {1, . . . , k}, are defined exactly as previous functions up and down (see Definition 12), for each dimension ℓ and with respect to priority function αℓ. Third, we adapt (as expected) 12 [PITH_FULL_IMAGE:figures/full_fig_p012_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Layered structure of attractors with U8 ⊆ U6 ⊆ U4 = U and B8 ⊆ B6 ⊆ B4 = LayAttr0 (G, α, P≥q, U) We derive from this proposition a polynomial time algorithm similar to Algorithm 4 where LayEpi (G, α, P≥q) is used instead of GoodEpi (G, α) and P is an input list composed of all possible sets P≥q, with q ∈ [d]. This algorithm considers different sets P≥q until finding one composed of i-priorities and such th… view at source ↗
read the original abstract

Parity games have been broadly studied in recent years for their applications to controller synthesis and verification. In practice, partial solvers for parity games that execute in polynomial time, while incomplete, can solve most games in publicly available benchmark suites. In this paper, we combine those partial solvers with the classical recursive algorithm for parity games due to Zielonka. We also extend partial solvers to generalized parity games that are games with conjunction of parity objectives. We have implemented those algorithms and evaluated them on a large set of benchmarks proposed in the last LTL synthesis competition.

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

2 major / 2 minor

Summary. The paper claims that combining existing polynomial-time partial solvers for parity games with Zielonka's recursive algorithm solves most instances from publicly available benchmark suites, and that the partial solvers can be extended in a straightforward way to generalized parity games whose objectives are conjunctions of parity conditions. The combined and extended algorithms are implemented and evaluated on the benchmark set from the most recent LTL synthesis competition.

Significance. If the empirical results hold, the work supplies a practical, readily implementable route to solving the parity games that arise in controller synthesis and verification. The combination exploits the speed of incomplete partial solvers while retaining completeness via Zielonka's algorithm; the extension to conjunctions of parity objectives widens applicability without requiring an entirely new solver. The use of public benchmarks and the provision of an implementation are positive features that support reproducibility.

major comments (2)
  1. [Evaluation] The central empirical claim (that the partial-solver + Zielonka combination solves most benchmark instances) is load-bearing for the paper's contribution, yet the abstract supplies no quantitative success rates, run-time distributions, or comparison against standalone Zielonka. The evaluation section must therefore contain a clear table or figure reporting, for each benchmark family, the fraction of instances solved, the number of instances on which the partial solver alone succeeded, and the overhead of the combined procedure.
  2. [Generalized parity games] The extension of partial solvers to generalized parity games (conjunctions of parity objectives) is presented as straightforward, but the manuscript must explicitly argue that the soundness and polynomial-time guarantees of the original partial solvers are preserved under the conjunction; otherwise the claim that the same approach extends cannot be assessed.
minor comments (2)
  1. The abstract should name the concrete partial solvers that are combined with Zielonka and extended to the generalized setting.
  2. Pseudocode or a high-level description of the integration point between a partial solver and Zielonka's recursion would improve clarity.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the positive assessment and the constructive suggestions for improving the clarity of our empirical claims and theoretical arguments. We address each major comment below.

read point-by-point responses

  1. Referee: [Evaluation] The central empirical claim (that the partial-solver + Zielonka combination solves most benchmark instances) is load-bearing for the paper's contribution, yet the abstract supplies no quantitative success rates, run-time distributions, or comparison against standalone Zielonka. The evaluation section must therefore contain a clear table or figure reporting, for each benchmark family, the fraction of instances solved, the number of instances on which the partial solver alone succeeded, and the overhead of the combined procedure.

    Authors: We agree that a more explicit tabular summary would strengthen the presentation. In the revised manuscript we will add a table (or figure) in the evaluation section that, for each benchmark family from the LTL synthesis competition, reports: (i) the fraction of instances solved by the combined partial-solver + Zielonka procedure, (ii) the number of instances solved by the partial solver alone, and (iii) the runtime overhead incurred by invoking Zielonka on the residual instances. We will also include a direct comparison against standalone Zielonka on the same families. revision: yes

  2. Referee: [Generalized parity games] The extension of partial solvers to generalized parity games (conjunctions of parity objectives) is presented as straightforward, but the manuscript must explicitly argue that the soundness and polynomial-time guarantees of the original partial solvers are preserved under the conjunction; otherwise the claim that the same approach extends cannot be assessed.

    Authors: We will add an explicit argument (in a new subsection or dedicated paragraph) showing that both soundness and polynomial-time complexity are preserved. The extension works by lifting the partial-solver invariants to the product game whose priorities encode the conjunction; because the original partial solvers rely only on local attractor computations and priority-order comparisons that remain well-defined under this product construction, the same polynomial-time bounds and soundness proofs carry over directly. revision: yes

Circularity Check

0 steps flagged

No significant circularity; algorithmic construction and empirical evaluation are self-contained

full rationale

The paper presents algorithmic constructions (partial solvers combined with Zielonka recursion, plus direct extension to conjunctions of parity objectives) and reports their performance on externally defined benchmark suites from the LTL synthesis competition. No equations, fitted parameters, or predictions appear that reduce to the inputs by construction. Zielonka's algorithm is a standard external reference, not a self-citation chain. The evaluation claim is directly testable on the stated suites without internal preconditions that collapse the result to a renaming or fit. This is the normal case of an algorithmic paper whose central claims remain independently verifiable.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper is an algorithmic contribution resting on standard definitions of parity games and Zielonka's algorithm; no free parameters, new entities, or ad-hoc axioms are introduced in the abstract.

axioms (1)
  • standard math Parity games are two-player turn-based games on finite graphs with integer priorities where the winner is decided by the parity of the highest priority appearing infinitely often.
    Standard definition invoked when describing the problem domain.

pith-pipeline@v0.9.0 · 5628 in / 1090 out tokens · 17700 ms · 2026-05-24T20:40:31.722104+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

19 extracted references · 19 canonical work pages · 1 internal anchor

  1. [1]

    Ah-Fat and M

    P . Ah-Fat and M. Huth. Partial solvers for parity games: Effective polynomial-time composition. In GandALF Proceedings, volume 226 of EPTCS, pages 1–15, 2016

    work page 2016

  2. [2]

    Bloem, K

    R. Bloem, K. Chatterjee, K. Greimel, T. A. Henzinger, and B . Jobstmann. Robustness in the presence of liveness. In CA V Proceedings, volume 6174 of Lecture Notes in Computer Science , pages 410–424. Springer, 2010

    work page 2010

  3. [3]

    C. S. Calude, S. Jain, B. Khoussainov, W. Li, and F. Stephan . Deciding parity games in quasipolynomial time. In STOC Proceedings, pages 252–263. ACM, 2017

    work page 2017

  4. [4]

    Chatterjee, W

    K. Chatterjee, W. Dvor´ ak, M. Henzinger, and V . Loitzenba uer. Conditionally optimal algorithms for generalized B¨ u chi games. In MFCS Proceedings, volume 58 of LIPIcs, pages 25:1–25:15. Schloss Dagstuhl - Leibniz-Zentrum fue r Infor- matik, 2016

    work page 2016

  5. [5]

    Chatterjee and M

    K. Chatterjee and M. Henzinger. Efficient and dynamic algo rithms for alternating b¨ uchi games and maximal end- component decomposition. J. ACM, 61(3):15:1–15:40, 2014

    work page 2014

  6. [6]

    Chatterjee, T

    K. Chatterjee, T. A. Henzinger, and N. Piterman. Generali zed parity games. In FOSSACS Proceedings, volume 4423 of Lecture Notes in Computer Science , pages 153–167. Springer, 2007

    work page 2007

  7. [7]

    Doyen and J

    L. Doyen and J. Raskin. Antichain algorithms for finite aut omata. In TACAS Proceedings, volume 6015 of Lecture Notes in Computer Science, pages 2–22. Springer, 2010

    work page 2010

  8. [8]

    E. A. Emerson and C. S. Jutla. Tree automata, mu-calculus a nd determinacy (extended abstract). In FOCS Proceedings, pages 368–377. IEEE Computer Society, 1991

    work page 1991

  9. [9]

    Filiot, N

    E. Filiot, N. Jin, and J. Raskin. Exploiting structure in L TL synthesis. STTT, 15(5-6):541–561, 2013

    work page 2013

  10. [10]

    Friedmann and M

    O. Friedmann and M. Lange. Solving parity games in practi ce. In ATVA Proceedings, volume 5799 of Lecture Notes in Computer Science, pages 182–196. Springer, 2009

    work page 2009

  11. [11]

    Gr¨ adel, W

    E. Gr¨ adel, W. Thomas, and T. Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Rese arch [outcome of a Dagstuhl seminar , February 2001], volume 2500 of Lecture Notes in Computer Science . Springer, 2002

    work page 2001

  12. [12]

    M. Huth, J. H. Kuo, and N. Piterman. Fatal attractors in pa rity games. In FOSSACS Proceedings, volume 7794 of Lecture Notes in Computer Science , pages 34–49. Springer, 2013

    work page 2013

  13. [13]

    M. Huth, J. H. Kuo, and N. Piterman. Static analysis of par ity games: Alternating reachability under parity. In Semantics, Logics, and Calculi - Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays, volume 9560 of Lecture Notes in Computer Science , pages 159–177. Springer, 2016

    work page 2016

  14. [14]

    The 5th Reactive Synthesis Competition (SYNTCOMP 2018): Benchmarks, Participants & Results

    S. Jacobs, R. Bloem, M. Colange, P . Faymonville, B. Finkb einer, A. Khalimov, F. Klein, M. Luttenberger, P . J. Meyer, T. Michaud, M. Sakr, S. Sickert, L. Tentrup, and A. Walker. Th e 5th reactive synthesis competition (SYNTCOMP 2018): Benchmarks, participants & results. CoRR, abs/1904.07736, 2019

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  15. [15]

    Jurdzinski

    M. Jurdzinski. Deciding the winner in parity games is in U P ∩ co-UP. Inf. Process. Lett., 68(3):119–124, 1998

    work page 1998

  16. [16]

    D. A. Martin. Borel determinacy. Annals of Mathematics, 102:363–371, 1975

    work page 1975

  17. [17]

    Pnueli and R

    A. Pnueli and R. Rosner. On the synthesis of a reactive mod ule. In POPL Proceedings, pages 179–190. ACM Press, 1989

    work page 1989

  18. [18]

    van Dijk

    T. van Dijk. Oink: An implementation and evaluation of mo dern parity game solvers. In TACAS Proceedings, Part I , volume 10805 of Lecture Notes in Computer Science , pages 291–308. Springer, 2018

    work page 2018

  19. [19]

    Zielonka

    W. Zielonka. Infinite games on finitely coloured graphs wi th applications to automata on infinite trees. Theor . Comput. Sci., 200(1-2):135–183, 1998. 18

    work page 1998