Non-deterministic weighted automata evaluated over Markov chains

Jakub Michaliszyn; Jan Otop

REVIEW 3 major objections 5 minor 12 references

Non-deterministic weighted automata evaluated over Markov chains

T0 review · 3 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Nondeterministic weighted automata over Markov chains: exact answers are uncomputable, epsilon-approximations are feasible.

desk verdict 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. read the letter →

arxiv 1908.04625 v2 pith:CWY64BLU submitted 2019-08-13 cs.FL

Jakub Michaliszyn , Jan Otop This is my paper · ORCID

classification cs.FL MSC 68Q4568Q60

keywords weightedautomataMarkovchainsprobabilisticsemanticslimitaverageexpectedvalueapproximationalgorithmsquantitativeverificationapproximatedeterminisation

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

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.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Jan,

Short 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.

What 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.

The 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.

Second, 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.

These 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.

Referee Report

3 major / 5 minor

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.

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 (3)

[Section 7, proof of Theorem 22] 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.
[Theorems 6(2) and 7(2)] 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.
[Lemma 18 and Lemma 19] 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.

minor comments (5)

[Theorem 6 proof] 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.
[Lemma 18 statement] 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.
[Lemma 18 proof] 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.
[Lemma 18, definition of H] The definition of H appears to use set difference; it should be the intersection {j*epsilon0 | j in Z} intersect (-|A|,|A|).
[Section 6.4] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the derivation chain is self-contained; the identified weaknesses are proof gaps, not circular reductions.

full rationale

The paper's central derivation chain is not circular. Theorem 22 builds on Lemmas 14, 15, 18, 19, 20 and 21: recurrent automata are approximated by block-deterministic k-jumping runs, saturation is proved by a combinatorial pumping argument, and the expected block values are approximated by a clusterization procedure over quantized averages. None of these steps fits a parameter to the target expected value or distribution, and none defines the conclusion into its premises. The irrationality and uncomputability results in Theorems 6 and 7 use standard external facts (Roth's theorem, the strong law of large numbers, and undecidability of quantitative universality) as inputs, not as disguised versions of the target statements. The self-citations are not load-bearing in a circular sense: the paper states that it is an extended and corrected version of [27] and explicitly corrects two claims from that earlier version; [12] supplies prior deterministic-case results and a counterexample, but the main approximation theorem is proved from automata-theoretic and probabilistic reasoning developed in the paper rather than assumed from those citations. The reviewer-identified weaknesses, namely the questionable implication in the permanent/transitory dichotomy of Theorem 22 and the unweighted per-block averaging in the E(A_infty) = E(A) argument of Theorems 6(2) and 7(2), are genuine correctness or proof-gap concerns, but they are not circularity: they do not make the derived quantity equal to an input by construction, and they do not involve fitted parameters renamed as predictions. Accordingly, the circularity score is 0.

Assumptions & free parameters 0 free parameters · 8 assumptions · 0 invented entities

The results rest on standard probability and automata theory. No free parameters are fitted to data. The central technical device (k-jumping runs) is a mathematical construction, not a postulated physical entity. The only ad hoc assumption is the emissions assumption in Section 6.4, which the authors later eliminate.

assumptions (8)

standard math Strong law of large numbers for i.i.d. random variables
Used in Theorems 6 and 7 and Lemma 16 to argue that almost all words have the same value for the reset automaton. The application in the paper appears to use an unweighted average, which is a misapplication; see red flags.
standard math Roth's theorem on rational approximations to algebraic numbers
Used in Theorem 6 to prove transcendence of gamma via infinitely many rational approximations with precision 1/q^3.
standard math Properties of bottom strongly connected components (BSCCs) of finite Markov chains, including almost-sure reachability and absorption
Used in Lemmas 15, 16 and Theorem 22 to decompose the product Markov chain and to argue that almost all paths eventually stay in a single BSCC.
standard math Measurability of analytic sets (projection of Borel sets)
Used in Remark 2 to establish that L_A for a non-deterministic LimAvg automaton is measurable.
standard math König's lemma / finite-branching compactness
Used implicitly in Theorem 22 to derive a finite prefix with empty reachable set from the absence of an infinite run on a fixed word.
domain assumption Undecidability of the quantitative universality problem for weighted automata [1,25]
Used in Theorem 7 as the source of undecidability for reductions to probabilistic questions.
domain assumption Terminating and non-terminating Markov chains have rational transition probabilities when given as algorithmic input
Stated in Section 2.1 as part of the input model for computational problems.
ad hoc to paper In Section 6.4, the assumption that M emits every word on which A has an infinite run
This assumption is used to adapt Lemma 14 to non-uniform measures. The paper then shows how to discharge it by restricting A to the language of M, so it is not a permanent free assumption.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Non-deterministic weighted automata evaluated over Markov chains." pith.science (2026). https://pith.science/paper/CWY64BLU

@misc{pith2026190804625,
  author       = {Pith},
  title        = {Pith review of: Non-deterministic weighted automata evaluated over Markov chains},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CWY64BLU}},
  note         = {Machine review of arXiv:1908.04625}
}

