{"id":"8c2747d5-7c85-417b-94ef-5b267a00077e","arxiv_id":"2504.16528","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"QaSTels encode all winning strategies in energy and mean-payoff games via edge activation thresholds, synthesized by edge-based value iteration.","lead":"This paper introduces Quantitative Strategy Templates (QaSTels), compact data structures that encode all winning strategies for energy and mean-payoff games. They let game-based controllers adapt at runtime and add new objectives incrementally, with experiments showing large speedups on benchmark games.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Permissiveness theorems appear sound; the real gap is Proposition 3, whose proof is incomplete and which underpins runtime adaptability and MiSTel soundness.","rationale":"I independently checked the two permissiveness theorems. Theorem 3's proof is sound: for a winning pi-play, each prefix credit dominates the edge-optimal value of the edge just taken, and the case u0 not in W is handled by the definition of (Pi,c)-plays. Lemma 1 is valid: in the finite-memory product graph, all reachable simple cycles have non-negative total weight, and any prefix is an acyclic part plus at most one partial cycle, so B_pi = 2|V'|W is a correct bound. Theorem 4 then follows by choosing c = max(W|V|, B_pi) and invoking Theorem 3. The genuinely load-bearing gap is Proposition 3. It is stated without proof in the main text, and the appendix proof (Cor. 2) has a reversed inequality and an unjustified Knaster-Tarski application. The statement is plausibly true via a Bellman-fixed-point induction, but that argument is absent. Because eq. (6), the conflict-free criterion of Algorithm 2, Theorem 6, and the fault-tolerance experiment all depend on Prop. 3, the paper's advertised runtime robustness is not yet established. This does not undermine the core QaSTel permissiveness results, so the reader's CONDITIONAL verdict is appropriate. Minor additional concerns: Theorem 5's stated complexity is not derived in the proof text, and the empirical section lacks code/data release, but these are secondary.","tokens_in":22502,"tokens_out":16267,"duration_ms":164799,"concrete_test":"Run a randomized falsification check for Proposition 3: for small random weighted graphs (|V| <= 8, weights in [-3,3]), compute the optimal QaSTel Pi from scratch, choose a random subset F of Player0 edges such that for every node v at least one edge in argmin_{e in E(v)} act_Pi(e) is not in F, delete F to obtain G', recompute optE' from zero, and compare act_Pi'(e) with act_Pi(e) for all remaining edges. Repeat at least 10^4 times; any mismatch falsifies Prop. 3. In parallel, re-derive Cor. 2 with the inequality direction corrected and verify that optE is a fixed point of the modified edge operator before invoking Knaster-Tarski.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central permissiveness theorems (Thm 3 and Thm 4) appear sound. For Thm 3, a winning pi-play from a winning node has each prefix credit at least the edge-optimal value of the edge just taken, and the outside-winning-region case is handled by the definition of (Pi,c)-plays. Lemma 1 is also valid: in the finite-memory product graph all reachable simple cycles have non-negative total weight, so every prefix consists of an acyclic part plus at most one partial cycle, giving the uniform bound B_pi = 2|V'|W. Thm 4 then follows by taking c = max(W|V|, B_pi) and applying Thm 3. The load-bearing gap is Proposition 3 (Sec. 5.1), which is stated without proof in the main text and used both for runtime adaptability (eq. 6) and for the soundness of MiSTel synthesis (Thm 6 through Cor. 2). The appendix proof (Cor. 2, App. A.7) is incomplete: it derives the inequality in the wrong direction ('optE(e) >= optE'(e)' where the needed claim is 'optE(e) <= optE'(e)'), and the Knaster-Tarski step would require first showing that optE is a fixed point of the edge operator of G', which is not done. The intended argument should be a Bellman-equation induction showing that if every Player0 node retains at least one minimal-activation edge, the least fixed point of O'_E equals optE restricted to the remaining edges. That argument is absent. Since Algorithm 2's conflict-free condition and the fault-tolerance experiment in Sec. 7 both rely on Prop. 3, the runtime-adaptability claim is not yet established even though the permissiveness core may be correct. The claimed O(k|V||E|W) complexity of Theorem 5 is also under-justified in the proof text, but this is secondary.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces Quantitative Strategy Templates (QaSTels), which are local edge-activation annotations that succinctly represent families of winning strategies in two-player energy and mean-payoff games. The main theoretical results are that an optimal QaSTel, computed by an edge-based value iteration, is winning and maximally permissive for energy games (Theorem 3) and f-maximally permissive for mean-payoff games (Theorem 4). The paper also proposes a combination of QaSTels with bounded PeSTels into MiSTels for mixed quantitative/qualitative objectives, an incremental synthesis algorithm (Algorithm 2), and a prototype implementation evaluated on benchmarks derived from SYNTCOMP. The central permissiveness theorems have detailed appendix proofs, while the runtime-adaptability and MiSTel-soundness claims are shown to rest on Proposition 3, whose proof is incomplete.","tokens_in":22857,"tokens_out":4925,"duration_ms":49483,"significance":"If the results are fully established, the paper makes a useful contribution by transferring permissive strategy templates from qualitative parity games to quantitative energy and mean-payoff games, with a permissiveness guarantee that goes beyond single winning strategies. The edge-based value iteration and the extraction of the optimal QaSTel are cleanly defined, and Theorems 2--4 appear substantially correct. The empirical section is a strength: it builds a new benchmark suite, implements the state-of-the-art MPCoBuechi algorithm as a baseline, and reports quantitative comparisons for incremental synthesis. The paper does not provide machine-checked proofs or a code/data release, but the detailed appendix proofs and prototype experiments are valuable. The main unaddressed issue is the missing or incorrect proof of Proposition 3, which underpins both the runtime-adaptability claim and the soundness of MiSTel synthesis; until that is fixed, the applied claims are not fully supported.","major_comments":[{"comment":"Proposition 3 is load-bearing for the runtime-adaptability claim (Eq. (6)) and for the soundness of Algorithm 2 via Theorem 6, but its proof is not supplied. The appendix proof of Corollary 2 first states the desired inequality optE(e) <= optE'(e), then derives the opposite inequality optE(e) >= optE'(e) from winning strategies in G', and it never shows that optE is a fixed point of the edge operator O'_E of G'. Consequently, the Knaster-Tarski step does not apply, and the claim that computeQaSTel(G',w,act_Π) equals computeQaSTel(G',w,µ0) is unsubstantiated. The intended argument should be a Bellman-equation induction showing that if every Player-0 node retains at least one minimal-activation edge, then the least fixed point of O'_E equals optE on the surviving edges; that argument is absent and must be supplied or the later claims must be weakened.","section":"Sec. 5.1 and App. A.7"},{"comment":"The complexity claim O(k·|V|·|E|·W) for CombineQaSTel is not proved. The proof in Appendix A.6 ends with 'the time complexity of the algorithm is O(k·|V|·|E|)', omitting the W factor, and the theorem's W factor is never justified. Moreover, each outer iteration hot-starts computeQaSTel from the previous activation function, and the proof does not bound the accumulated cost of these hot-started value iterations over up to |V| outer iterations. Please provide a per-iteration bound that accounts for W and the number of value-iteration rounds, or revise the claimed complexity accordingly.","section":"Thm. 5 and App. A.6"},{"comment":"The statement of Proposition 3 is tautological as written: it asserts that Π = computeQaSTel(G',w,µ0) is the optimal QaSTel for G'\\E*_t, but Π is already defined as exactly that object by the right-hand side. The intended content — namely, that the original activation function act_Π, restricted to the remaining edges, still coincides with the optimal edge values in the modified game — is not actually stated. The proposition and its surrounding text should be reformulated so that the condition under which the original template remains optimal is explicit and testable.","section":"Sec. 5.1, Proposition 3"}],"minor_comments":[{"comment":"The sentence 'n the context of the previously discussed robot example' contains a typo and should read 'In the context'.","section":"Sec. 1, p. 2"},{"comment":"The set 'W'×(W\\W')' denotes node pairs, not necessarily edges; please write {e∈E | src(e)∈W', tgt(e)∈W\\W'} and justify why all such edges are Player-0 edges.","section":"Alg. 1, line 5"},{"comment":"The x-axis is labeled 'Player 0 edges deleted (in %)' while the text describes the average number of deletions needed to remove a minimal-activation edge; please align the axis label with the reported quantity.","section":"Sec. 7, Fig. 3a"},{"comment":"The footnote marker after 'T' appears malformed in the provided text, and the sentence around it is awkward; please repair the citation and the sentence structure.","section":"Sec. 6.3, footnote 2"},{"comment":"The proof should explicitly justify why a reachable simple cycle of negative weight in Gπ yields a π-play with negative limit average weight; the current sentence 'has a negative limit average weight' is a conclusion without the intervening argument.","section":"App. A.4, Lemma 1"}],"recommendation":"major_revision","confidential_remarks":"The central permissiveness results are promising, but the missing Proposition 3 proof is a genuine load-bearing gap rather than a presentation issue. The paper also leans heavily on the authors' prior PeSTel work, which is natural here, but the novelty and incremental contribution should be assessed once the proof gap is resolved; the empirical claims about robustness currently inherit the unresolved status of Proposition 3."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The permissiveness results are the heart of this paper, and they look like they hold up. The edge-based value iteration is a straightforward variant of the standard one, but the definitions of QaSTels and the proofs that the optimal template captures all energy-winning strategies and all finite-memory mean-payoff-winning strategies are genuine contributions. I checked the argument for Theorem 3 and the use of Lemma 1 in Theorem 4; the logic is plausible and the details in the appendix are mostly there. That's the part worth citing.\n\nThe weak spot is Proposition 3, which is doing a lot of work and is not established. The statement is given without proof in the main text, and the appendix proof (as Corollary 2) has an inequality going in the wrong direction: it claims to show optE(e) ≤ optE'(e), but the proof derives optE(e) ≥ optE'(e). The Knaster-Tarski step then assumes what needs to be shown. Since this proposition underpins the runtime-adaptability claim (equation 6) and the soundness of MiSTel synthesis (through Theorem 6), that whole part of the paper is currently unsupported. The authors either need a correct proof of Prop. 3 or they need to weaken the claims that depend on it.\n\nAlso, the complexity statement in Theorem 5 is under-justified. The proof text omits the W factor and does not explain why hot-starting across up to |V| iterations of the while loop gives the claimed O(k·|V|·|E|·W) bound rather than something with an extra |V|. The same issue appears in Corollary 3. This is secondary, but a serious referee will want the accounting done properly.\n\nThe empirical section is illustrative but not reproducible as written: no code or data is shipped, and the random graph modifications are described only at a high level. That's a minor issue for a theory paper, but it does mean the performance claims should be read loosely.\n\nWho should read this? People working on reactive synthesis, quantitative games, or controller design with runtime adaptation will find the permissiveness idea useful. The paper deserves serious peer review — the core is novel and likely correct — but it needs a major revision on Proposition 3 and the complexity analysis before I would trust the broader claims.","headline":"The permissiveness theorems for QaSTels are the real contribution and appear sound, but the runtime-adaptability claim rests on a flawed proof that needs fixing before the paper is solid.","tokens_in":23427,"tokens_out":3558,"would_cite":true,"duration_ms":32279,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["91A43","91A50"],"pacs":[],"model":"deepseek-v4-flash","headline":"A single strategy template can encode every winning strategy of an energy game and every finite-memory winning strategy of a mean-payoff game.","keywords":["quantitative strategy templates","energy games","mean-payoff games","permissive strategies","edge-based value iteration","strategy synthesis","mixed objectives","reactive synthesis"],"falsifier":"A concrete counterexample to Proposition 3 would settle the issue: take a small weighted game, delete a set of Player-0 edges that leaves at least one minimum-activation edge at every node, and recompute the edge-optimal value function from scratch; if any value changes, the hot-starting guarantee and the runtime-adaptability claim fail for that instance.","tokens_in":22328,"feed_emoji":"🤖","tokens_out":5634,"duration_ms":53476,"temperature":0.7,"pith_summary":"The paper establishes that a single data structure called a Quantitative Strategy Template (QaSTel) can represent, at once, all winning strategies of an energy game and all finite-memory winning strategies of a mean-payoff game. The template records, for each node and each current energy credit, every outgoing edge that can safely be taken, so a controller can switch between moves at runtime without losing the winning guarantee. The authors give an edge-based value iteration algorithm that computes an optimal template, prove that it is winning and permissive, and show how to combine it with qualitative strategy templates for mixed quantitative-qualitative objectives. They argue that this makes quantitative game solving more robust to disturbances and more amenable to incremental synthesis when new objectives arrive after the fact.","feed_headline":"One template captures every winning move in an energy game","feed_subtitle":"Controllers can swap moves at runtime and absorb new objectives without recomputing a strategy from scratch.","key_machinery":"The load-bearing mechanism is edge-based value iteration. The standard vertex value iteration operator is extended from functions over nodes to functions over edges: for $e=(u,v)$, the operator takes the minimum or maximum over successor edges of $\\mu(e')\\ominus w(e)$, depending on which player controls $v$. Its least fixed point is the edge-optimal value function $\\mathrm{opt}_E$, from which the optimal QaSTel is read off by activating exactly the edges with value at most the current credit. The same fixed point yields the winning region, and its monotonicity is what makes hot-starting template recomputation possible after edge deletions.","core_discovery":"The central discovery is that the optimal initial credit of a node can be refined into an edge-optimal value function $\\mathrm{opt}_E(e)$, the least credit needed to take edge $e$ and still win from its source. The QaSTel defined by $\\Pi(u,c)=\\{e\\in E(u)\\mid c\\ge \\mathrm{opt}_E(e)\\}$ is winning, and it is maximally permissive for energy games (every winning strategy follows it) and $f$-maximally permissive for mean-payoff games (every finite-memory winning strategy follows it). The proof works because any play that follows the template keeps the credit nonnegative, while any winning strategy can only use edges whose edge-optimal value is no larger than the current credit.","pith_inferences":["If the runtime-adaptability guarantee holds, the template itself becomes a compact robustness certificate: the fraction of minimum-activation edges that can be deleted before a recomputation is forced gives a quantitative measure of how fault-tolerant a synthesized controller is.","The same edge-activation scheme should transfer to other quantitative objectives that admit a value iteration algorithm, such as discounted-sum or shortest-path-like objectives, provided an analogous edge-optimal value function can be defined.","Because the mixed-template construction under-approximates the winning region in general, a practitioner should run a completeness check before relying on a MiSTel; the paper's experiments suggest incompleteness appears mainly after several conflict-resolution rounds.","A directly testable extension is to run the online preference strategy on a physical robot with a battery constraint and measure how often blocked edges force a template recomputation, comparing the measured frequency with the paper's simulated deletion rates."],"forward_implications":["An optimal QaSTel for an energy or mean-payoff game is computable in $O(|V||E|W)$ time, matching the complexity of standard value iteration while delivering many viable strategies rather than a single one.","Any runtime choice of an active edge, for example driven by dynamic preferences such as obstacle avoidance or actuator failures, preserves the winning guarantee as long as every node retains at least one minimum-activation edge, per Proposition 3.","For several mean-payoff objectives, the algorithm CombineQaSTel returns a single winning strategy for their conjunction in $O(k|V||E|W)$ time, supporting incremental arrival of quantitative objectives.","For mixed games with a quantitative objective and a qualitative objective such as mean-payoff co-Büchi, computeMiSTel iteratively resolves conflicts between the QaSTel and a bounded PeSTel, and on the paper's benchmarks it recovers the full winning region for over 90% of the instances."],"supporting_citations":[{"why":"Introduces permissive strategy templates (PeSTels) for parity games, the qualitative concept that QaSTels extend.","marker":"[2]"},{"why":"Defines energy games and grounds the energy-objective model used throughout the paper.","marker":"[7]"},{"why":"Supplies the value-iteration algorithm for energy games and the equivalence between mean-payoff and energy objectives used in the permissiveness proofs.","marker":"[9]"},{"why":"Provides the multi-mean-payoff combination lemma and the observation that conjunctive objectives may require infinite-memory strategies.","marker":"[27]"},{"why":"Defines mean-payoff co-Büchi games and gives the MPCoBuechi algorithm used as the experimental baseline.","marker":"[11]"},{"why":"Gives the polynomial translation from parity objectives to mean-payoff objectives that underlies the mixed-template discussion.","marker":"[14]"},{"why":"Provides the SYNTCOMP benchmark suite from which the paper derives its 245 test instances.","marker":"[19]"},{"why":"Supplies the concrete technique for translating SYNTCOMP parity games into mean-payoff games in the benchmark construction.","marker":"[21]"}],"fun_headline_variants":["One template packs all winning moves in quantitative games","Maximally permissive strategies from edge-optimal templates","One template, infinite winning strategies","Compose objectives incrementally with QaSTels","Runtime-adaptable strategies without recomputation"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The runtime-adaptability claim rests on Proposition 3, which says the original template remains optimal after deleting edges as long as every node keeps at least one minimum-activation edge; the proposition is stated without proof in the appendix and its written condition is tautological, so this is the point where the practical robustness story could collapse.","fun_headline_variants_meta":{"raw":{"variants":["One template packs all winning moves in quantitative games","Maximally permissive strategies from edge-optimal templates","One template, infinite winning strategies","Compose objectives incrementally with QaSTels","Runtime-adaptable strategies without recomputation"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001065,"raw_usage":{"total_tokens":4430,"prompt_tokens":876,"completion_tokens":3554,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":492,"completion_tokens_details":{"reasoning_tokens":3484}},"tokens_in":492,"tokens_out":3554,"duration_ms":22850,"temperature":1.0,"reasoning_tokens":3484,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T11:01:30.039702+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"A concrete counterexample to Proposition 3 would settle the issue: take a small weighted game, delete a set of Player-0 edges that leaves at least one minimum-activation edge at every node, and recompute the edge-optimal value function from scratch; if any value changes, the hot-starting guarantee and the runtime-adaptability claim fail for that instance.","supporting_citations":[{"cited_title":"In: Cassez, F., Jard, C","cited_arxiv_id":null,"evidence_quote":"Defines energy games and grounds the energy-objective model used throughout the paper."},{"cited_title":"In: Larsen, K.G., Bodlaender, H.L., Raskin, J","cited_arxiv_id":null,"evidence_quote":"Defines mean-payoff co-Büchi games and gives the MPCoBuechi algorithm used as the experimental baseline."},{"cited_title":"https://doi.org/10.5281/zenodo.8112518","cited_arxiv_id":null,"evidence_quote":"Provides the SYNTCOMP benchmark suite from which the paper derives its 245 test instances."},{"cited_title":"In: Artho, C., Legay, A., Peled, D","cited_arxiv_id":null,"evidence_quote":"Supplies the concrete technique for translating SYNTCOMP parity games into mean-payoff games in the benchmark construction."}],"review_version":1}