Pith. sign in

REVIEW 3 major objections 4 minor 16 references

Permissive Equilibria in Multiplayer Reachability Games

T0 review · 3 major / 4 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Deciding existence of permissive equilibria with bounded penalties in multiplayer reachability games is in PSPACE under unary bounds.

desk verdict Promising framework for permissive equilibria, but the central PSPACE claim rests on a compression lemma whose written bound is exponential, not polynomial. read the letter →

arxiv 2411.13296 v1 pith:P2WDYI42 submitted 2024-11-20 cs.GT

Aline Goeminne , Benjamin Monmege This is my paper · ORCID
classification cs.GT MSC 91A1891A2068Q25
keywords multiplayerreachabilitygamesmulti-strategiespermissiveequilibriapenaltiesNashequilibriumsubgame-perfectPSPACEsymbolictrees
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper asks whether a multiplayer game on a finite graph can be solved not by a single strategy per player but by a multi-strategy: a nonempty set of allowed moves at each decision point, with the property that every way of choosing one allowed move yields a Nash equilibrium or a subgame-perfect equilibrium. The authors prove that the question "does such a permissive equilibrium exist, with per-player main and retaliation penalties below given thresholds?" is decidable in PSPACE when the thresholds are written in unary, and that the same holds when a designated set of players must win in at least one or in every consistent play. This matters because permissiveness is a natural reliability requirement for synthesized strategies: if one prescribed action becomes unavailable, another allowed action keeps every consistent profile in equilibrium. The paper's contribution is a complexity-theoretic decidability result, plus a finite witness representation that makes the search possible.

What carries the argument

The load-bearing objects are multi-strategies, penalties, and symbolic trees. A multi-strategy assigns each player, at each history he owns, a nonempty set of allowed successors instead of a single one; a player's penalty is the largest sum of weights of the edges he blocks along any play consistent with the multi-strategy, with a main penalty for the equilibrium outcome and a retaliation penalty for plays that follow a deviation. A tree is good when it is resistant to internal deviations, meaning that at every branching point owned by a player either all allowed continuations win for him or all lose, and resistant to external deviations, meaning that if a player can move outside the tree to a successor from which he can win, then all continuations inside the tree from that point must also win for him. The compression step in Proposition 11 is the technical core: it shows that any good infinite tree or forest respecting the penalty caps contains a finite symbolic subtree whose unfolding keeps all resistance and penalty properties, with height bounded by a polynomial in the number of players and vertices and in the largest penalty threshold.

What would settle it

Construct a reachability game with unary penalty bounds where a permissive equilibrium exists but every witnessing good tree has a branch in which some penalty only stops increasing after more than the claimed polynomial number of steps, or where no symbolic tree of the claimed height satisfies all resistance and penalty conditions even though an infinite good tree does.

Watch

Extended reading notes

Core claim

The central claim, stated as Theorems 14 and 15, is that for multiplayer reachability games the constrained penalty problem is decidable in PSPACE when penalty bounds are encoded in unary: given upper thresholds on each player's main and retaliation penalties, one can decide whether a permissive Nash equilibrium (with no restriction on retaliation) or a permissive subgame-perfect equilibrium exists. The same PSPACE bound holds for the weakly winning variant, where at least one consistent profile lets a designated set of players reach their targets, and for the strongly winning variant, where every consistent profile does so. The proof works by characterizing permissive equilibria with good trees and good forests, infinite objects whose branches are all equilibrium outcomes, and then compressing every such infinite witness into a symbolic tree of height polynomial in the game size and the largest penalty bound. An alternating polynomial-time machine guesses this finite symbolic witness and verifies its conditions branch by branch; since alternating polynomial time equals PSPACE, decidability follows.

Load-bearing premise

The load-bearing premise is Proposition 11's claim that every good infinite tree satisfying the resistance conditions and the penalty caps can be compressed to a symbolic tree of polynomial height; if the branch-completion step ever requires a taller witness, the PSPACE algorithm would not terminate correctly on all instances.

Editorial extensions

