{"id":"4ccdf6bb-ae72-4983-b4b8-6390de0ce589","arxiv_id":"2607.24219","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Approximate constrained NE existence in concurrent stopping games is EXPTIME (PSPACE-hard); XRSE constrained existence is NP-complete.","lead":"The paper gives the first exponential-time algorithm for approximate constrained Nash equilibria in concurrent stopping games, and proves that extreme risk-sensitive equilibria are NP-complete there. It turns two undecidable multi-agent questions into tractable ones by relaxing exactness or the payoff criterion.","discovery_kind":"new_method","skeptic_critique":{"model":"moonshotai/kimi-k3","headline":"The Section 3 truncation chain contains two repairable proof slips: the discretisation parameter D = 2(K+1)R/ε ignores the factor N in the algorithm's loop bound KN, and Lemma 6's proof builds the truncated profile \"arbitrarily\" while asserting exact payoff preservation its construction cannot yield","rationale":"The reader's weakest_assumption — that everything collapses outside stopping games — is real but is a boundary of the claims, not a threat to their truth: the theorems are stated for stopping games and Section 5 scopes the non-stopping case as open. Nothing internal \"collapses\". The genuinely least-secure location is the same one the reader pointed at (the Lemma 4–6 truncation machinery) but for a different reason: two concrete slips in the written proofs. First, the cube-count parameter D = 2(K+1)R/ε is inconsistent with the algorithm's iteration to memory horizon KN, so the ε/2 error bound in Theorem 12's soundness direction fails as written by a factor of roughly N. Second, Lemma 6's appendix proof constructs the truncated profile with an \"arbitrary\" continuation — which neither satisfies Definition 5's memoryless-continuation requirement nor preserves expected payoffs — yet asserts exact payoff equality and uses it in the final line, while citing and then disavowing [14, Thm 3.2] as the would-be justification. Both are the kind of defect a careful referee catches and an author fixes in revision: the first is a one-symbol parameter change with no complexity consequence (D remains exponential in |G| and polynomial in the bit-size of ε); the second is repaired by choosing any memoryless continuation and using the tail bound 2Rλ^k ≤ δ/2, which is exactly what the lemma's statement claims anyway. No statement in the paper appears false, and the architecture (truncation + characteristic vectors + over-approximation) is sound. On the XRSE half I found no additional load-bearing flaw beyond the reader-noted dependence on the companion paper [7] for uncorrelated team punishment; the anchored-set counting argument (Lemma 22, tying the bound to the explicit transition-table size via vertex cores) is the right idea and checks out structurally. Verdict stays ACCEPT, consistent with the reader's medium correctness risk; recommend the authors patch the D parameter, harmonise K vs KN, and rewrite Lemma 6's construction.","tokens_in":26067,"tokens_out":7518,"duration_ms":224788,"concrete_test":"Two checks. (a) Instantiate N=2, K=1, R=ε=1 in Theorem 12's soundness bound: at k=KN=2 the error (k+1)R/D = (KN+1)/(2(K+1))·ε = 3ε/4 > ε/2, confirming the inequality fails as written; then re-run the Lemma 10 → Theorem 12 chain with D := 2(KN+1)R/ε and confirm every subsequent inequality, including polynomiality in the bit-size of ε, is unchanged. (b) Re-prove Lemma 6 with σ̄′ defined to follow an arbitrary fixed memoryless profile τ̄ after each length-kN prefix; verify |E_i(σ̄′) − E_i(σ̄)| ≤ 2Rλ^k ≤ δ/2 and the deviation inequality E_i(σ̄′_{−i},σ²_i) ≤ E_i(σ̄′) + δ without invoking payoff equality or [14, Thm 3.2]. If either repair requires more than constant-factor adjustment, Theorem 12's promise-gap formulation would need restatement.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The least secure point is not the stopping restriction (a stated scope boundary) but the interior of the Lemma 6 → Lemma 10 → Theorem 12 chain, which is step (1) of the three-step algorithm. (a) Parameter mismatch: Lemma 6 yields memory horizon kN, and Theorem 12's algorithm explicitly iterates \"k ranging from 0 to KN\". But §3.5 fixes D = 2(K+1)·R/ε, and the soundness direction bounds the discretisation error by (k+1)R/D ≤ (K+1)R/D = ε/2. At k = KN the actual error is (KN+1)R/D ≈ Nε/2, which exceeds ε/2 for every N ≥ 2, so the \"yes ⇒ positive instance\" argument does not go through as written. The text even oscillates between \"k ranging from 0 to KN\" and \"the maximal number of steps of this algorithm is K\". (b) Lemma 6 (App. A.1): σ̄′ follows σ̄ for kN steps and is then defined \"arbitrarily\"; but Definition 5 requires a memoryless continuation for memory horizon kN, and an arbitrary continuation perturbs expected payoffs, contradicting the proof's claim that \"each player i has the same expected payoff as in σ̄\" — an equality the final line uses (E(σ̄) = E(σ̄′)). The adjacent citation of [14, Thm 3.2] for an exactly-equivalent memoryless profile is immediately disavowed (\"might not [be] possible without correlated strategies\"), leaving that step unsupported. Both slips are genuine but erratum-level: setting D := 2(KN+1)R/ε restores the bound with no complexity change (D is already exponential in |G|, polynomial in bits of ε), and Lemma 6's statement (payoffs within δ/2) is true with any memoryless continuation via the tail bound 2Rλ^k ≤ δ/2, constants absorbed. The theorem statements survive; the proofs as written do not quite.","agreement_with_reader":"partial"},"referee_report":{"model":"moonshotai/kimi-k3","summary":"The paper studies the constrained existence problem for equilibria in terminal-reward concurrent stochastic games under the stopping assumption (every strategy profile reaches a terminal almost surely). Since the exact problem is undecidable even in this setting, the authors pursue two relaxations. First, they give an approximate (gap) decision procedure for constrained existence of Nash equilibria: they show that any NE can be truncated to an ε/2-NE of finite memory horizon KN (Lemmas 4–6), define a characteristic vector recording each player's payoff and best deviation value (Definition 8), and compute an inductive cube over-approximation of the set of characteristic vectors of horizon-k profiles with controlled error (Lemmas 10–11), yielding an algorithm that runs in time exponential in the game size and polynomial in the bit-size of ε (Theorem 12), plus a PSPACE-hardness lower bound via QBF (Theorem 14). Second, for extreme risk-sensitive equilibria (XRSE), they prove the constrained existence problem is NP-complete on concurrent stopping games (Theorem 29), via a finite-memory witness construction based on anchored players, i-ranks, and a combinatorial bound on the number of anchored sets (Lemmas 20–28).","tokens_in":26528,"tokens_out":3811,"duration_ms":113688,"significance":"If the results hold, this is a solid contribution. The approximate algorithm is the first for constrained NE existence without any restriction on strategies, and it quantifies the gain precisely: undecidability collapses to EXPTIME, with only polynomial dependence on the bit-size of epsilon — a sharp statement of what approximation buys. The PSPACE lower bound, already for turn-based pure equilibria, usefully delimits the gap. The XRSE half closes an explicitly open problem and the anchored-set counting argument (Lemma 22), which charges the potential exponential blow-up in anchored sets against the exponential input representation of concurrent transition matrices, is an elegant and genuinely concurrent-specific insight; the handling of uncorrelated punishment via [7] addresses a real obstacle rather than assuming it away. The stopping-games restriction is a real scope boundary but is stated honestly and motivated. The work is reproducible in the sense that all constructions are explicit and the complexity accounting is checkable; there are no hidden parameters.","major_comments":[{"comment":"Discretisation parameter mismatch. The algorithm iterates \"k ranging from 0 to KN\" (correct, since Lemma 6 delivers memory horizon KN), and Lemma 10 bounds the approximation error of X_k by (k+1)R/D. At k = KN the error is (KN+1)R/D, but D is fixed as 2(K+1)R/epsilon, giving an error of roughly N*epsilon/2, which exceeds the epsilon/2 slack used in the soundness direction (\"yes => positive instance\") for every N >= 2. The fix is immediate: set D := 2(KN+1)R/epsilon. This does not affect the complexity claim, since D is already exponential in |G| and polynomial in the bit-size of epsilon. Relatedly, the complexity paragraph says \"the maximal number of steps of this algorithm is K\", which should read KN+1; the text oscillates between the two and should be made consistent.","section":"§3.5 and Theorem 12 (§3.6)"},{"comment":"The truncation construction has two defects. First, sigma-bar' is defined to follow sigma-bar for kN steps and is then defined \"arbitrarily\" on extensions of length-kN histories; but Definition 5 requires the continuation after the horizon to be memoryless, so an arbitrary continuation does not in general produce a profile of memory horizon kN. Second, the proof asserts \"each player i has the same expected payoff as in sigma-bar\" (and uses E(sigma-bar) = E(sigma-bar') in the final line), which the construction cannot guarantee. The adjacent citation of [14, Thm 3.2] for an exactly payoff-equivalent memoryless profile is immediately disavowed (\"might not [be] possible without correlated strategies\"), so that step is currently unsupported. The lemma's statement (payoffs within delta/2) is nevertheless true under a corrected argument: after kN steps, switch to any fixed memoryless profile;","section":"Lemma 6, proof in Appendix A.1"}],"minor_comments":[{"comment":"In the NP-membership argument, the guessed witness includes choice functions valued in probability distributions. The paper should state explicitly that a witness with polynomially bounded bit-size exists. This follows because all verification questions reduce to positive-probability and almost-sure reachability, which depend only on supports, not on probability values; a sentence making this explicit would close the gap. Similarly, in Proposition 35 the invocation of Lemma 27 requires the opponent profile to be memoryless; strictly, one must pass to the product of the game with the (polynomial-size) memory structure, on which sigma-bar*-_{-i} is memoryless. Worth one clarifying sentence.","section":"Theorem 29 (§4.6) and Proposition 35 (App. B.3)"},{"comment":"The QBF instance is described with \"each clause C_i is a conjunction of three literals\"; this should be disjunction (the game construction and the rest of the argument are consistent with CNF clauses).","section":"Theorem 14, proof in App. A.4"},{"comment":"\"the path can be chosen of length at most N+1\" and later \"from any path v\" — the latter should read \"from any vertex v\". Also footnote 1 (\"the number of action interactions is then kN\") is cryptic; the convention that a step is a vertex visit while the horizon is measured in kN should be stated once, clearly, in the preliminaries.","section":"Lemma 4 proof (§3.2)"},{"comment":"Typos and glitches: \"problem of approximate constrained existence problem\" (abstract and §3.1); \"the can be done\" (Thm 12 complexity paragraph); \"doe snot\" and \"sine the vertex\" (App. A.4); \"Throught the claim\" (App. B.3); \"an delta-NE\" (App. A.1); \"from the result from the result from MDP literature\" (§4.5); in Definition 5 the quantified memoryless profile is written tau-bar without the subscript h; \"can be assume to form a punishing coalition\" (§1).","section":"Various"},{"comment":"Figures 1 and 2 are essential to following Example 17 and the QBF reduction, but the extracted/printed quality of the player glyphs and edge labels is poor; please check the final typeset versions for legibility.","section":"Figures 1 and 2"}],"recommendation":"minor_revision","confidential_remarks":"The two self-citations [7] (CAV 2026, to appear) and [8] (MFCS 2025) are load-bearing black boxes: Lemma 26 rests entirely on [7, Thms 1 and 5], and the NP lower bound for XRSE is imported from [8]. Since [7] is not yet published, the editor may wish to ask the authors to ensure the extended version cited (arXiv:2603.07094) remains stable and that the exact theorem numbers match. This is a dependency question, not a correctness concern."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The new results are real. Theorem 12 gives the first approximate constrained-existence procedure for Nash equilibria in concurrent stopping games that places no restriction on strategy memory; prior approximate work needed memoryless strategies. Theorem 29 closes the concurrent case for extreme risk-sensitive equilibria at NP-complete, matching the turn-based bound. Both sit cleanly against the known undecidability wall for exact NE even in 10-player stopping games.\n\nWhat works: the three-step pipeline (finite-horizon truncation via the stopping-probability bound, characteristic vectors, cube over-approximation of the X_k sets) is a sensible way to turn an undecidable problem into an EXPTIME one that is only polynomial in the bits of ε. The XRSE half is careful: the anchored-set counting argument ties the number of distinct labels to the explicit size of the transition tables, so concurrency does not produce an exponential blow-up in the number of players, and they correctly invoke uncorrelated memoryless punishment rather than pretending the coalition can share randomness. The QBF reduction for PSPACE-hardness is standard and already holds for pure/turn-based instances. Appendices supply the inductive arguments and the memory-structure construction.\n\nSoft spots, in proportion. The whole development is scoped to stopping games; the authors say so and leave the general case open. There is an EXPTIME–PSPACE gap left open, and the approximate problem is phrased with a promise gap. More concretely, the Lemma 6 \to Lemma 10 \to Theorem 12 chain has two repairable slips: D is set to 2(K+1)R/ε while the algorithm loops to horizon KN, so the written error bound fails by a factor of N, and the appendix proof of Lemma 6 claims exact payoff preservation after an “arbitrary” continuation that Definition 5 does not allow. Both are fixable without changing complexity (inflate D by N; use any memoryless tail and absorb the 2Rλ^k mass into the δ/2 slack). The theorem statements survive; the proofs as written need an erratum pass.\n\nThis is for people who work on algorithmic multi-agent verification or stochastic games. It deserves a serious referee. I would engage with it and expect it to be fixable into a solid theory-conference paper.","headline":"First unrestricted-strategy EXPTIME approx-NE algorithm for concurrent stopping games, plus NP-completeness for XRSE; two erratum-level slips in the truncation chain do not kill the theorems.","tokens_in":26813,"tokens_out":586,"would_cite":true,"duration_ms":12447,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["91A15","68Q25","91A43"],"pacs":[],"model":"grok-4.5","headline":"In concurrent stopping games, approximate Nash equilibria are decidable in exponential time and extreme risk-sensitive equilibria are NP-complete.","keywords":["Nash equilibria","concurrent games","stopping games","ε-Nash equilibria","extreme risk-sensitive equilibria","constrained existence","multi-agent systems"],"falsifier":"Exhibit a concurrent stopping game and a rational ε for which the cube-over-approximation algorithm returns the wrong yes/no answer, or a polynomial-memory XRSE witness that the NP procedure rejects.","tokens_in":26504,"feed_emoji":"⚖️","tokens_out":768,"duration_ms":19834,"temperature":0.7,"pith_summary":"The constrained existence problem for exact Nash equilibria is undecidable even in concurrent stopping games. This paper restores tractability in two ways. First, it decides whether an ε-Nash equilibrium with prescribed payoffs exists, running in time exponential in the game and only polynomial in the bit-size of ε, and proves the problem is already PSPACE-hard for turn-based games. Second, it shows that when players instead optimise the best or worst payoff that occurs with positive probability (extreme risk-sensitive equilibria), the same constrained existence question becomes NP-complete. Both results matter because they give the first algorithms that work for unrestricted strategies in the concurrent setting, a natural model of synchronous multi-agent systems that must eventually terminate.","feed_headline":"Approximate Nash becomes EXPTIME in stopping games","feed_subtitle":"Exact equilibria stay undecidable; extreme risk measures drop to NP-complete even with concurrency","key_machinery":"Characteristic vectors of finite-memory-horizon strategy profiles, discretised into cubes whose size is controlled by ε, together with an anchoring/rank labelling that produces a polynomial-size memory structure for XRSE witnesses.","core_discovery":"For concurrent stopping games the approximate constrained-existence problem for Nash equilibria is in EXPTIME (and PSPACE-hard already for turn-based and pure equilibria), while the exact constrained-existence problem for extreme risk-sensitive equilibria is NP-complete.","pith_inferences":["The exponential dependence on game size (via the horizon K) suggests that practical implementations will need aggressive pruning or symbolic representations of the cube sets.","Value-at-risk equilibria with a positive tolerance parameter look like a natural next target: the paper’s rank technique may lift once the support condition is replaced by a probability threshold.","If the stopping hypothesis can be relaxed to almost-sure termination under the candidate equilibrium alone, both algorithms would immediately apply to a larger class of concurrent games."],"forward_implications":["Exact Nash constrained existence stays undecidable, but any practical query that tolerates a known additive error becomes algorithmically answerable.","XRSE constrained existence can be decided by a nondeterministic polynomial-time guess of a polynomial-size memory structure followed by ordinary MDP reachability checks.","The same PSPACE lower bound applies to pure approximate equilibria, so randomisation is not the sole source of hardness.","Memoryless team-punishment strategies without shared randomness suffice to enforce XRSE deviations in the concurrent setting."],"fun_headline_variants":["Approx Nash constrained existence hits EXPTIME in concurrent stopping games","Exact NE undecidable; approx version EXPTIME for stopping games","XRSE constrained existence NP-complete even under concurrency","Stopping games: approx NE in EXPTIME, XRSE exact in NP","PSPACE-hard approx NE already for turn-based pure equilibria"],"cache_read_input_tokens":16512,"weakest_assumption_plain":"Every strategy profile must reach a terminal state with probability one; without that stopping assumption both the finite-horizon truncation and the rank construction fail.","fun_headline_variants_meta":{"raw":{"variants":["Approx Nash constrained existence hits EXPTIME in concurrent stopping games","Exact NE undecidable; approx version EXPTIME for stopping games","XRSE constrained existence NP-complete even under concurrency","Stopping games: approx NE in EXPTIME, XRSE exact in NP","PSPACE-hard approx NE already for turn-based pure equilibria"]},"model":"grok-4.5","effort":"low","cost_usd":0.005928,"raw_usage":{"total_tokens":1537,"prompt_tokens":769,"num_sources_used":0,"completion_tokens":76,"cost_in_usd_ticks":59284000,"prompt_tokens_details":{"text_tokens":769,"audio_tokens":0,"image_tokens":0,"cached_tokens":128},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":692,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":769,"tokens_out":76,"duration_ms":11932,"temperature":1.0,"reasoning_tokens":692,"cache_read_input_tokens":128,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-31T20:40:12.838247+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"Exhibit a concurrent stopping game and a rational ε for which the cube-over-approximation algorithm returns the wrong yes/no answer, or a polynomial-memory XRSE witness that the NP procedure rejects.","supporting_citations":[],"review_version":1}