{"id":"28b2e6df-c04e-4938-bf95-58f3d94ff301","arxiv_id":"1908.04625","paper_version":2,"verdict":"REJECT","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"For nondeterministic weighted automata over Markov chains, exact expected value and distribution can be irrational or uncomputable, but both can be approximated in exponential time in the automaton and polynomial time in the Markov chain and precision.","lead":"This paper studies nondeterministic weighted automata whose input words are generated at random by a Markov chain, and asks how to compute the expected value and cumulative distribution of the automaton's numeric output. It presents approximation algorithms with exponential-time complexity in the automaton and polynomial-time complexity in the Markov chain and precision, plus an approximate determinisation result.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 22's permanent/transitory dichotomy rests on a false reachability implication: absence of a run eventually staying in an SCC does not imply the reachable set \\hat{\\delta}(A\\setminus S_j,u) becomes empty. The main approximation theorem is unproved.","rationale":"The paper's strongest positive contribution would be Theorem 22; the proof's SCC classification is the load-bearing step. My concern is not disagreement with the consensus but an internal proof gap: the text explicitly asserts an implication that fails on a simple automaton. The mechanism is not a subtle measure-theoretic edge case; it is a reachability property. Since the only supporting argument for \"transitory\" is the false emptiness claim, the algorithm's correctness is unsupported. I checked whether the dichotomy could be salvaged: the permanent/transitory dichotomy itself may be provable from Markov-chain tail triviality, and the counterexample does not refute the theorem, only the proof. But the preprint does not give such an argument, and the text's own Figure 3 shows the authors were aware that reachability of an SCC does not imply almost-sure eventual residence. I also note the independent issue in Theorems 6/7: limit-average over $-separated blocks is length-weighted, so the SLLN statement used there computes the wrong quantity unless the per-block averages are uncorrelated with block lengths, which is not shown. Both issues affect the abstract's central claims; the Sum-automaton #P results and the measurable/block-deterministic framework remain potentially valuable, and the flaws may be repairable, so a revised version could change the verdict.","tokens_in":26947,"tokens_out":14404,"duration_ms":161631,"concrete_test":"Implement the four-state counterexample above: Q={r,s,t}, Q0={r}, transitions r--a-->r, r--a-->s, s--a-->t, t--a-->t, S_j={s}, Markov chain emitting a^ω. Compute \\hat{\\delta}(Q0,a^n) and \\hat{\\delta}({r,t},a^m). For all n≥1, s∈\\hat{\\delta}(Q0,a^n), while for all m≥0, \\hat{\\delta}({r,t},a^m) contains r (and t for m≥1); hence the implication used in Theorem 22 is false. Then, to assess repairability, re-run the proof of Theorem 22 with an ergodic tail argument for the dichotomy and verify that, for almost every word, L_A(w) is the minimum over runs eventually staying in permanent SCCs; if that verification succeeds, the approximation algorithm may survive despite the false intermediate claim.","verdict_should_be":"REJECT","load_bearing_attack":"The main claim is Theorem 22(2): exponential-time approximation of E_M(A) and D_{M,A}(λ) for nondeterministic LimAvg automata. The proof partitions each BSCC of M×A_D and every SCC S_j of A into permanent or transitory. The dichotomy is justified by: if S_j is not permanent, take an infinite path ρ visiting (s,A) whose word has no run eventually staying in S_j; then, for the suffix u after that visit, \"we observe that \\hat{\\delta}(A\\setminus S_j,u)=∅\". This observation is false. A run can leave S_j and never return while different runs enter S_j at arbitrarily late times, so S_j is reachable at every position although no run eventually stays in it. Concretely, over alphabet {a}, take states r (initial) with r--a-->r and r--a-->s, s--a-->t, t--a-->t, with S_j={s}. On a^ω the reachable set after every nonempty prefix contains s; yet every run that ever enters s immediately moves to t and never returns, and the run staying in r never visits s. Thus no run eventually stays in S_j, while \\hat{\\delta}({r,t},a^m)={r,t}≠∅ for every suffix. The proof's subsequent step—that a finite prefix u' makes \\hat{\\delta}(A\\setminus S_j,u')=∅ with positive probability—also fails in this example. Because the algorithm then evaluates only runs that eventually stay in \"permanent\" SCCs and takes their minimum over SCCs, the claimed computation of E_M(A|H_i), and therefore Theorem 22(2) and Theorem 24, are not established as written. A separate, independent gap in Theorems 6/7 replaces the length-weighted long-run average over $-blocks by the unweighted Cesàro average of per-block averages; that identity also does not follow from the SLLN.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper studies non-deterministic weighted automata (Sum and LimAvg semantics) evaluated on words generated by Markov chains. The value L_A(w) is the infimum over accepting runs, which makes L_A a random variable. The authors prove that exact expected value and distribution can be irrational/transcendental and are uncomputable in any effective representation (Theorems 6 and 7), that the approximate distribution/expected value problems are #P-complete for total Sum-automata (Theorem 10), PSpace-hard for LimAvg automata (Theorem 11), and that for LimAvg automata the approximate problems can be solved in exponential time in |A| and polynomial time in |M| and 1/epsilon (Theorem 22). The paper concludes with an approximate determinisation result for LimAvg automata with respect to the standard deviation metric (Theorem 24). The technical core is a two-stage approximation: for recurrent automata, optimal \"k-jumping runs\" with bounded look-ahead are shown to approximate the true value for almost all words, and the resulting finite-block Markov chains are approximated by a clusterization method; the general case is reduced to recurrent components by a permanent/transitory classification of SCCs.","tokens_in":27235,"tokens_out":23264,"duration_ms":222648,"significance":"If the main results hold, Theorem 22 would be the first feasible average-case analysis for non-deterministic weighted automata with limit-average semantics, and Theorem 24 would provide approximate determinisation under a probabilistic metric. The paper also contains genuinely interesting ideas: the use of Roth's theorem to exhibit transcendental values, the #P-completeness reduction for Sum automata, and the jumping-run/saturation technique for recurrent automata. The paper is explicit about measurability and about why the product construction for deterministic automata does not extend to nondeterministic ones. However, as I detail below, several load-bearing proof steps are currently incorrect or incomplete, so the manuscript is not publishable in its present form.","major_comments":[{"comment":"The permanent/transitory dichotomy is not established. The proof argues that if an SCC S_j is not permanent, then for a path rho visiting (s,A) whose word has no run eventually staying in S_j, the suffix u satisfies \\hat{\\delta}(A\\setminus S_j,u)=emptyset. This implication is false. Over the alphabet {a}, take states r (initial), s, t with transitions r--a-->r, r--a-->s, s--a-->t and t--a-->t, and set S_j={s}. On the word a^omega, the reachable set of A\\setminus S_j={r,t} after every nonempty prefix is {r,t}, while no run eventually stays in S_j. Hence the subsequent claim that some finite prefix u' of u has \\hat{\\delta}(A\\setminus S_j,u')=emptyset with positive probability also fails. Because the algorithm then evaluates only runs that eventually stay in \"permanent\" SCCs and takes the minimum over them, the computation of E_M(A|H_i), and therefore Theorem 22(2) and Theorem 24, are not established as written.","section":"Section 7, proof of Theorem 22"},{"comment":"The reduction from finite-word Sum automata to infinite-word LimAvg automata by inserting a reset letter $ claims that E(A_infty)=E(A) via an unweighted SLLN over per-block averages. The limit-average value of the composed word is a length-weighted average: if the i-th block has length L_i and average X_i, then LA_infty(w)=lim_s (sum_{i<=s} L_i X_i)/(sum_{i<=s} L_i), which by SLLN converges to E(L X)/E(L), not to E(X)=E(A). For the automaton constructed in Theorem 6, the \"good\" words of the form a#a^4#...#a^{4^n} contribute 0 to the numerator but a positive amount to the denominator, so E(L X)/E(L) differs from E(X). Thus the equality E(A_infty)=E(A) is false, and the uncomputability claim for LimAvg automata in Theorem 7(2) is not supported by the given reduction.","section":"Theorems 6(2) and 7(2)"},{"comment":"The clusterization enumeration does not yield the claimed complexity. If the clusterization functions c_i are indexed by tables f:QxQ->H, the number of tables is |H|^{O(|Q|^2)} with |H|=Theta(|A| k / epsilon); the convolution over all pairs f_1,f_2 takes time (|A| k / epsilon)^{O(|Q|^2)}, which is not polynomial in 1/epsilon with an exponent independent of |A|. If, as written, f is a function Q x Sigma^N x Q -> H, the enumeration is larger still. The proof of Theorem 22(2) depends on the polynomial dependence on 1/epsilon, so this step needs to be clarified or corrected.","section":"Lemma 18 and Lemma 19"}],"minor_comments":[{"comment":"The definition of q_i should read q_i = 3^{l_i+1}, not 3^{-(l_i+1)}; otherwise the denominator is not an integer.","section":"Theorem 6 proof"},{"comment":"The statement says \"let i > 0\" but then uses \"|w|=2^k\"; the variable k appears to be the number of binary levels and should be i, or the statement should be rewritten consistently.","section":"Lemma 18 statement"},{"comment":"The inequality displaying the induction step is missing a '+' sign between the two terms; it should read h(q,w1,q'') - a*epsilon0 <= i*epsilon0 and h(q'',w2,q') - b*epsilon0 <= i*epsilon0, with a sum bounding the average.","section":"Lemma 18 proof"},{"comment":"The definition of H appears to use set difference; it should be the intersection {j*epsilon0 | j in Z} intersect (-|A|,|A|).","section":"Lemma 18, definition of H"},{"comment":"The assumption that M emits every word on which A has an infinite run is introduced informally; it should be stated formally and its preservation under the construction A_R = A_M x A' should be argued, since the proof of Lemma 21 relies on it.","section":"Section 6.4"}],"recommendation":"major_revision","confidential_remarks":"Given the footnote stating that the paper has already been published in JCSS, I note that the proof gaps identified above are present in this arXiv version; if this is the version under consideration, the journal should weigh whether the published claims need correction. The permanent/transitory gap and the SLLN equality are central and should be addressed in any revision."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Jan,\n\nShort version: this is the first real study of nondeterministic weighted automata under probabilistic semantics, and the Sum-automaton results are in decent shape, but the headline theorem for LimAvg automata (Thm 22) has a proof gap that I think is genuine, and the reductions behind the LimAvg uncomputability/transcendence claims (Thms 6 and 7) have a second gap. I wouldn't accept the text as is, but I would send it to a serious referee: the framework and the recurrent-automaton machinery are worth repairing.\n\nWhat is actually new: the paper opens a class that had only been studied deterministically. The #P-completeness for approximating expected value/distribution of total Sum automata looks solid and self-contained. The recurrent automata, k-jumping runs, and block-deterministic approximations are a nice toolbox, and the approximate determinization result with respect to the standard-deviation metric is a genuinely different answer to Boker-Henzinger's negative result on d_sup. Also, the authors are upfront that they corrected claims from the CONCUR version; that's the right way to handle it.\n\nThe soft spots are in the LimAvg part. In Theorem 22, the proof of the permanent/transitory dichotomy relies on: if no run eventually stays in SCC S_j, then for some suffix u the reachable set \\hat{\\delta}(A\\setminus S_j,u) is empty. That implication is false. Take states r (initial) with r--a-->r, r--a-->s, s--a-->t, t--a-->t, and let S_j={s}. On a^\\omega, no run eventually stays in s, but every nonempty prefix still reaches s from {r,t}. So the subsequent step—that a finite prefix with empty reachable set occurs with positive probability—doesn't follow, and the conditional expectation computation over \"permanent\" SCCs is not established. The dichotomy might be true by a different argument; the proof as written doesn't show it.\n\nSecond, in Theorems 6 and 7 the passage from Sum automata to LimAvg automata via reset symbols compares the long-run limit average to an SLLN average of per-block averages. Those are not the same thing when block lengths are random: the limit average is a length-weighted average of block sums, and its limit is E(block sum)/E(block length), not E(block sum/block length). The identity E(A_infty)=E(A) does not follow from the cited SLLN. This affects the transcendence and uncomputability claims for LimAvg.\n\nThese are correctable, not fatal to the whole program. The Sum results and the recurrent-automaton approximation for uniform measures/strongly connected automata survive as far as I can see. Who should read this: anyone working on quantitative verification or weighted automata; the questions and much of the machinery will matter even if these two proofs need rework. Recommendation: accept for peer review, with a request for major revision focusing on Theorem 22 and the block-average reduction. I wouldn't desk-reject it.","headline":"First serious treatment of nondeterministic weighted automata under probabilistic semantics, but the main LimAvg approximation theorem rests on a false reachability claim and the LimAvg uncomputability reductions have a second gap.","tokens_in":27875,"tokens_out":5310,"would_cite":true,"duration_ms":55968,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q45","68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"Nondeterministic weighted automata over Markov chains: exact answers are uncomputable, epsilon-approximations are feasible.","keywords":["weighted automata","Markov chains","probabilistic semantics","limit average","expected value","approximation algorithms","quantitative verification","approximate determinisation"],"falsifier":"One could test this dichotomy directly: build an automaton and a Markov chain where a run leaves a strongly connected component and re-enters it infinitely often on a set of words of positive probability but never remains there forever, and ask whether the reachability test used in Theorem 22 (whether the set of states outside the component can reach the empty set in finitely many steps) still classifies the component as transitory. If the test answers 'transitory' while such words have positive probability, the dichotomy and the approximation theorem would need a weaker substitute.","tokens_in":26612,"feed_emoji":"🎲","tokens_out":9370,"duration_ms":94926,"temperature":0.7,"pith_summary":"This paper asks what a nondeterministic weighted automaton computes when the word it reads is produced randomly by a Markov chain. It establishes that the exact expected value and the exact cumulative distribution of the automaton's value can be irrational, even transcendental, and in general cannot be computed by any effective representation. The main result is an approximation algorithm: for automata with the sum or limit-average value function, both quantities can be epsilon-approximated in exponential time in the automaton and polynomial time in the Markov chain and in 1/epsilon. That makes average-case analysis possible for quantitative specifications that only nondeterministic weighted automata can express, replacing the undecidable 'for every word' question with a feasible 'for almost every word' one.","feed_headline":"Limit-average automata on random words: approximable, not exact","feed_subtitle":"Exponential-time approximation replaces the undecidable 'for all words' question with a feasible 'for almost all words' one.","key_machinery":"The key object is the k-jumping run: a run that is an ordinary automaton run inside each length-k block of the input word but may jump between arbitrary states at block boundaries, paying the minimal automaton weight for the jump. On recurrent automata the optimal k-jumping run is block-deterministic, so the approximation reduces to a weighted Markov chain over subsets of automaton states, whose expected value can be computed by approximating average weights of length-2^i blocks through a length-doubling clusterization (Lemma 18). The remaining gap between a jumping run and a true run is closed by showing that a true run can synchronize with the jumping run once it reads a 'saturating' suffix, which exists and is reached with high probability by Lemma 14. The full theorem decomposes the product of the Markov chain with the determinized automaton into bottom strongly connected components and classifies each automaton SCC as permanent if almost every word has a run eventually staying in it, or transitory otherwise, so the value on almost all words is the minimum over the permanent components.","core_discovery":"The central discovery is that nondeterminism, which makes exact probabilistic semantics ill-behaved, becomes tractable when the probabilistic questions are relaxed to approximation. For limit-average automata the expected value and distribution values can be transcendental and uncomputable (Theorems 6 and 7), yet Theorem 22 gives epsilon-approximations of both in exponential time in the automaton size and polynomial time in the Markov chain size and 1/epsilon. The mechanism is that a random word's value is almost surely determined by the bottom strongly connected component of the product Markov chain that the word eventually falls into, and each such component contributes a single value; those component values can be computed approximately by replacing runs with bounded-look-ahead 'jumping' runs. A corollary (Theorem 24) shows that every limit-average automaton can be approximated by a deterministic one with respect to expected absolute difference, a form of approximate determinization that is impossible for the worst-case distance.","pith_inferences":["If the approximation algorithm scales past the doubly-exponential look-ahead bound on practical inputs, the same block-clusterization idea could become a default statistical model-checking method for quantitative specifications; the authors' own Monte Carlo experiment on the running example hints that the bound is pessimistic.","The permanent/transitory classification, once made rigorous, should transfer to other objectives such as discounted sums or mean-payoff games, where 'almost all plays' is a natural average-case semantics.","A broader moral is that randomness can be a resource for quantitative verification: replacing universal quantification over words by a Markov-chain measure converts undecidable threshold questions into approximable counting questions."],"forward_implications":["For a recurrent limit-average automaton, almost all random words share the same value, so the distribution question reduces to comparing the threshold with the expected value; this is why Theorem 22 can approximate the distribution so cheaply.","Quantitative model checking can now separate 'almost all words satisfy the threshold' from 'almost all words violate it', a computationally attractive stand-in for the undecidable universality problem.","Every nondeterministic limit-average automaton can be epsilon-approximated by a deterministic one in the standard-deviation metric, despite the known impossibility of approximate determinization in the worst-case metric.","The online/offline competitive-ratio analysis can be extended from worst-case to average-case competitiveness.","For sum automata, approximating the expected value and the distribution is #P-complete, locating the problem in the counting hierarchy rather than beyond it."],"supporting_citations":[{"why":"Establishes that limit-average automata cannot be approximately determinised in the worst-case metric; this is the baseline that the standard-deviation result overcomes.","marker":"[9]"},{"why":"Introduces quantitative languages and the value-function semantics for nondeterministic weighted automata used throughout.","marker":"[11]"},{"why":"Studies weighted automata under probabilistic semantics for deterministic automata and shows that the straightforward product construction fails for nondeterministic ones.","marker":"[12]"},{"why":"Earlier conference version whose claims about distribution mass points and PSPACE-hardness are corrected in this paper.","marker":"[27]"},{"why":"Supplies the weighted Markov chain and bottom strongly connected component techniques used to compute expected values.","marker":"[18]"},{"why":"Provides the algorithms for probabilities of omega-regular languages and Markov chain analysis that the lower and upper bounds build on.","marker":"[4]"},{"why":"Supplies the rational-approximation theorem used to prove that exact values can be transcendental.","marker":"[30]"},{"why":"Gives the undecidability of quantitative universality for sum automata, the source of the uncomputability reductions.","marker":"[25, 1]"}],"fun_headline_variants":["From undecidable to approximable: automata on random words","Uncomputable exact answers, but exponential-time approximations exist","Approximating non-deterministic automata over Markov chains in exponential time","Epsilon-approximations for automata on random words despite undecidability"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The proof rests on the claim that a run which never settles into a given strongly connected component must eventually pass a point after which it cannot reach that component again; in principle a run could keep leaving and returning forever, and the argument does not rule this out.","fun_headline_variants_meta":{"raw":{"variants":["From undecidable to approximable: automata on random words","Uncomputable exact answers, but exponential-time approximations exist","Approximating non-deterministic automata over Markov chains in exponential time","Epsilon-approximations for automata on random words despite undecidability"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001416,"raw_usage":{"total_tokens":5679,"prompt_tokens":868,"completion_tokens":4811,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":484,"completion_tokens_details":{"reasoning_tokens":4732}},"tokens_in":484,"tokens_out":4811,"duration_ms":32805,"temperature":1.0,"reasoning_tokens":4732,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T13:39:19.955303+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"One could test this dichotomy directly: build an automaton and a Markov chain where a run leaves a strongly connected component and re-enters it infinitely often on a set of words of positive probability but never remains there forever, and ask whether the reachability test used in Theorem 22 (whether the set of states outside the component can reach the empty set in finitely many steps) still classifies the component as transitory. If the test answers 'transitory' while such words have positive probability, the dichotomy and the approximation theorem would need a weaker substitute.","supporting_citations":[],"review_version":1}