pith. sign in

arxiv: 1907.06264 · v1 · pith:J7ELNEZ4new · submitted 2019-07-14 · 💻 cs.LO · cs.FL· cs.GT

Solving Mean-Payoff Games via Quasi Dominions

Massimo Benerecetti , Daniele Dell'Erba , Fabio Mogavero This is my paper

Pith reviewed 2026-05-24 21:30 UTC · model grok-4.3

classification 💻 cs.LO cs.FLcs.GT
keywords mean-payoff gamesquasi dominionssmall progress measuresparity gamesgame solvingalgorithmcomplexity
0
0 comments X

The pith

Merging small progress measures with quasi dominions yields an algorithm for mean-payoff games that converges much faster in practice while preserving the prior worst-case complexity bound.

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

The paper establishes a new algorithm for solving mean-payoff games that integrates small progress measures with quasi dominions, two ideas first developed for parity games. The combination accelerates practical convergence to the correct values without altering the theoretical complexity guarantee of the underlying progress-measure procedure. Experiments on standard benchmarks show the resulting solver runs orders of magnitude faster than the asymptotically optimal algorithm previously known. Readers who solve verification or synthesis problems modeled as mean-payoff games would therefore obtain usable solutions on larger instances.

Core claim

The integration of quasi dominions into the small-progress-measure procedure for mean-payoff games produces an algorithm whose practical running time improves by orders of magnitude over the best prior method while the worst-case complexity bound remains unchanged.

What carries the argument

Quasi-dominion-augmented small progress measures, which use dominion detection to prune value iterations during the computation of mean payoffs.

If this is right

  • The algorithm solves concrete mean-payoff instances orders of magnitude faster than the previous best method.
  • The same worst-case complexity bound as the underlying progress-measure procedure is retained.
  • The technique supplies a practical replacement for existing mean-payoff solvers in verification pipelines.

Where Pith is reading between the lines

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

  • The same integration pattern could be tried on other payoff objectives whose solution algorithms already rely on progress measures.
  • Implementation inside existing model checkers would immediately enlarge the set of verifiable systems.
  • Tighter bounds on the number of dominion detections might yield further practical speed-ups.

Load-bearing premise

That the addition of quasi-dominion detection inside the progress-measure loop does not increase the number of iterations needed in the worst case.

What would settle it

A family of mean-payoff game instances on which the new procedure requires asymptotically more iterations than the original small-progress-measure algorithm.

Figures

Figures reproduced from arXiv: 1907.06264 by Daniele Dell'Erba, Fabio Mogavero, Massimo Benerecetti.