If this is right

  • For any finite reachability game with unary penalty bounds, the existence of a permissive Nash or subgame-perfect equilibrium can be decided in polynomial space.
  • The same algorithms handle requirements that a distinguished set of players win in at least one consistent play or in every consistent play, with no change to the complexity bound.
  • Positive answers are witnessed by finite symbolic trees or forests, so a permissive equilibrium can be described by a finite object rather than by an infinite strategy profile.
  • The tree and forest characterization reduces equilibrium checking to local branch conditions, which is exactly what allows an alternating polynomial-time machine to verify a guessed witness in polynomial space.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Beyond the paper: the same symbolic-tree and forest template is a natural candidate for other objectives such as safety or Büchi, since only the leaf and lasso winning checks would change.
  • Beyond the paper: if the polynomial height bound is tight, binary encoding of penalty bounds should push the decision problems out of PSPACE; a matching lower bound would sharpen the complexity boundary.
  • Beyond the paper: the constructive nature of the witness compression suggests a practical search for permissive equilibria by looking for polynomial-height symbolic trees directly, rather than exploring the infinite game tree.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper studies permissive equilibria in multiplayer reachability games on finite graphs. A multi-strategy assigns to each history a non-empty set of actions rather than a single action, and a permissive Nash or subgame-perfect equilibrium is a profile of multi-strategies such that every fully specified strategy profile consistent with it is an NE or SPE, respectively. Permissiveness is measured by two penalty notions: a main penalty, which is the worst-case penalty over outcomes of the multi-strategy, and a retaliation penalty, which is the worst-case penalty over histories outside the outcome tree. The paper characterizes permissive NEs by ``good trees'' (Theorem 5) and permissive SPEs by ``good forests'' (Theorem 8), then introduces finite symbolic trees and forests as witnesses. The central claims are Corollaries 12 and 13, which assert that the existence of such equilibria is equivalent to the existence of symbolic witnesses of height polynomial in the game size, the number of players, and the largest penalty bound; Theorems 14 and 15 then use those witnesses to give PSPACE decision procedures for the constrained penalty problem and for weakly/strongly winning variants when the penalty bounds are encoded in unary.

Significance. If the proof obligations are completed, this is a valuable contribution: it extends the two-player permissive-strategy framework of Bouyer-Duflot-Markey-Renault to multiplayer equilibrium concepts, provides structural tree/forest characterizations, and gives uniform PSPACE decision procedures for several natural robustness and relevance problems. The paper is self-contained in its main definitions and the appendix contains detailed proofs of the equilibrium characterizations (Theorems 5 and 8). The decision procedures are constructive and are stated as falsifiable complexity claims rather than as existence arguments relying on hidden parameters. The main weakness is that the finite-witness compression step, Proposition 11, is presented as a sketch and its displayed height bound is exponential in the number of players, which directly affects the PSPACE statements.

