{"id":"42a337ed-17dd-4054-8f0a-91b33c35f4bf","arxiv_id":"2412.16793","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Theorem 1: for a guidable automaton A, L(A) is J-feasible iff some bound N makes the parity transduction game T^N_J coincide with the acceptance game of A on every tree.","lead":"An informal note defines \"parity transduction games\" and proves that the Mostowski index of a guidable tree automaton is characterized by whether Eve wins these games with some counter bound. It offers a simplified, game-based reformulation of a key reduction in the open Mostowski index problem.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 5's register strategy is not rigorously established: the assertion that r_j* equals i* at B's maximal priority events is unjustified, and the counter-overflow argument depending on Lemma 3 is only sketched, leaving the forward direction of Theorem 1 unsupported.","rationale":"The reader's weakest_assumption identifies Lemma 3 as the load-bearing step, and Lemma 3 is indeed where the pumping argument is sketched. However, the more immediate gap in the paper is Lemma 5's application of Lemma 3: the proof asserts an alignment between the maxima of A and B runs that is not justified, and then relies on an unformalized counter-overflow invariant. If that invariant can be established, the forward direction likely goes through; if not, the proof is incomplete. The theorem itself is plausible and consistent with the known Colcombet-Loding reduction, so I do not see grounds for rejection, only for requiring a rigorous proof of the missing invariant. Thus the reader's CONDITIONAL verdict remains appropriate. My concern is a proof-completeness issue, not an internal inconsistency or a disagreement with the community consensus.","tokens_in":9190,"tokens_out":25679,"duration_ms":231143,"concrete_test":"Formalize Lemma 5's proof, specifically the invariant that if the counter c_{i,2j*} is not reset between two consecutive occurrences of B-priority 2j* along a branch, then the A-segment between those occurrences has greatest priority i odd, contradicting Lemma 3. Alternatively, exhaustively enumerate all guidable automata A and B with at most 3 states over a binary alphabet, with L(A)=L(B) and A guided by B, and check whether the described register strategy wins T^N_J(ρA) for N=|A||B|+1 on every accepting guided run. A single counterexample would falsify the proof as written; a successful formal verification would remove the concern.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The forward direction of Theorem 1 rests on Lemma 5. The proof describes Eve's strategy and then claims: 'infinitely often, r_j* = i* when the register j* is picked.' This equality does not follow from the assumptions: from limsup of B along a branch being 2j* and limsup of A being i*, one cannot conclude that A has priority i* at the same positions where B has priority 2j*. The register r_j* is set to the A-priority at the moment the register is chosen, so if A's maximal priority occurs at B-positions below 2j*, the register may never equal i*. The subsequent counter argument is the actual load-bearing step: even if r_j* is odd at B=2j* positions, the output is still 2j* with a counter increment, and Eve must be shown not to overflow the counter c_{i,2j*}. The proof dismisses overflow by a pumping/pigeonhole argument whose invariant is only stated informally: a counter overflow would yield a pumpable segment dominated by an odd priority in A and by an even 2j* in B, contradicting Lemma 3. This invariant is not derived rigorously, and Lemma 3 itself is only sketched. If this step fails, the theorem's forward implication does not hold as proved.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces \"parity transduction games\" T^N_J, which extend Lehtinen's register games from her quasipolynomial-time algorithm for parity games by adding bounded counters. The main result (Theorem 1) states that for a guidable nondeterministic parity tree automaton A, the language L(A) is J-feasible (i.e., recognized by some nondeterministic parity tree automaton with priorities in the index J) if and only if there exists a natural number N such that for every Σ-tree t, t is in L(A) exactly when Eve wins the parity transduction game T^N_J played on the acceptance game G(A,t). The forward direction uses the guidability of A: given an accepting run of a hypothetical J-automaton B for L(A), a guided run of A is obtained, and Eve's register strategy in the transduction game is based on the priorities of that guiding run; a pumping argument is invoked to show that the counters never overflow. The backward direction encodes the finite-state configuration space of the transduction game into a nondeterministic J-automaton and composes it with A. The paper is explicitly labeled an informal note, and all proofs are presented as sketches.","tokens_in":9435,"tokens_out":25696,"duration_ms":212799,"significance":"If correct, the main theorem provides a new game-based characterization of the Mostowski (parity) index problem, which is a long-standing open problem. The use of guidable automata is well motivated: they are fully expressive for regular tree languages, so the characterization applies to the general index problem. The connection between Lehtinen's register games and the Colcombet-Löding distance-parity automaton reduction is conceptually attractive, and the paper's approach has the potential to yield a more accessible proof of this important reduction. The paper also benefits from grounding the proof in an existing, well-studied game framework (Lehtinen's register games) and from explicitly identifying guidability as the key automaton-theoretic condition. At the same time, the significance is currently limited by the informal, sketch-level presentation: the soundness of the central construction is plausible but not yet established at the standard of rigor expected for a journal publication.","major_comments":[{"comment":"The claim \"infinitely often, rj∗ = i∗ when the register j∗ is picked\" is not justified by the text. The equality does not follow immediately from the fact that i* and 2j* are the respective limsup priorities along the branch: the runs ρA and ρB are not aligned, and the register r_j* can be reset to a lower value each time j* is picked. A rigorous proof would need to argue that every occurrence of an A-priority equal to i* (after the cutoff point) sets r_j* to i*, because at such a step the register chosen by the strategy has index at most j*, and the update rule raises all higher-index registers to max(i*, ·); since r_j* can only decrease when j* itself is picked, infinitely many j* picks must occur after an A-i* event and therefore see r_j* = i*. As written, this load-bearing claim is unsupported.","section":"Lemma 5, Section 3"},{"comment":"The counter-overflow argument is only sketched. To prove that no counter c_{i,2j*} overflows, the text asserts that an overflow would yield a pumpable segment whose A-maximum is odd i and whose B-maximum is even 2j*, contradicting Lemma 3. However, the construction of this segment is not made precise: one must specify the sequence of N+1 occurrences of the pair (A-priority i, B-priority 2j*), apply the pigeonhole principle with N > |A×B| to obtain repeated state pairs, and then verify that the segment between the repeated positions indeed has no priority larger than i in A and no priority larger than 2j* in B, so that Lemma 3 applies. This step is essential because it is the only mechanism that rules out infinitely many outputs 2j*+1, and without it the output sequence could have an odd limsup.","section":"Lemma 5, Section 3 (counter-overflow argument)"},{"comment":"The proof of Lemma 3 is a sketch. The construction of t*, ρ*A and ρ*B should be formalized: the recursive replacement of subtrees needs a precise definition, and one must prove that ρ*A is exactly the run of A guided by ρ*B (i.e., ρ*A = g(ρ*B)). The argument that every branch of ρ*B is accepting is compressed into a single sentence; in particular, the branches of the form u·v^k·w with w ≠ v^ω require a careful justification that their suffixes are clones of accepting branches of ρB. Since Lemma 5 relies on Lemma 3 for the pumping argument, this lemma must have a complete proof.","section":"Lemma 3, Section 2.3"},{"comment":"The definition of the parity transduction game T^N_J contains ambiguities that affect the automaton construction in Lemma 6. The update rule \"∀j′ < j, crj ,j ′ := 0\" is unclear; the second index should presumably refer to the counter associated with the current value i (e.g., c_{i,j′}), not to r_j. The order between the output step and the register/counter updates is also not fully specified. Since the states of the automaton C in Lemma 6 are the configurations of T^N_J, a rigorous treatment of the game is necessary for the backward direction to be verifiable.","section":"Section 3, definition of T^N_J"}],"minor_comments":[{"comment":"The abstract contains several typos: \"based on on the games\" should be \"based on the games\", \"automaton\" should be \"automaton\", and \"interger\" should be \"integer\".","section":"Abstract / Section 1"},{"comment":"In the definition of a strategy for Eve, the phrase \"if ρ|n ends in a vertex v ∈ VE, σ(ρ|n) follows an edge from v\" should explicitly state that σ is defined on finite plays ending in Eve vertices; the current wording is slightly ambiguous.","section":"Section 2.1"},{"comment":"The line \"ρA(u) = ρB(u) = ρA(u·v) = ρB(u·v)\" is a typo: it should read ρA(u) = ρA(u·v) and ρB(u) = ρB(u·v), since ρA and ρB take values in different state sets.","section":"Lemma 3, Section 2.3"},{"comment":"The text says \"T N k outputs a 2j∗\" where the subscript \"k\" is undefined; it should be \"T^N_J\". Also, \"looses\" should be \"loses\".","section":"Lemma 5, Section 3"},{"comment":"The statement of Theorem 1 uses \"n\" for the bound in the existential quantifier, while the rest of the paper uses \"N\"; this inconsistent notation should be harmonized.","section":"Theorem 1, Section 3"},{"comment":"In the proof of Lemma 4, the phrase \"the game only outputs min(I)\" when j*=0 should refer to the output of the register r0, which is 1 if it exists; the notation ρ(p) is also used without definition (it should likely be L(e) or the priority of the current position).","section":"Lemma 4, Section 3"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is explicitly presented as an informal note, and the proof of the main theorem is a sequence of sketches. The core idea — using Lehtinen's register games with counters to characterize the Mostowski index for guidable automata — is promising and appears to be mathematically sound, but the current level of rigor is not sufficient for a journal publication. The major issues are all fixable within the scope of the manuscript: they require expanding the proofs of Lemmas 3, 4, 5, and 6, clarifying the definition of the transduction game, and removing the many typographical errors. I therefore recommend a major revision rather than rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe paper is an informal note giving a game-based characterization of the Mostowski index for guidable tree automata, extending Lehtinen's register games with counters. The main theorem says J-feasibility of L(A) for guidable A is equivalent to the existence of N such that the parity transduction game T^N_J on G(A,t) captures membership. That statement is new, and it offers a simpler-looking route to the Colcombet-Löding reduction. The authors are upfront that it's informal, which is honest.\n\nWhat's genuinely good: the parity transduction game is a natural extension, the counter mechanism is neat, and the backward direction (Lemma 6) is plausible—encode configurations into a finite automaton, compose with A, use determinacy. It's sketched but standard and likely fixable. Lemma 4, Adam winning on non-even graphs, is essentially correct.\n\nThe soft spot is the forward direction, Lemma 5. The strategy is to pick register j when the guiding B-run has priority in [2j,2j+1]. The proof then asserts that infinitely often r_j* = i* when j* is picked, where 2j* is B's maximal recurrent priority and i* is A's. That equality does not follow. The register r_j* is updated to the A-priority at the moment it's chosen, so it equals i* only if A's i* occurs at the same positions where B has priority 2j* (or 2j*+1). Guidability gives global acceptance preservation, not local alignment of maxima. The stress-test note is right to flag this. The counter-overflow argument that follows is meant to handle the case where r_j* is odd, but it rests on an invariant about pumpable segments that is only asserted, not derived. Lemma 3 itself is proved in a paragraph and seems okay, but the forward implication as written is unsupported.\n\nThis is a real gap, but it may be repairable. The claimed equivalence is plausible, and the machinery is close to existing work. I'd like to see a full version with rigorous proofs, especially for the register/counter invariant. The citation pattern is fine: self-citation to Lehtinen's game is appropriate, and Colcombet-Löding gets credit.\n\nWho is it for? People working on the Mostowski index or game-based reductions. I'd bring it to a reading group and encourage the authors to write it up properly. I wouldn't cite it in my own work until the proof is solid.\n\nRecommendation: send to review, but expect heavy revision; the current form should not be accepted. It deserves referee time because the idea is new and the area is important.","headline":"Promising game-based characterization of the Mostowski index, but the forward direction's key lemma has a real gap and the proof is only a sketch; worth referee time, not acceptance as is.","tokens_in":9969,"tokens_out":4754,"would_cite":false,"duration_ms":42090,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03D05","68Q45"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper claims that for guidable tree automata, a language is recognizable with a given priority index exactly when a single uniform counter bound makes Eve's win in an extended register game coincide with membership in the language.","keywords":["Mostowski index","parity index problem","tree automata","register games","parity transduction games","guidable automata","parity games","nondeterministic parity tree automata"],"falsifier":"Exhibit an automaton $B$ guiding an automaton $A$, accepting runs $\\rho_B$ and $\\rho_A$ on some tree, and a pumpable pair of positions $u, uv$ with $\\rho_A(u)=\\rho_A(uv)$ and $\\rho_B(u)=\\rho_B(uv)$, such that the highest priority in $\\rho_B$'s segment from $u$ to $uv$ is even while the highest in $\\rho_A$'s segment is odd; that refutes Lemma 3 and, since Lemma 5 relies on it, invalidates the forward direction of Theorem 1.","tokens_in":8973,"feed_emoji":"🎮","tokens_out":11048,"duration_ms":84610,"temperature":0.7,"pith_summary":"The paper tackles the Mostowski index problem: given a regular tree language, what is the least number of priorities a nondeterministic parity tree automaton needs to recognize it? The authors define parity transduction games, an extension of register games with bounded counters, parameterized by a target index $J$ and a counter bound $N$. They claim that for any guidable automaton $A$ — an automaton that resolves its nondeterminism by reading an accepting run of any equivalent automaton — the language $L(A)$ is $J$-feasible if and only if some uniform $N$ makes Eve's winning in $T^N_J(G(A,t))$ exactly coincide with $t \\in L(A)$ for every tree $t$. If true, this reduces the index question to a uniform finitary parameter of a game, re-deriving the known reduction to distance-parity automata with a simpler proof. The paper is a brief informal note; the forward direction's key pumping lemma is sketched rather than fully proved.","feed_headline":"Bounded-counter register games characterize the Mostowski index","feed_subtitle":"For guidable automata, Eve's win in the game equals tree membership exactly when a uniform counter bound exists.","key_machinery":"The central object is the parity transduction game $T^N_J$, an extension of the register games used in a known quasipolynomial-time parity-game algorithm. Played over a parity game $G = (V,E,L)$ whose edges carry priorities in an index $I$, the game outputs a priority in $J$: at each step Adam picks an edge, Eve picks a register $r_j$ (one per even $2j \\in J$, plus possibly $r_0$), and the outputs are determined by whether the register's stored value is even, with counters $c_{i,j}$ for odd $i$ limiting how often Eve can delay outputting an odd priority. Her goal is that the infinite output sequence is parity accepting. The counter bound $N$ is the uniformity parameter: the theorem says the index problem is equivalent to the existence of a single finite $N$ working for all trees. Guidability drives the forward direction: an accepting run of the hypothetical $J$-automaton determines Eve's register choices, and the pumping lemma ensures no counter can reach $N+1$ on a branch that is even-dominated in the guiding run.","core_discovery":"The central result is Theorem 1: given a guidable automaton $A$ and an index $J$, the language $L(A)$ is $J$-feasible exactly when there exists a natural number $N$ such that for every $\\Sigma$-tree $t$, $t \\in L(A)$ if and only if Eve wins the parity transduction game $T^N_J(G(A,t))$ on the acceptance parity game of $t$ in $A$. The forward direction assumes a $J$-automaton $B$ recognizing $L(A)$ and lets $B$ guide Eve: her register choices follow $B$'s priorities, and a pumping argument (Lemma 3) shows that the counters can never overflow, because an overflow would produce a pumpable segment where $B$'s run is even-dominated but $A$'s run is odd-dominated, contradicting guidability. The backward direction encodes the configurations of $T^N_J$ as states of a finite automaton and composes it with $A$ to obtain an automaton of index $J$ recognizing the same language. Since every regular tree language is recognized by some guidable automaton, a fact the paper recalls, the characterization covers all regular tree languages.","pith_inferences":["A natural testable extension is to ask whether the bound $N = |A||B|+1$ can be turned into an effective procedure: if a candidate $J$-automaton $B$ and a bound are given, the construction of Lemma 6 yields the equivalent $J$-automaton, which could support a search algorithm for $J$-feasibility over guidable automata.","The counter structure suggests a quantitative measure of the 'distance' between a language's true index and a proposed index $J$: the minimal $N$ needed (if any) behaves like a budget of tolerated odd dominations, which may give finer information than the bare index and could be compared directly against distance costs in distance-parity automata.","If Lemma 3 were formalized and made constructive, it would yield an algorithm for synthesizing Eve's winning register strategy from the guiding run, potentially simplifying the practical computation of winning strategies in these games.","One could investigate whether the same game characterization extends to non-guidable automata, or whether the failure of local preservation of even domination is exactly the obstruction; the paper's theorem does not address non-guidable automata."],"forward_implications":["If $L(A)$ is $J$-feasible, the witness automaton $B$ of size $|B|$ gives a concrete bound $N = |A||B| + 1$ for which Eve can win $T^N_J$ on every accepted tree, so the existential bound in Theorem 1 is instantiated by a product of the two automata sizes.","Conversely, whenever such a uniform $N$ exists, the paper constructs a genuine $J$-automaton by composing $A$ with a finite-state automaton whose states are the configurations of the transduction game; this yields $J$-feasibility.","The games are parity games, hence determined, so for each tree $t$ and each $N$ exactly one of Eve or Adam wins $T^N_J(G(A,t))$; this makes the characterization two-sided rather than a one-way containment.","Because every regular tree language is recognized by a guidable automaton, the equivalence is not restricted to a special subclass: it holds for all regular tree languages.","As the paper notes, encoding the counters into the distance of a distance-parity automaton recovers the shape of the established reduction to distance-parity automata, connecting the two approaches."],"supporting_citations":[{"why":"Introduces guidable automata and the distance-parity automaton reduction, provides the full-expressivity theorem that every regular tree language has a guidable automaton, and is the result whose proof is here simplified.","marker":"[2]"},{"why":"Source of the register-game mechanism that the paper extends with counters to define parity transduction games.","marker":"[4]"},{"why":"Borel determinacy, invoked so that parity games and the transduction games over them are determined.","marker":"[6]"},{"why":"Gives the equivalence used in the definition of guidable automata, allowing guidance from any automaton whose language is contained in that of A.","marker":"[5]"}],"fun_headline_variants":["Bounded counters decide Mostowski feasibility","Mostowski index reduces to bounded-counter games","Register games with bounded counters capture index","Parity transduction games characterize Mostowski index","Simpler proof: Mostowski index via bounded games"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The main theorem's forward direction rests on the lemma that whenever a repeating segment of the guiding run is dominated by an even priority, the corresponding segment of the guided run is even too, and this lemma is only sketched in the paper.","fun_headline_variants_meta":{"raw":{"variants":["Bounded counters decide Mostowski feasibility","Mostowski index reduces to bounded-counter games","Register games with bounded counters capture index","Parity transduction games characterize Mostowski index","Simpler proof: Mostowski index via bounded games"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000223,"raw_usage":{"total_tokens":1494,"prompt_tokens":1016,"completion_tokens":478,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":632,"completion_tokens_details":{"reasoning_tokens":412}},"tokens_in":632,"tokens_out":478,"duration_ms":4395,"temperature":1.0,"reasoning_tokens":412,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T10:16:25.517716+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Exhibit an automaton $B$ guiding an automaton $A$, accepting runs $\\rho_B$ and $\\rho_A$ on some tree, and a pumpable pair of positions $u, uv$ with $\\rho_A(u)=\\rho_A(uv)$ and $\\rho_B(u)=\\rho_B(uv)$, such that the highest priority in $\\rho_B$'s segment from $u$ to $uv$ is even while the highest in $\\rho_A$'s segment is odd; that refutes Lemma 3 and, since Lemma 5 relies on it, invalidates the forward direction of Theorem 1.","supporting_citations":[{"cited_title":"The non-determin istic mostowski hierarchy and distance-parity automata","cited_arxiv_id":null,"evidence_quote":"Introduces guidable automata and the distance-parity automaton reduction, provides the full-expressivity theorem that every regular tree language has a guidable automaton, and is the result whose proof is here simplified."},{"cited_title":"A modal mu perspective on solving pa rity games in quasi-polynomial time","cited_arxiv_id":null,"evidence_quote":"Source of the register-game mechanism that the paper extends with counters to define parity transduction games."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Borel determinacy, invoked so that parity games and the transduction games over them are determined."},{"cited_title":"Logic and automata over infinite trees","cited_arxiv_id":null,"evidence_quote":"Gives the equivalence used in the definition of guidable automata, allowing guidance from any automaton whose language is contained in that of A."}],"review_version":1}