read the original abstract

We present the first study of non-deterministic weighted automata under probabilistic semantics. In this semantics words are random events, generated by a Markov chain, and functions computed by weighted automata are random variables. We consider the probabilistic questions of computing the expected value and the cumulative distribution for such random variables. The exact answers to the probabilistic questions for non-deterministic automata can be irrational and are uncomputable in general. To overcome this limitation, we propose approximation algorithms for the probabilistic questions, which work in exponential time in the size of the automaton and polynomial time in the size of the Markov chain and the given precision. We apply this result to show that non-deterministic automata can be effectively determinised with respect to the standard deviation metric.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

12 extracted references · 12 canonical work pages

[6]

Strategy synthesis for multi-dimensional quantitative objectives

13 Krishnendu Chatterjee, Mickael Randour, and Jean-François Raskin. Strategy synthesis for multi-dimensional quantitative objectives. InCONCUR 2012, pages 115–131,

work page 2012
[7]

Predicate abstraction and reﬁnement for verifying multi-threaded programs

20 Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Predicate abstraction and reﬁnement for verifying multi-threaded programs. InPOPL 2011, pages 331–344,

work page 2011
[1979]

Convex language semantics for nondeterministic probabilistic automata

32 Gerco van Heerdt, Justin Hsu, Joël Ouaknine, and Alexandra Silva. Convex language semantics for nondeterministic probabilistic automata. InICTAC 2018, pages 472–492,

work page 2018
[2003]

Percentile queries in multi- dimensional markov decision processes

29 Mickael Randour, Jean-François Raskin, and Ocan Sankur. Percentile queries in multi- dimensional markov decision processes. InCA V 2015, pages 123–139,

work page 2015
[2006]

Non-deterministic weighted automata on random words

27 Jakub Michaliszyn and Jan Otop. Non-deterministic weighted automata on random words. In CONCUR 2018, pages 10:1–10:16,

work page 2018
[2008]

Markov chains and unambiguous büchi automata

5 Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klüppelholz, David Müller, and James Worrell. Markov chains and unambiguous büchi automata. InCA V 2016, pages 23–42. Springer,

work page 2016
[2010]

Henzinger, and Jan Otop

12 Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Quantitative automata under probabilistic semantics. InLICS 2016, pages 76–85. ACM,

work page 2016
[2012]

Henzinger

10 Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. A survey of stochastic games with limsup and liminf objectives. InICALP 2009, pages 1–15,

work page 2009

Show all 12 references

[2013]

Henzinger

9 Udi Boker and Thomas A. Henzinger. Approximate determinization of quantitative automata. In FSTTCS 2012, pages 362–373. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik,

2012
[2016]

Regular repair of speciﬁcations

6 Michael Benedikt, Gabriele Puppis, and Cristian Riveros. Regular repair of speciﬁcations. In LICS 2011, pages 335–344,

2011
[2017]

Kwiatkowska, Gethin Norman, and David Parker

22 Andrew Hinton, Marta Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM: A tool for automatic veriﬁcation of probabilistic systems. InTACAS 2006, pages 441–444,

2006
[2018]

33 Moshe Y. Vardi. Automatic veriﬁcation of probabilistic concurrent ﬁnite-state programs. In FOCS 1985, pages 327–338. IEEE Computer Society, 1985

1985

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [6]

Strategy synthesis for multi-dimensional quantitative objectives

13 Krishnendu Chatterjee, Mickael Randour, and Jean-François Raskin. Strategy synthesis for multi-dimensional quantitative objectives. InCONCUR 2012, pages 115–131,

work page 2012

[2] [7]

Predicate abstraction and reﬁnement for verifying multi-threaded programs

20 Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Predicate abstraction and reﬁnement for verifying multi-threaded programs. InPOPL 2011, pages 331–344,

work page 2011

[3] [1979]

Convex language semantics for nondeterministic probabilistic automata

32 Gerco van Heerdt, Justin Hsu, Joël Ouaknine, and Alexandra Silva. Convex language semantics for nondeterministic probabilistic automata. InICTAC 2018, pages 472–492,

work page 2018

[4] [2003]

Percentile queries in multi- dimensional markov decision processes

29 Mickael Randour, Jean-François Raskin, and Ocan Sankur. Percentile queries in multi- dimensional markov decision processes. InCA V 2015, pages 123–139,

work page 2015

[5] [2006]

Non-deterministic weighted automata on random words

27 Jakub Michaliszyn and Jan Otop. Non-deterministic weighted automata on random words. In CONCUR 2018, pages 10:1–10:16,

work page 2018

[6] [2008]

Markov chains and unambiguous büchi automata

5 Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klüppelholz, David Müller, and James Worrell. Markov chains and unambiguous büchi automata. InCA V 2016, pages 23–42. Springer,

work page 2016

[7] [2010]

Henzinger, and Jan Otop

12 Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Quantitative automata under probabilistic semantics. InLICS 2016, pages 76–85. ACM,

work page 2016

[8] [2012]

Henzinger

10 Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. A survey of stochastic games with limsup and liminf objectives. InICALP 2009, pages 1–15,

work page 2009