major comments (3)
  1. [Appendix B, Proposition 11] The displayed bound alpha = |V| x |D| x 2^{|D|} x sum_{i in N'} P_i is exponential in |D|. Since Remark 10 and Corollary 12 take D = N for permissive Nash equilibria, and since a tree in a good forest can have D = N\I = N, the claimed polynomial height bound is false as stated. The PSPACE algorithms in Theorems 14 and 15 require the alternating polynomial-time machine to guess and check a symbolic tree or forest of polynomial height; a witness of height 2^{|D|} cannot be guessed and checked in polynomial time. The informal explanation that the labels cannot freely change suggests that a polynomial bound may be obtainable by counting actual label changes along a branch (I increases at most |D| times, each m_i switches at most twice, and each p_i increases at most P_i times), but that bound is not what is written. The authors must either prove the tighter bound explicitly or revise the complexity claim.
  2. [Section 5.3, proof of Theorem 15] The proof states: ``For the retaliation penalties, for each player, we check that the total penalty of all new symbolic trees T_{i,u,I} is below the given upper threshold.'' However, RPenalty_i(F) is defined in Section 4.2 and used in Corollary 13 as the supremum of Penalty_i(T) over the trees in Out, not as a sum over trees. If the algorithm literally checks that the sum of the penalties is at most r_i, it is incomplete: it will reject valid forests in which each individual tree has penalty at most r_i but the sum of the penalties exceeds r_i. If a different check is intended, the proof must be rewritten to describe how the universal branches enforce the supremum condition. Since this proof is the only justification for the SPE PSPACE result, the issue must be resolved.
  3. [Section 5.1, paragraph after Proposition 11] The passage arguing that Proposition 11 can be applied independently to each tree of a forest to obtain a symbolic forest is only sketched. It claims that gamma_{~H} is componentwise not above gamma_F and therefore (gamma_{~H}, N\I)-resistance is inherited, but the monotonicity argument is not written out. This step is load-bearing for Corollary 13 and therefore for Theorem 15; it should be a formal proof rather than a remark.
minor comments (4)
  1. [Corollary 13] Item 2(a) says each tree is ``(N\I)-resistant to internal deviations, and (gamma_F, N)-resistant,'' but Remark 10 and Definition 7 require the second condition to be (gamma_F, N\I)-resistance. As written, the corollary is misstated and should be corrected.
  2. [Remark 10] There is a duplicated word in ``a good forest iff each each tree T_{i,v,I} of F is ...''; this should be fixed.
  3. [Appendix B, Proposition 11 proof] The grammar in the sentence ``every branch ultimately ends with a label where all values m_i are bottom or ?'' uses ``ends'' with a plural subject; this is a minor presentation issue.
  4. [Section 5.2, proof of Theorem 14] The proof says the vector gamma_G ``has exponential size, but the index I in a triple (i,v,I) is useless''; this is true only if i in I is the only relevant information, and the sentence could be clarified by stating explicitly that I is maintained along the execution rather than stored in the precomputed vector.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the PSPACE results follow from newly proved tree/forest characterizations and a self-contained compression lemma; self-citations are background only.

full rationale

The central PSPACE claims in Theorems 14 and 15 are derived from Corollaries 12 and 13, which in turn rest on the paper's own characterizations (Theorems 5 and 8) and on Proposition 11. The characterizations are proved in full in Appendix A, not imported from the authors' prior work: the proof of Theorem 5 is self-contained, and the proof of Theorem 8 relies on an external result by Brihaye, Bruyère, Meunier and Raskin [12] plus a proposition proved in the paper. Proposition 11 is a constructive compression argument for good trees; although its displayed bound contains a 2^{|D|} factor and is therefore debatable as a polynomial bound, that is a correctness/complexity concern, not a circularity: the construction does not assume the target existence result and no fitted parameter or input-derived constant is renamed as a conclusion. The decision algorithms in Theorems 14 and 15 exploit standard equivalences (AP = PSPACE [13]) and standard reachability winning-region computations [15], and they verify the symbolic-tree conditions rather than presupposing them. Self-citations to [9,10,11] appear only as background for the classical equilibrium characterizations and are not load-bearing: the invoked results are either proved in the present paper or supplied by external references. Accordingly, no circular step is exhibited. The possible exponential height bound in Proposition 11 is a potential gap in the polynomial-height premise, but it does not make the derivation equivalent to its inputs by definition; it belongs to a correctness evaluation, not to circularity analysis.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The paper introduces no fitted constants or empirical entities. Multi-strategies and penalties are definitions taken from prior work, and symbolic trees and forests are proof artifacts with no independent falsifiable content.

assumptions (5)
  • standard math AP = PSPACE, as established by Chandra, Kozen, and Stockmeyer.
    Used in Theorems 14 and 15 to convert alternating polynomial-time Turing machine constructions into PSPACE decision procedures.
  • standard math Two-player zero-sum reachability games are determined and winning regions are computable in polynomial time.
    Used for retaliation strategies in Theorem 5 and for precomputing the gamma_G vector in Remark 10 and Corollary 12.
  • domain assumption In reachability games, weak and very weak subgame-perfect equilibria coincide with subgame-perfect equilibria.
    Cited from Proposition 16 based on [12], this equivalence is used in the proof of Theorem 8 to reason about one-shot deviations.
  • standard math Koenig's lemma: every finitely branching infinite tree has an infinite branch.
    Used in the proof of Proposition 11 to argue that the core of a strongly winning tree is finite.
  • domain assumption The game graph is finite, has no deadlocks, and players' objectives are reachability of target sets.
    This is the explicit model of Section 2 and is necessary for the tree-height bounds and for the existence of winning strategies.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Permissive Equilibria in Multiplayer Reachability Games." pith.science (2026). https://pith.science/paper/P2WDYI42

@misc{pith2026241113296,
  author       = {Pith},
  title        = {Pith review of: Permissive Equilibria in Multiplayer Reachability Games},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/P2WDYI42}},
  note         = {Machine review of arXiv:2411.13296}
}
read the original abstract