Figure 1
Figure 1. Figure 1: An MPG. Let us consider the simple example game depicted in [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Another MPG. Consider, for instance, the example in [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Yet another MPG. We now exemplify the lack of monotonicity of the progress operator prg+. To do so, consider the game of [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: A simulation. the only escape position is f, which is lifted to measure k + 1. The resulting weak quasi dominion {c, d, g}, however, is closed, since µ̺ (c) = 2 < µ̺ (d) + c = 3. Therefore, player ⊕ changes strategy and chooses the move (c, d). Since no escape positions remain, the set {c, d, g} is winning for player ⊕ and the win operator lifts all their measures to ∞, leading to ̺ in Picture (5). The … view at source ↗
Figure 5
Figure 5. Figure 5: Experiments on random games with 5000 positions. In order to assess the effectiveness of the pro￾posed approach, we implemented both QDPM and SEPM [13], the most efficient known solution to the problem and the more closely related one to QDPM, in C++ within OINK [32]. OINK has been developed as a framework to compare parity game solvers. However, extending the framework to deal with MPGs is not difficult. … view at source ↗
Figure 6
Figure 6. Figure 6: Total solution times in seconds of SEPM and QDPM on [PITH_FULL_IMAGE:figures/full_fig_p014_6.png] view at source ↗
read the original abstract

We propose a novel algorithm for the solution of mean-payoff games that merges together two seemingly unrelated concepts introduced in the context of parity games, small progress measures and quasi dominions. We show that the integration of the two notions can be highly beneficial and significantly speeds up convergence to the problem solution. Experiments show that the resulting algorithm performs orders of magnitude better than the asymptotically-best solution algorithm currently known, without sacrificing on the worst-case complexity.

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 / 2 minor

Summary. The paper proposes a novel algorithm for mean-payoff games that integrates small progress measures and quasi dominions (originally from parity games). It claims that this merger accelerates convergence to the solution while preserving the worst-case complexity of the underlying progress-measure procedure, and that experiments demonstrate orders-of-magnitude practical speedups over the asymptotically best known algorithm.

Significance. If the integration and complexity preservation hold, the work would represent a notable practical advance for mean-payoff games, which arise in verification and synthesis. The explicit preservation of worst-case complexity alongside empirical gains, together with the cross-game transfer of quasi-dominion techniques, would be a clear strength.

minor comments (2)
  1. [Abstract / Introduction] The abstract asserts complexity preservation but does not name the precise bound (e.g., the original progress-measure complexity); a one-sentence reminder in the introduction would help readers locate the claim.
  2. [Experimental section] Figure captions and table headers should explicitly state the benchmark suite size and timeout used for the reported speedups, to allow direct comparison with prior work.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of our work and the recommendation for minor revision. The recognition that the integration of small progress measures with quasi dominions preserves worst-case complexity while delivering substantial practical improvements is appreciated.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper presents a direct algorithmic construction that integrates small progress measures and quasi dominions from parity games into the mean-payoff setting. The abstract explicitly states that the integration preserves the original worst-case complexity bound while improving practical performance. No equations, definitions, or claims in the provided text reduce a result to a fitted parameter, self-citation chain, or renamed input by construction. The derivation is self-contained against external benchmarks and does not rely on load-bearing self-references or ansatzes smuggled via citation.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the standard definitions of mean-payoff games together with the established notions of small progress measures and quasi dominions; no new free parameters or invented entities are introduced in the abstract.

axioms (1)
  • domain assumption Mean-payoff games and the auxiliary notions of small progress measures and quasi dominions are well-defined and correctly transferred from parity games.
    The algorithm is built directly on these prior definitions.

pith-pipeline@v0.9.0 · 5596 in / 1060 out tokens · 21296 ms · 2026-05-24T21:30:05.954246+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

34 extracted references · 34 canonical work pages

  1. [1]

    PRIMES is in P

    M. Agrawal, N. Kayal, and N. Saxena, “PRIMES is in P .” AM, vol. 160, no. 2, pp. 781–793, 2004

    work page 2004

  2. [2]

    Combinato rial Simplex Algorithms Can Solve Mean-Payoff Games

    X. Allamigeon, P . Benchimol, and S. Gaubert, “Combinato rial Simplex Algorithms Can Solve Mean-Payoff Games.” SIAM, vol. 24, no. 4, pp. 2096–2117, 2014

    work page 2096

  3. [3]

    The Tropical Shadow-V ertex Algorithm Solves Mean- Payoff Games in Polynomial Time on Average

    ——, “The Tropical Shadow-V ertex Algorithm Solves Mean- Payoff Games in Polynomial Time on Average.” in ICALP’14, 2014, pp. 89–100

    work page 2014

  4. [4]

    Tropicalizing the Simplex Algorithm

    X. Allamigeon, P . Benchimol, S. Gaubert, and M. Joswig, “ Tropicalizing the Simplex Algorithm.” SIAM, vol. 29, no. 2, pp. 751–795, 2015

    work page 2015

  5. [5]

    Solving Parity Games via Priority Promotion

    M. Benerecetti, D. Dell’Erba, and F. Mogavero, “Solving Parity Games via Priority Promotion.” in CA V’16, ser. LNCS 9780 (Part II). Springer, 2016, pp. 270–290

    work page 2016

  6. [6]

    A Combinatorial Strongly Subexponential Strategy Improvement Algorithm for Mean-Payoff Games

    H. Bj¨ orklund, S. Sandberg, and S. V orobyov, “A Combinatorial Strongly Subexponential Strategy Improvement Algorithm for Mean-Payoff Games.” in MFCS’04, 2004, pp. 673–685

    work page 2004

  7. [7]

    A Combinatorial Strongl y Subexponential Strategy Improvement Algorithm for Mean-Payoff Games

    H. Bj¨ orklund and S. V orobyov, “A Combinatorial Strongl y Subexponential Strategy Improvement Algorithm for Mean-Payoff Games.” DAM, vol. 155, no. 2, pp. 210–229, 2007

    work page 2007

  8. [8]

    Synth esis from LTL Specifications with Mean-Payoff Objectives

    A. Bohy, V . Bruy` ere, E. Filiot, and J.-F. Raskin, “Synth esis from LTL Specifications with Mean-Payoff Objectives.” in TACAS’13, 2013, pp. 169–184

    work page 2013

  9. [9]

    Temporal Specifications with Accumulative V alues

    U. Boker, K. Chatterjee, T. Henzinger, and O. Kupferman, “Temporal Specifications with Accumulative V alues.” in LICS’11, 2011, pp. 43–52

    work page 2011

  10. [10]

    Sur le Th´ eor` eme de Zorn

    N. Bourbaki, “Sur le Th´ eor` eme de Zorn.” AM, vol. 2, no. 6, pp. 434–437, 1949

    work page 1949

  11. [11]

    Infinite Runs in Weighted Timed Automata with Energy Constraints

    P . Bouyer, U. Fahrenberg, K. Larsen, N. Markey, and J. Sr ba, “Infinite Runs in Weighted Timed Automata with Energy Constraints.” in FORMATS’2008. Springer, 2008, pp. 33–47

    work page 2008

  12. [12]

    Using Strategy Improvement t o Stay Alive

    L. Brim and J. Chaloupka, “Using Strategy Improvement t o Stay Alive.” IJFCS, vol. 23, no. 3, pp. 585–608, 2012

    work page 2012

  13. [13]

    Faster Algorithms for Mean-Payoff Games

    L. Brim, J. Chaloupka, L. Doyen, R. Gentilini, and J.-F. Raskin, “Faster Algorithms for Mean-Payoff Games.” FMSD, vol. 38, no. 2, pp. 97–118, 2011

    work page 2011

  14. [14]

    Better Quality in Synthesis Through Quantitative Objectives

    R. B. K. Chatterjee, T. Henzinger, and B. Jobstmannand, “Better Quality in Synthesis Through Quantitative Objectives.” in CA V’09, 2009, pp. 140–156

    work page 2009

  15. [15]

    Hyper Temporal Net works - A Tractable Generalization of Simple Temporal Networks and its Relation to Mean-Payoff Games

    C. Comin, R. Posenato, and R. Rizzi, “Hyper Temporal Net works - A Tractable Generalization of Simple Temporal Networks and its Relation to Mean-Payoff Games.” Constraints, vol. 22, no. 2, 2017

    work page 2017

  16. [16]

    Dynamic Consistency of Conditio nal Simple Temporal Networks via Mean-Payoff Games: A Singly-Exponential Time DC-checking

    C. Comin and R. Rizzi, “Dynamic Consistency of Conditio nal Simple Temporal Networks via Mean-Payoff Games: A Singly-Exponential Time DC-checking.” in TIME’15. IEEECS, 2015, pp. 19–28

    work page 2015

  17. [17]

    Improved Pseudo-Polynomial Bound for the V alue Pr oblem and Optimal Strategy Synthesis in Mean- Payoff Games

    ——, “Improved Pseudo-Polynomial Bound for the V alue Pr oblem and Optimal Strategy Synthesis in Mean- Payoff Games.” Algorithmica, vol. 77, no. 4, 2017

    work page 2017

  18. [18]

    The Complexity of Stochastic Games

    A. Condon, “The Complexity of Stochastic Games.” IC, vol. 96, no. 2, pp. 203–224, 1992

    work page 1992

  19. [19]

    How to Solve Large Scale Dete rministic Games with Mean Payoff by Policy Iteration

    V . Dhingra and S. Gaubert, “How to Solve Large Scale Dete rministic Games with Mean Payoff by Policy Iteration.” in VALUETOOLS’06. ACM, 2006, p. 12

    work page 2006

  20. [20]

    Positional Strategi es for Mean Payoff Games

    A. Ehrenfeucht and J. Mycielski, “Positional Strategi es for Mean Payoff Games.” IJGT, vol. 8, no. 2, 1979

    work page 1979

  21. [21]

    An Ordered Approach to Solving Parity Games in Quasi Polynomial Time and Quasi Linear Space

    J. Fearnley, S. Jain, S. Schewe, F. Stephan, and D. Wojtc zak, “An Ordered Approach to Solving Parity Games in Quasi Polynomial Time and Quasi Linear Space.” in SPIN’17. ACM, 2017, pp. 112–121

    work page 2017

  22. [22]

    Self-Witnessing Polynomia l-Time Complexity and Prime Factorization

    M. Fellows and N. Koblitz, “Self-Witnessing Polynomia l-Time Complexity and Prime Factorization.” in CSCT’92. IEEECS, 1992, pp. 107–110

    work page 1992

  23. [23]

    Solving Parity Games in Prac tice

    O. Friedmann and M. Lange, “Solving Parity Games in Prac tice.” in ATVA’09, ser. LNCS 5799. Springer, 2009, pp. 182–196

    work page 2009

  24. [24]

    Cyclic Game s and an Algorithm to Find Minimax Cycle Means in Directed Graphs

    V . Gurvich, A. Karzanov, and L. Khachivan, “Cyclic Game s and an Algorithm to Find Minimax Cycle Means in Directed Graphs.” USSRCMMP, vol. 28, no. 5, pp. 85–91, 1988

    work page 1988

  25. [25]

    Deciding the Winner in Parity Games is in UP ∩ co-UP

    M. Jurdzi´ nski, “Deciding the Winner in Parity Games is in UP ∩ co-UP .”IPL, vol. 68, no. 3, pp. 119–124, 1998

    work page 1998

  26. [26]

    Small Progress Measures for Solving Parity Games

    ——, “Small Progress Measures for Solving Parity Games. ” in STACS’00, ser. LNCS 1770. Springer, 2000, pp. 290–301

    work page 2000

  27. [27]

    Succinct Progress Measur es for Solving Parity Games

    M. Jurdzi´ nski and R. Lazic, “Succinct Progress Measur es for Solving Parity Games.” in LICS’17. ACM, 2017, pp. 1–9

    work page 2017

  28. [28]

    Progress Measures for Complementation o f omega-Automata with Applications to Temporal Logic

    N. Klarlund, “Progress Measures for Complementation o f omega-Automata with Applications to Temporal Logic.” in FOCS’91. IEEECS, 1991, pp. 358–367

    work page 1991

  29. [29]

    Potential theory for mean pa yoff games

    Y . Lifshits and D. Pavlov, “Potential theory for mean pa yoff games.” JMS, vol. 145, no. 3, pp. 4967–4974, 2007

    work page 2007

  30. [30]

    Mean-Cost Cyclical Games

    N. Pisaruk, “Mean-Cost Cyclical Games.” MOR, vol. 24, no. 4, pp. 817–828, 1999

    work page 1999

  31. [31]

    An Optimal Strategy Improvement Algorithm for Solving Parity and Payoff Games

    S. Schewe, “An Optimal Strategy Improvement Algorithm for Solving Parity and Payoff Games.” in CSL’08, ser. LNCS 5213. Springer, 2008, pp. 369–384

    work page 2008

  32. [32]

    Oink: an Implementation and Evaluation of Modern Parity Game Solvers

    T. van Dijk, “Oink: an Implementation and Evaluation of Modern Parity Game Solvers.” in TACAS’18, ser. LNCS 10805. Springer, 2018, pp. 291–308

    work page 2018

  33. [33]

    Beweisstudien zum Satz von M. Zorn

    E. Witt, “Beweisstudien zum Satz von M. Zorn.” MN, vol. 4, no. 1-6, pp. 434–438, 1950

    work page 1950

  34. [34]

    The Complexity of Mean Payoff Games on Graphs

    U. Zwick and M. Paterson, “The Complexity of Mean Payoff Games on Graphs.” TCS, vol. 158, no. 1-2, pp. 343–359, 1996. Appendix A. Proofs In this appendix, we collect some supplementary material, p roviding three further lemmas (Lemmas 4, 5, and 6), and the proofs of the theorems and lemmas introduced i n Sections 3 and 4. Theorem 1 (Progress Measure) . Le...

    work page 1996