{"id":"55788902-96d6-41bc-a384-d76a5b1c4b48","arxiv_id":"2411.13296","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Permissive Nash and subgame-perfect equilibria with bounded main and retaliation penalties in multiplayer reachability games are decidable in PSPACE under unary-encoded penalty bounds.","lead":"Multiplayer reachability games are infinite graph games where each player wants to reach his own target set, and this paper studies multi-strategies that leave several actions open at each step. The authors prove that checking whether such a permissive profile exists while bounding the price of undeclared actions and requiring certain winners is decidable in polynomial space when the bounds are written in unary.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Proposition 11's polynomial-height bound is not polynomial as stated: its α contains a 2^{|D|} factor, and for NE (D=N) the symbolic-tree height would be exponential in the number of players.","rationale":"The reader's weakest_assumption correctly identifies Proposition 11's symbolic compression as the load-bearing step. My stress-test sharpens this into a concrete defect: the bound α displayed in the proof is exponential in |D|, so the stated polynomial-height claim fails for D = N, the case used for permissive Nash equilibria and for trees in permissive SPE forests. This directly threatens Theorems 14 and 15, since the alternating polynomial-time decision procedure cannot afford symbolic trees of height exponential in the number of players. The defect is potentially repairable: the transition rules for labels suggest a polynomial bound via counting label changes along a branch, rather than counting all possible label combinations. For this reason I do not move the verdict to REJECT; the paper should be accepted only after the height bound is corrected and a proof of the polynomial bound is supplied. I mark agreement as 'partial' because the reader flagged the compression step as insufficiently formal, but not the specific 2^{|D|} factor that makes the written bound non-polynomial. The conditional verdict remains appropriate.","tokens_in":25132,"tokens_out":15890,"duration_ms":188265,"concrete_test":"Re-derive the maximum length of a completion branch from the update rules (a)-(c) of the Appendix B proof, counting actual label changes along a single branch: I increases at most |D| times, each m_i can switch at most twice (from ? to ∀ and then to ?), and each p_i can increase at most P_i times. If the resulting length is O(|V|(3|D| + Σ_{i∈N'} P_i + 1)), then Proposition 11 is repairable and the PSPACE argument can go through with a corrected bound. If no such polynomial bound can be derived, exhibit a family of reachability games with n players and unit penalties where the minimal good tree requires symbolic height 2^{Ω(n)}; such a family would invalidate the height premise behind Corollaries 12 and 13 and hence Theorems 14 and 15.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The PSPACE results in Theorems 14 and 15 depend on Corollaries 12 and 13, which in turn depend on Proposition 11's claim that every relevant good tree has a symbolic subtree of height polynomial in the game size, the number of players, and the largest penalty bound. The proof of Proposition 11 in Appendix B does not establish this. Its displayed bound is α = |V| × |D| × 2^{|D|} × Σ_{i∈N'} P_i. Since the label set I satisfies N\\D ⊆ I ⊆ N, the number of possible I values is 2^{|D|}, not |D|. For permissive Nash equilibria Remark 10 and Corollary 12 use D = N; for trees in a good forest, D = N\\I can also be N. Thus the bound is exponential in the number of players, not polynomial. The alternating-polynomial-time algorithms in Theorems 14 and 15 require a symbolic tree of polynomial height; an exponential height cannot be guessed and checked in polynomial time. The informal explanation that 'the three parts of the labels cannot freely change' suggests a tighter polynomial bound may be obtainable by counting actual label changes along a single branch (I increases at most |D| times, each m_i switches at most twice, each p_i increases at most P_i times), but that bound is not what is written. As it stands, the central PSPACE claim rests on an unproven and, as stated, false polynomial-height premise.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":25389,"tokens_out":9243,"duration_ms":103534,"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":[{"comment":"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.","section":"Appendix B, Proposition 11"},{"comment":"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.","section":"Section 5.3, proof of Theorem 15"},{"comment":"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.","section":"Section 5.1, paragraph after Proposition 11"}],"minor_comments":[{"comment":"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.","section":"Corollary 13"},{"comment":"There is a duplicated word in ``a good forest iff each each tree T_{i,v,I} of F is ...''; this should be fixed.","section":"Remark 10"},{"comment":"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.","section":"Appendix B, Proposition 11 proof"},{"comment":"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.","section":"Section 5.2, proof of Theorem 14"}],"recommendation":"major_revision","confidential_remarks":null},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThis paper extends the penalty-based permissiveness idea from two-player games to multiplayer reachability, and the tree/forest characterizations for permissive NE and SPE are genuinely new. Theorems 5 and 8 are clean, and the appendix proofs for those are careful. The symbolic-witness idea is natural, and if the compression step worked, the PSPACE algorithms would be a solid contribution.\n\nBut as written, the load-bearing Proposition 11 does not deliver the polynomial-height bound it claims. The proof's displayed α = |V|·|D|·2^{|D|}·Σ P_i is exponential in the number of players. Since Corollary 12 uses D = N, and Corollary 13 uses D = N∖I which can also be all of N, the symbolic trees in the NE case would have exponential height, so the alternating-polynomial-time argument in Theorems 14 and 15 cannot go through. The informal remark that the three parts of the labels cannot freely change suggests a tighter bound may be possible—counting I increases at most |D| times, each m_i switching at most twice, and each p_i increasing at most P_i times gives something polynomial. But that argument is not what is written. As it stands, the central PSPACE claim is unproven.\n\nA second, smaller issue: the abstract says the constrained penalty problem is solved for both NE and SPE, but Theorem 14 only handles NE with infinite retaliation penalties. Finite retaliation penalties are handled only for SPEs. That scope limitation should be explicit in the abstract.\n\nThe citation pattern and the mathematical setup appear honest; the characterizations are not circular, and the two-player previous work is cited properly. This is not a trivial paper: the good-tree and good-forest conditions are a real step forward, and the flaw in Proposition 11 looks repairable. But a repair requires a genuinely polynomial bound on the height of the symbolic tree, with the label-change counting made precise, or a different compression argument.\n\nSerious editor should send this to referees, but the verdict should be major revision. I would not cite the PSPACE result until Proposition 11 is fixed. Worth a reading-group discussion, mainly to see whether the refined bound actually holds.\n\nBest.","headline":"Promising framework for permissive equilibria, but the central PSPACE claim rests on a compression lemma whose written bound is exponential, not polynomial.","tokens_in":25911,"tokens_out":5743,"would_cite":false,"duration_ms":57896,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["91A18","91A20","68Q25"],"pacs":[],"model":"deepseek-v4-flash","headline":"Deciding existence of permissive equilibria with bounded penalties in multiplayer reachability games is in PSPACE under unary bounds.","keywords":["multiplayer reachability games","multi-strategies","permissive equilibria","penalties","Nash equilibrium","subgame-perfect equilibrium","PSPACE","symbolic trees"],"falsifier":"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.","tokens_in":24912,"feed_emoji":"🎯","tokens_out":8611,"duration_ms":88340,"temperature":0.7,"pith_summary":"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.","feed_headline":"Move-set equilibria are decidable in polynomial space","feed_subtitle":"Every way of picking an allowed move stays an equilibrium; penalties written in unary keep the search in PSPACE.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Introduces the penalty measure for multi-strategies in two-player games that the paper adapts to profiles.","marker":"[3]"},{"why":"Studies permissive strategies under qualitative set inclusion and shows why that notion lacks most-permissive objects, motivating quantitative penalties.","marker":"[2]"},{"why":"Provides the tree-based characterization of Nash equilibria in reachability games that is generalized to permissive Nash equilibria.","marker":"[11]"},{"why":"Characterizes weak subgame-perfect equilibria with omega-regular objectives, the basis for the forest characterization.","marker":"[9]"},{"why":"Proves that very weak subgame-perfect equilibria coincide with subgame-perfect equilibria in reachability games, used in the proof of Theorem 8.","marker":"[12]"},{"why":"Establishes that alternating polynomial time equals PSPACE, which the decision procedure exploits.","marker":"[13]"},{"why":"Supplies determinacy and winning-region computation for two-player reachability games, used to build retaliation strategies and the gain vector.","marker":"[15]"}],"fun_headline_variants":["Permissive equilibria in reachability games decided in PSPACE","Multi-strategy profiles: equilibrium existence in polynomial space","Unary penalty bounds keep permissive equilibrium search in PSPACE","Every allowed move yields equilibrium: PSPACE decision","Good-tree compression proves PSPACE for permissive equilibria"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Permissive equilibria in reachability games decided in PSPACE","Multi-strategy profiles: equilibrium existence in polynomial space","Unary penalty bounds keep permissive equilibrium search in PSPACE","Every allowed move yields equilibrium: PSPACE decision","Good-tree compression proves PSPACE for permissive equilibria"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000308,"raw_usage":{"total_tokens":1743,"prompt_tokens":913,"completion_tokens":830,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":529,"completion_tokens_details":{"reasoning_tokens":749}},"tokens_in":529,"tokens_out":830,"duration_ms":8461,"temperature":1.0,"reasoning_tokens":749,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T16:35:39.479220+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Moreover, for a subsetWin of players, if we start withT that is strongly (respectively, weakly) winning w.r.t","cited_arxiv_id":null,"evidence_quote":"Introduces the penalty measure for multi-strategies in two-player games that the paper adapts to profiles."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Studies permissive strategies under qualitative set inclusion and shows why that notion lacks most-permissive objects, motivating quantitative penalties."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the tree-based characterization of Nash equilibria in reachability games that is generalized to permissive Nash equilibria."},{"cited_title":"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","cited_arxiv_id":null,"evidence_quote":"Characterizes weak subgame-perfect equilibria with omega-regular objectives, the basis for the forest characterization."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Proves that very weak subgame-perfect equilibria coincide with subgame-perfect equilibria in reachability games, used in the proof of Theorem 8."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies determinacy and winning-region computation for two-player reachability games, used to build retaliation strategies and the gain vector."}],"review_version":1}