We study multi-strategies in multiplayer reachability games played on finite graphs. A multi-strategy prescribes a set of possible actions, instead of a single action as usual strategies: it represents a set of all strategies that are consistent with it. We aim for profiles of multi-strategies (a multi-strategy per player), where each profile of consistent strategies is a Nash equilibrium, or a subgame perfect equilibrium. The permissiveness of two multi-strategies can be compared with penalties, as already used in the two-player zero-sum setting by Bouyer, Duflot, Markey and Renault. We show that we can decide the existence of a multi-strategy that is a Nash equilibrium or a subgame perfect equilibrium, while satisfying some upper-bound constraints on the penalties in PSPACE, if the upper-bound penalties are given in unary. The same holds when we search for multi-strategies where certain players are asked to win in at least one play or in all plays

Figures

Figures reproduced from arXiv: 2411.13296 by the authors.

Figure 7
Figure 7. a core taking care of the strongly winning part (which will thus ensure that the [PITH_FULL_IMAGE:figures/full_fig_p023_7.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

16 extracted references · 14 canonical work pages

  1. [1]

    There exists a permissive NEΘ in (G,v 0) such that⟨Θ⟩H v0 =T

    work page

  2. [2]

    The treeT is good. Proof. (1⇒ 2) Let us assume that there exists a permissive NEΘ in (G,v 0) such that⟨Θ⟩H v0 =T . First, let us assume by contradiction that the treeT is not resistant to internal deviations. Therefore, there existshv∈T with v∈ Vi (for somei∈ N) such that |{hvv′∈T |v′∈V}|≥ 2, as well as two playsρ,ρ′∈T ∞ ↾hv such that Gaini(hρ) = 0 and Ga...

    work page

  3. [3]

    Moreover, for a subsetWin of players, if we start withT that is strongly (respectively, weakly) winning w.r.t

    ~U is (γ,D )-resistant. Moreover, for a subsetWin of players, if we start withT that is strongly (respectively, weakly) winning w.r.t. Win, then we can make the above construction so that moreover~U is strongly (respectively, weakly) winning w.r.t.Win. Proof. LetT be a treeD-resistant to internal deviations, and(γ,D )-resistant. The proof consists in addi...

    work page

  4. [5]

    ⟨Θ⟩H v0 =T∗; b

    There exists a permissive SPEΘ in (G,v 0) such that: a. ⟨Θ⟩H v0 =T∗; b. Θ is strongly winning w.r.t.Win; c. for alli∈ N, MPenaltyi(Θ,v 0)≤mi and RPenaltyi(Θ,v 0)≤ri

    work page

  5. [6]

    Θ is weakly winning w.r.t.Win

    There exists a good forestF in (G,v 0) such that: a. T 0,v0,I0 =T∗; b. for allρ∈T ∞ 0,v0,I0, for alli∈ Win, Gaini(ρ) = 1; c. for alli∈ N, MPenaltyi(F)≤mi and RPenaltyi(F)≤ri. A. Goeminne and B. Monmege 19 These assertions are still equivalent by replacing 1b by “Θ is weakly winning w.r.t.Win” and 2b by “there existsρ∈T ∞ 0,v0,I0 such that for alli∈ Win, G...

    work page

  6. [7]

    for all i∈ N and for all hv∈ Histi(v0), if| Θi(hv)|≥ 2, then for allρ,ρ′∈⟨ Θ↾h⟩v, Gaini(hρ) = Gaini(hρ′)

    work page

  7. [8]

    for all i∈ N and hv∈ Histi(v0) such that there existsu′∈ Succ(v)\ Θi(hv), if there exists ρ′∈⟨ Θ↾hv⟩u′ such that Gaini(hvρ′) = 1, then for allρ∈⟨ Θ↾h⟩v, Gaini(hρ) = 1. Proof. 1. Let i∈ N and hv∈ Histi(v0) such that| Θi(hv)|≥ 2. We assume that there exist ρ,ρ′∈⟨ Θ↾h⟩v such that Gaini(hρ) = 0 and Gaini(hρ′) = 1. Let u and u′ be the first vertices ofρ and ρ′...

    work page

  8. [9]

    If there exists ρ∈⟨ Θ↾h⟩v such that Gaini(hρ) = 0, then any strategy profileσ ≲ Θ such that⟨σ↾h⟩v =ρ and⟨σ↾hv⟩u′ =ρ′ cannot be a very weak SPE

    Leti∈ N andhv∈ Histi(v0) such that there existu′∈ Succ(v)\Θi(hv) andρ′∈⟨ Θ↾hv⟩u′ with Gaini(hvρ′) = 1. If there exists ρ∈⟨ Θ↾h⟩v such that Gaini(hρ) = 0, then any strategy profileσ ≲ Θ such that⟨σ↾h⟩v =ρ and⟨σ↾hv⟩u′ =ρ′ cannot be a very weak SPE. Indeed, let us consider the subgame(G↾h,v ) and the one-shot deviating strategyσ′ i from 20 Permissive Equilib...

    work page

Show all 16 references
  1. [10]

    Θ is weakly winning w.r.t.Win

    By Proposition 17, we have that for allπ∈⟨ Θ↾hg⟩u, Gainj(π) = 1. To conclude, as ρ∈T ∞ i,v I↾gu =⟨Θ↾hg⟩u, Gainj(ρ) = 1. We have proved thatF is a good forest withT 0,v0,I0 =T∗. Since Θ is strongly winning w.r.t. Win, we have that for allσ ≲ Θ, for alli∈ Win, Gaini(⟨σ⟩v0) = 1. ...

  2. [11]

    ~U is D-resistant to internal deviations

  3. [12]

    in ~U, every playeri∈ N′ has a penalty at mostPi

  4. [14]

    ~U1 is D-resistant to internal deviations

  5. [15]

    in ~U1, each playeri∈N′ has a penalty at mostPi

  6. [16]

    Moreover, by the core of the symbolic tree, we know that~U1 is strongly winning w.r.t.Win

    ~U1 is (γ,D )-resistant. Moreover, by the core of the symbolic tree, we know that~U1 is strongly winning w.r.t.Win. We now explain how to reduce the height of this symbolic tree, by reducing the height of the core and expanded core, while maintaining the rules (a), (b), (c), a...

  7. [2019]

    12 Thomas Brihaye, Véronique Bruyère, Noémie Meunier, and Jean-François Raskin

    doi:10.1007/978-3-030-30806-3\_5. 12 Thomas Brihaye, Véronique Bruyère, Noémie Meunier, and Jean-François Raskin. Weak subgame perfect equilibria and their application to quantitative reachability. InCSL 2015, volume 41 ofLIPIcs, pages 504–518. Schloss Dagstuhl - Leibniz-Zentr...

    2015 doi

  8. [2024]

    17 Michael Ummels

    doi:10.1007/978-3-031-57256-2\_9. 17 Michael Ummels. Rational behaviour and strategy construction in infinite multiplayer games. In FSTTCS 2006, volume 4337 of LNCS, pages 212–223. Springer, 2006. doi:10.1007/ 11944836\_21. A Proofs of Section 4: Characterizations of permissiv...

    2006 doi

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.