A Complexity Bound for Determinisation of Min-Plus Weighted Automata

Guy Arbel; Sarai Sheinvald; Shaull Almagor

arxiv: 2602.01221 · v2 · submitted 2026-02-01 · 💻 cs.FL

A Complexity Bound for Determinisation of Min-Plus Weighted Automata

Shaull Almagor , Guy Arbel , Sarai Sheinvald This is my paper

Pith reviewed 2026-05-16 08:37 UTC · model grok-4.3

classification 💻 cs.FL

keywords min-plus automataweighted automatadeterminisationcomplexity boundfast-growing hierarchytropical semiringdecidabilityautomata theory

0 comments

The pith

Determinisation of min-plus weighted automata has an explicit complexity bound in the fast-growing hierarchy.

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

The paper establishes the first complexity upper bound for turning a nondeterministic min-plus weighted automaton into an equivalent deterministic one. It replaces the earlier purely existential decidability proof with a constructive framework that tracks runs of the automaton explicitly. This framework yields membership in the fast-growing hierarchy while also tightening the original argument. A reader cares because the result converts a theoretical decidability statement into a concrete measure of computational cost for an operation that appears in verification and optimization.

Core claim

The determinisation problem for min-plus weighted automata lies in the fast-growing hierarchy. The authors supply a constructive framework for analysing runs that captures all relevant behaviours without non-constructive steps, thereby both proving the bound and simplifying the prior existential decidability argument.

What carries the argument

A versatile constructive framework for analysing runs of weighted automata that tracks all relevant behaviours explicitly.

Load-bearing premise

The earlier existential decidability proof is correct and the new run-analysis framework faithfully records every accepting run without hidden non-constructive choices.

What would settle it

An explicit family of min-plus automata whose deterministic equivalents require a number of states or computation steps that grows faster than any function in the fast-growing hierarchy for the given input size.

Figures

Figures reproduced from arXiv: 2602.01221 by Guy Arbel, Sarai Sheinvald, Shaull Almagor.

**Figure 1.** Figure 1: A configuration of A is a vector c ∈ Z Q ∞ which, intuitively, describes for each q ∈ Q the weight c(q) of a minimal run to q thus far. We denote by xconf(q0, w) the configuration reached after reading w starting from q0. We denote by δB : Q × Σ → 2 Q the Boolean transition function that corresponds to the underlying NFA induced by finite-weight transitions (and naturally extend it to δB : 2Q × Σ → 2 Q). A… view at source ↗

**Figure 9.** Figure 9: A summary of our proof flow. The precise main result is the following. ▶ Theorem 8.1. Consider a WFA A, then A is undeterminisable if and only if there is a B-gap witness with B = GAmp(|S|, 0) where |S| is the size of Ab. Note that the direction A is undeterminisable =⇒ B-gap witness is trivial from Theorem 2.2. We handle the converse in several steps. Step 1: From a Gap witness to a ψ-Decreasing Word. Con… view at source ↗

**Figure 21.** Figure 21: ▶ Definition 19.13 (Cover decomposition). Consider a (d, i) well-separated word w1w2w3 (see Definition 19.8) with a set of independent runs I and a decomposition w2 = u0u1 · · · utut+1. Denote vj = u0 · u1 · · · uj and cj = xconf(s0, vj ) for every 0 ≤ j ≤ t. Let b = Cov(d + 1, i) with |I| = i. The decomposition is a cover if for every 0 < j ≤ t and state s ∈ supp(cj ) there exists ρ ∈ I such that nearb(ρ… view at source ↗

read the original abstract

The determinisation problem for min-plus (tropical) weighted automata was recently shown to be decidable. However, the proof is purely existential, relying on several non-constructive arguments. Our contribution in this work is twofold: first, we present the first complexity bound for this problem, placing it in the Fast-growing hierarchy. Second, our techniques introduce a versatile framework to analyse runs of weighted automata in a constructive manner. In particular, this simplifies the previous decidability argument and provides a tighter analysis, thus serving as a critical step towards a tight complexity bound.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives the first explicit complexity bound for min-plus automata determinization, placing it in the fast-growing hierarchy through a new constructive run-analysis framework.

read the letter

The main news is that determinization for min-plus weighted automata now has an explicit complexity bound in the fast-growing hierarchy. The authors also supply a constructive framework for analyzing runs that turns the prior existential decidability result into something with a concrete upper bound and a simpler argument overall. This is the first such bound, and the framework is what makes it possible. It tracks run heights and weight combinations inductively, which replaces non-constructive steps and gives a tighter picture of how the state space grows. For anyone working with cost-tracking automata in verification or optimization, that constructive handle on the runs is the useful part. The bound itself is high in the hierarchy, as these problems often are, and the paper presents the result as an intermediate step toward a tighter analysis rather than claiming finality. That framing is straightforward. The main soft spot is that the abstract gives no proof sketch or definitions, so the claim rests entirely on whether the inductive construction in the full paper really captures every relevant run without introducing extra towers or hidden choices. The stress-test note sees no such problem, but that needs checking against the details. This work is for specialists in weighted automata and the complexity of their decision procedures. A reader who already knows the recent decidability result will see the progress most clearly. It deserves peer review because the constructive method is new and the complexity claim is the first of its kind.

Referee Report

2 major / 2 minor

Summary. The paper claims to deliver the first explicit complexity bound for determinising min-plus weighted automata, locating the problem in the fast-growing hierarchy, while supplying a constructive framework for analysing runs that replaces prior non-constructive decidability arguments and yields a tighter analysis.

Significance. If the central claims hold, the result is significant: it supplies the first concrete complexity bound for this determinisation problem and introduces a reusable constructive technique for weighted-automaton runs. The inductive analysis of run heights and weight combinations is presented as a step toward tighter bounds, and the constructive replacement of existential arguments strengthens the decidability result.

major comments (2)

[§4] §4 (Inductive analysis): the placement of the bound inside the fast-growing hierarchy rests on the height and weight-combination induction; the manuscript must exhibit the precise base cases and the exact recurrence that produces the tower height, because the abstract claim that the bound is 'in the fast-growing hierarchy' is otherwise unverifiable from the given sketch.
[§3.2] §3.2 (Run representation): the constructive framework is asserted to capture all relevant runs without hidden non-constructive choice; an explicit statement that every accepting run of the original automaton corresponds to a finite-height tree in the new representation is required, as this correspondence is load-bearing for both the complexity bound and the simplification of the prior decidability proof.

minor comments (2)

[§2] The notation for min-plus matrix multiplication and the definition of run weight should be accompanied by a small worked example in §2 to aid readability.
[Figure 2] Figure 2 (state-space construction) would benefit from an explicit legend distinguishing original states from the new run-height labels.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the positive evaluation and the constructive suggestions. We agree that both major comments can be addressed by adding explicit details, and we will revise the manuscript accordingly to make the inductive analysis and run correspondence fully verifiable.

read point-by-point responses

Referee: [§4] §4 (Inductive analysis): the placement of the bound inside the fast-growing hierarchy rests on the height and weight-combination induction; the manuscript must exhibit the precise base cases and the exact recurrence that produces the tower height, because the abstract claim that the bound is 'in the fast-growing hierarchy' is otherwise unverifiable from the given sketch.

Authors: We agree that the current sketch in §4 leaves the precise base cases and recurrence implicit. In the revised manuscript we will add a dedicated paragraph (or short subsection) that states the base cases for height 0 and the initial weight combinations, followed by the exact inductive recurrence that produces the tower height in the fast-growing hierarchy. This will render the placement of the bound directly verifiable from the text. revision: yes
Referee: [§3.2] §3.2 (Run representation): the constructive framework is asserted to capture all relevant runs without hidden non-constructive choice; an explicit statement that every accepting run of the original automaton corresponds to a finite-height tree in the new representation is required, as this correspondence is load-bearing for both the complexity bound and the simplification of the prior decidability proof.

Authors: We will insert an explicit statement (as a lemma or proposition) in §3.2 establishing that every accepting run of the original automaton corresponds to a finite-height tree in the new representation. The proof will be entirely constructive, with no appeal to non-constructive choice, thereby reinforcing both the complexity bound and the simplified decidability argument. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper replaces a prior existential decidability proof with an explicit constructive framework for run analysis in min-plus automata. The complexity bound is obtained via inductive analysis of run heights and weight combinations placed in the fast-growing hierarchy. No equations, self-definitions, fitted parameters renamed as predictions, or load-bearing self-citations appear in the abstract or described derivation. The central claim remains independent of its own outputs.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review supplies no explicit free parameters, axioms, or invented entities; the contribution is described as a complexity placement and a constructive analysis framework.

pith-pipeline@v0.9.0 · 5388 in / 913 out tokens · 43806 ms · 2026-05-16T08:37:44.111350+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

Our main result is that the determinisation problem is decidable in primitive-recursive complexity... using separated repeating infixes and quantitative zooming technique

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

78 extracted references · 78 canonical work pages

[1]

If there existsB∈N such that there is noB-gap witness overΣ, thenA is determinisable

work page
[2]

suggested

If there is a finite alphabetΣ′⊆Σ such that for everyB∈N there is aB-gap witness over Σ′, thenA is undeterminisable. Observe that for WFAs over a finite alphabet, Theorem 10.3 provides an exact character- isation of determinisability. 11 The Baseline-Augmented Subset Construction We recall a construction from [1] of a WFAˆA that augmentsA with additional ...

work page 2026
[3]

If (s,r ) /∈GrnPairs(S′,w ) then mwt(s wm·2m, −−−−−→r)>n

work page
[4]

13 The Cactus Extension Intuitively, when reaching a stable cycle, we wish to mimic its long-term behaviour with a single letter

If (s,r )∈GrnPairs(S′,w ) with grounding stateg, then mwt(s wm·2m −−−−→r) = mwt(s wM0·2m −−−−−→r) = mwt(s wm −−→g wm −−→r) Moreover, we havemwt(s wm′·2m −−−−−→r)≤mwt(s wm −−→g wm −−→r) for everym′∈N. 13 The Cactus Extension Intuitively, when reaching a stable cycle, we wish to mimic its long-term behaviour with a single letter. This is the motivation behi...

work page 2026
[5]

folding” parts of words into a cactus, “unfolding

We define the setghost-reachable states ofw from s as δ(s,w ) ={(p2,q 2,T′ 1)|p2∈T′ 1}. ▶ Remark 13.13 (Ghost States are implied by Reachable States).Note thatδ(s,w ) includes the ghost states as well as the standard reachable states. That is,δB(s,w )⊆δ(s,w ). Moreover, observe thatδ(s,w ) is determined byδB(s,w ), and therefore ifδB(s,w ) =δB(s′,w′) then...

work page 2026
[6]

If q∈supp(c1) then c2(q) = c1(q)

work page
[7]

Unfolding cactus letters is fairly “safe”:αS′,w is replaced with many iterations ofw

If q /∈supp(c1) then c2(q)>F −max_eff(xαS′,wy) (and could be∞). Unfolding cactus letters is fairly “safe”:αS′,w is replaced with many iterations ofw. However, we also want to unfold rebase letters. This turns out to be more involved. We refer to [1] for the details, as we do not need them here. Having the ability to unfold, we can apply it recursively unt...

work page
[8]

If u∈(Γ0 ∞)∗then flatten(u≀F)∈(Γ0 0)∗(i.e., ifu has only cactus letters, the flattening has only Γ0 0 letters)

work page
[9]

relevant

If u has rebase letters, then flatten(u≀F)∈(Γ0 0∪JL)∗(i.e., flattening rebase letters introduces jump letters). The following holds: letc = xconf(s0,u ) and d = xconf(s0, flatten(u≀F)). Then δB(s0,u ) = supp(c)⊆supp(d) =δB(s0, flatten(u≀F )) =δ(s0, flatten(u≀F)) =δ(s0,u ) and for every q ∈supp(d), if q ∈supp(c) then c(q) = d(q), and otherwise d(q)≥ max{c(...

work page 2026
[10]

The potential of w is ϕ(w) = dom_val(cw)

work page
[11]

violently

The charge of w is ψ(w) =−min{cw(q)|q∈Q}. Note that ϕ(w) and ψ(w) are always nonnegative (when they are defined), since the minimal run is of weight at most0, due to the seamless baseline run. The notions of dominant state, potential and charge are depicted in Figure 15 Figure 15The stateq reached after readingw is dominant: there exists a finite-run on a...

work page 2026
[12]

The baseline run ofxconf(d,w ) is seamless

work page
[13]

ϕ(xconf(c,w ))≤ϕ(xconf(d,w ))

work page
[14]

pumpable infix

ψ(xconf(c,w ))≥ψ(xconf(d,w )) LICS 2026 16:46 A Complexity Bound for Determinisation of Min-Plus Weighted Automata 17 A Witness for Undeterminisability The characterisation of undeterminisability given in [1] is by means ofwitnesses – a word containing a cactus letter whose various unfoldings serve to induce arbitrarily large gap witnesses as per Definiti...

work page 2026
[15]

αS1,w2∈Υ 1 simp,1 for type-1), and w3∈(Υ 1 simp,0+JL)∗·Υ 1 gen,1

w1∈(Υ 0 simp,0)∗, S1 = δ(s0,w 1), αS1,w2∈Υ 0 simp,0 (resp. αS1,w2∈Υ 1 simp,1 for type-1), and w3∈(Υ 1 simp,0+JL)∗·Υ 1 gen,1

work page
[16]

δB(s0,w 1) =δB(s0,w 1·w2m 2 ) (i.e., w2m 2 cycles on the reachable states)

work page
[17]

The main characterisation proved in [1] is thatˆA∞ ∞is undeterminisable if and only if it has a witness

mwt(s0 w1·w2m 2 ·w3 −−−−−−−→S)<∞whereas mwt(s0 w1αS1,w2w3 −−−−−−−−→S) =∞. The main characterisation proved in [1] is thatˆA∞ ∞is undeterminisable if and only if it has a witness. Our modified definition is more restrictive than in [1], hence the challenge is in proving the completeness of this characterisation. The soundness, however, follows directly fro...

work page
[18]

xconf(s0,ux 2mM0v′)≤xconf(s0,uαB,xv′). S. Almagor, G. Arbel and S. Sheinvald 16:47

work page
[19]

Either ˆA∞ ∞has a type-0 witness, or ϕ(ux2mM0v′) = ϕ(uαB,xv′). Proof. The proof structure is almost identical to the analogous claim in [1], but some changes need to be made to account for the new definitions of dominance (Definition 16.1) and of witnesses. Naturally, we tailor both definitions so that this proof carries out smoothly. Item 1 follows immed...

work page
[20]

very high

By Definition 16.1, this means that there existsz∈(Υ 1 simp,0+JL)∗Υ 1 gen,1 such that mwt(q z − →S) <∞whereas for everyp∈S with c′ 2(p)< c′ 2(q) we havemwt(p z − →S) =∞. We now split to cases according to whether q∈S′ 2\S2 (i.e., q is “very high”) orq∈S2 (i.e., q is “low”). Dominant State is Very High If q∈S′ 2\S2, we claim that (ux2mM0,αB,x,z ) is a type...

work page 2026
[21]

Also, note thatB = δ(s0,u ) =δ(s0,ux ) =δ(s0,ux 2mM0) since αB,x is a stable cycle readable afteru

ux2mM0∈(Υ 0 simp,0)∗,αB,x∈Υ 0 simp,0 and z∈(Υ 1 simp,0+JL)∗Υ 1 gen,1. Also, note thatB = δ(s0,u ) =δ(s0,ux ) =δ(s0,ux 2mM0) since αB,x is a stable cycle readable afteru

work page
[22]

By Proposition 12.5 we have that δB(s0,ux 2mM0) =δB(s0,ux 2m(M0+1)) =δB(s0,ux 2mM0x2m)

work page
[23]

In particular, mwt(s0 ux2mM0x2m −−−−−−−−→q)<∞

Since q∈S′ 2 = δB(s0,ux 2mM0) then by Item 2 above we haveq∈δB(s0,ux 2mM0x2m). In particular, mwt(s0 ux2mM0x2m −−−−−−−−→q)<∞. Since z satisfies that mwt(q z − →S)<∞, we conclude that: mwt(s0 ux2mM0·x2m·z −−−−−−−−−→S)≤ mwt(s0 ux2mM0x2m −−−−−−−−→q) + mwt(q z − →S)<∞ It therefore remains to prove thatmwt(s0 ux2mM0·αB,x·z −−−−−−−−−−→S) =∞. To this end, we cla...

work page
[24]

Then, by the observationsabove, wehave c′ 2(q) = c2(q)

=S′ 2). Then, by the observationsabove, wehave c′ 2(q) = c2(q). We claim that for every prefixv′ofv it holds thatϕ(ux2mM0v′) = ϕ(uαB,xv′). Indeed, fix such a prefixv′and denote c3 = xconf(s0,uαB,xv′) = xconf(c2,v′) S3 = supp(c3) c′ 3 = xconf(s0,ux 2mM0v′) = xconf(c′ 2,v′) S′ 3 = supp(c3) Similarly to the above, we haveS3⊆S′ 3, and due to the choice ofF as...

work page
[25]

xconf(s0,w )≤xconf(s0,w′)

work page
[26]

EitherˆA∞ ∞has a type-0 witness, or

ϕ(w) = ϕ(w′) (if the potential is defined, with respect to the given initial states0). ▶ Remark 17.6 (The Prefix “EitherˆA∞ ∞has a type-0 witness, or...”).Most of our reasoning about potential in the coming sections is ultimately based on Lemma 17.4. Therefore, the prefix “EitherˆA∞ ∞has a type-0 witness, or the following holds” appears in many statements...

work page 2026
[27]

That is, the subsets of states reached afteru,ux,uxy are the same

supp(cu) = supp(cux) = supp(cuxy) =B for some subsetB⊆S. That is, the subsets of states reached afteru,ux,uxy are the same

work page
[28]

|x|≤1 mL(dep(x) + 1)

work page
[29]

Then B can be partitioned to B =V1∪...∪Vℓfor someℓsuch that the following hold

Define G = { 4|S|mmax_eff(xy) if L =Lsimp, 4|S|mmax_eff(xy) + H if L =Lgen. . Then B can be partitioned to B =V1∪...∪Vℓfor someℓsuch that the following hold. a. For every 1≤j < ℓ, every s∈Vj,s′∈Vj+1 and every ξ∈{u,ux,uxy}we have cξ(s′)−cξ(s) > G. That is, the values assigned to states inVj+1 are significantly larger than those assigned toVj in the configu...

work page
[30]

positive

There is a seamless baseline runρ:s0 uxyv −−−→s for somes. The definition of SRI is structural. We now specialise it with a restriction onϕ or on ψ, as follows. ▶ Definition 18.2. Consider an SRIuxyz over L. It is aSimple SRI (SSRI)if L = Lsimp and in addition ϕ(u)≤ϕ(ux)≤ϕ(uxy), and ϕ(u) = ϕ(ux) iff ϕ(ux) = ϕ(uxy). It is aGeneral SRI (GSRI)if L =Lgen and ...

work page 2026
[31]

In step 4 we reach a contradiction, since this negative run is lower thanVj

so it becomes a negative run. In step 4 we reach a contradiction, since this negative run is lower thanVj. We now turn to the precise details. Letρ:s xk −→s with s∈δ(s0,u ) and k≤|S|be a negative minimal-slope run. Note that(δ(s0,u ),x ) is a reflexive cycle. Indeed, by Definition 18.1 we haveδB(B,x ) = B for B =δB(s0,u ), and by Remark 13.13 the ghost-re...

work page 2026
[32]

For everyt∈S it holds thatmwt(s0 w − →t)≤mwt(s0 w′ −→t)

work page
[33]

interfere

Either there is a type-0 witness, orϕ(w)≤ϕ(w′). Proof. Conceptually, the proof is an adaptation of the analogue in [1]. Technically, however, the proof is supported by the careful choice of bounds in Definition 18.1, which are different from those in [1]. Denote S′=δ(s0,u ), we therefore consider replacing the infixxy with αS′,x. Step 1: Fromy to x∗ The f...

work page 2026
[34]

way above

and cu′′x′(s′′). If cu′x′′(s2)< cu′x′′(s′′) then by the dominance ofs′′we have thatmwt(s2 z′′ −→S) =∞, in contradiction towt(τ′)<∞. Ifs2∈V′ d (recall thats′′∈V′ d ass∈Vd, wheres is the corresponding maximal dominant state in cux), thens2∈Vd. By Proposition 18.5 we haves1∈Vd. Sinces1 xkm − −− →r and r xkm − −− →s2, we haver∈Vd as well (otherwise eithers1 o...

work page 2026
[35]

t = Ramsey(Typ(d + 1,i ), 3)

work page
[36]

For every0≤j <j′≤t we have ϕ(w1vj)< ϕ(w1vj′)

work page
[37]

For every1≤j≤t and prefixx of uj we have ϕ(w1vj−1x)≤ϕ(w1vj)

work page
[39]

For every1≤j≤t we have|ui|≥Len(d, 1). Intuitively, aϕ-increasing decomposition has the following properties: there are enough segments to apply some Ramsey argument (Item 1), the potential when moving from one end of a segment to the next end of a segment strictly increases (Item 2), while in all prefixes between such ends the potential might decrease, bu...

work page
[40]

t = Ramsey(Typ(d + 1,i ), 3) + 1

work page
[41]

For every0<j <j′≤t we have ϕ(w1vj) = ϕ(w1vj′)

work page
[43]

|u0|≥Len(d + 1,i + 1)

work page
[44]

artificially

For every 0 < j≤t and prefixx of uj with|x|multiple of E we have ϕ(w1vjx)≤ ϕ(w1vj+1). Analogously to Proposition 19.10, we show that every bounded-amplitude word can be decomposed. The proof, however, is more intricate. Intuitively, this is because we no longer have the increasing potential to decompose by, so we need to introduce the decomposition indice...

work page 2026
[45]

w′ 2 has atT + 1 prefixes z0,z 1,...,zT where ϕ(w1u0zk) = ϕ(w1) +P for everyk≥0 (where the prefixes are concatenations of thexjs)

work page
[46]

Moreover, ifP =−Amp(d+1,i ) then we trivially have the first case, provided|w′ 2|≥E·(T +1)

There is an infixw′′ 2 of w2 that isP−1-upper bounded, and|w′′ 2|≥E·t′ T+2. Moreover, ifP =−Amp(d+1,i ) then we trivially have the first case, provided|w′ 2|≥E·(T +1). Recall thatt′≥(T + 2)2Amp(d+1,i)+1 and thatw2 is Amp(d + 1,i )-upper bounded. We can therefore apply the reasoning above inductively, starting fromP = Amp(d + 1,i ). Since we divide the len...

work page
[48]

w1w2w2 =w′ 1w′ 2w′ 3 wherew′ 1w′ 2w′ 3 is a (d−1, 1)-fit well-separated word (Definition 19.8) and w′ 2 is an infix ofw2 with|w′ 2|= 1 32m2 Len(d, 1). Proof. Let vj denote u0···uj as per Definitions 19.9 and 19.11. We begin by identifying a structure that repeats twice along the decomposition. Letb = 2Cov(d + 1,i ), and consider a complete graph on the ve...

work page
[49]

supp(cu) = supp(cux) = supp(cuxy) = B: since the decomposition is a cover, then as noted in Definition 19.13, every reachable state is near some independent run, and in particular the equivalentdiff_typeb implies the same support

work page
[50]

Then, the fact thatϕ(u) = ϕ(ux) iff ϕ(ux) = ϕ(uxy) is actually implied by the definition, in particular by Item 4 below

In the case of aϕ-increasing decomposition (Definition 19.9),ϕ(u)≤ϕ(ux)≤ϕ(uxy) follows immediately. Then, the fact thatϕ(u) = ϕ(ux) iff ϕ(ux) = ϕ(uxy) is actually implied by the definition, in particular by Item 4 below. In the case of aϕ-bounded decomposition, we already haveϕ(u) = ϕ(ux) = ϕ(uxy). Note that this is the only place where we treat the two t...

work page
[51]

|x|≤1 mLsimp(dep(x) + 1) = 1 m Len(d + 1, 1): this is immediate from the requirement in Definition 19.7 that|w2|≤1 32m2 Len(d + 1,i )≤1 m Len(d + 1, 1) (recall that the inductive definition of Len(d + 1,i ) is with increasingi)

work page
[52]

That is, setVj = supp(nearb(ρj,x )) for b = Cov(d + 1,i ) where I ={ρ1 <

We partitionB = V1∪...∪Vi according to the independent runs. That is, setVj = supp(nearb(ρj,x )) for b = Cov(d + 1,i ) where I ={ρ1 <... <ρi}. By Definition 19.13 this is indeed a partition. The gaps betweenVj and Vj+1 are higher than 4|S|mmax_eff(xy): byDefinition19.8theset I hasgapatleast 4m2(MaxWt(d)Len(d, 1)Len(d+ 1,i ) + Cov(d + 1,i )) Notice that|xy...

work page
[53]

This concludes thatuxyv is an SSRI

The seamless baseline run exists by Definition 19.6. This concludes thatuxyv is an SSRI. LICS 2026 16:72 A Complexity Bound for Determinisation of Min-Plus Weighted Automata If dep(x)<d . In this case we treat the two types of decomposition separately. The case of aϕ-increasing decomposition is simple: we just restrict attention to an infix ofw2, as follo...

work page 2026
[54]

Still by Definition 19.9 we haveϕ(w′ 1)≤ϕ(w′ 1w′

Note that there is such a suffix since|x|≥Len(d, 1) as a concatenation of uj’s, and by Definition 19.9. Still by Definition 19.9 we haveϕ(w′ 1)≤ϕ(w′ 1w′

work page
[55]

TakeI′={ρ1}(i.e., arbitrarily choose a single independent run from I) sow′ 1w′ 2w′ 3 with I′is a (d−1, 1) fit word, as per Definition 19.7

(viewing w′ 2 as a prefix ofuj′). TakeI′={ρ1}(i.e., arbitrarily choose a single independent run from I) sow′ 1w′ 2w′ 3 with I′is a (d−1, 1) fit word, as per Definition 19.7. The case ofϕ-bounded decomposition is slightly more delicate. We still takew′ 2 to be the suffix ofx of length 1 32m2 Len(d, 1). This is possible since each part in the decomposition ...

work page
[56]

We can now proceed as above by taking I′={ρ1}, and we are done

(although between them the potential may increase, but this does not concern us). We can now proceed as above by taking I′={ρ1}, and we are done. ◀ 19.1 From Well Separation to SSRI We now have the tools to show that given a well-separated word, we can obtain an SSRI from it. To do so, we develop an effective version of theZooming Techniqueintroduced in [...

work page
[57]

w1w2w3 =uxyv whereuxyv is an SSRI withdep(x) =d and xy is an infix ofw2

work page
[58]

w1w2w2 =w′ 1w′ 2w′ 3 wherew′ 1w′ 2w′ 3 is a (d−1, 1)-fit well-separated word (Definition 19.8) and w′ 2 is an infix ofw2 with|w′ 2|= 1 32m2 Len(d, 1). Proof. Let I ={ρ1 < ... < ρi}be the set of independent runs associated withw1w2w3 (Definition 19.2). Consider the behaviour ofϕ along w2 as per Definition 19.8. We claim there are two cases: eitherw1w2w3 is...

work page 2026
[59]

t = Ramsey(GTyp(d + 1,i ), 3)

work page
[60]

For every0≤j <j′≤t we have ψ(w1vj)> ψ(w1vj′)

work page
[61]

For every1≤j≤t and prefixx of uj we have ψ(w1vj−1x)≥ψ(w1vj)

work page
[63]

In contrast to Proposition 19.10, beingψ high amplitude is not a sufficient condition for having a decomposition

For every1≤j≤t we have|ui|≥GLen(d, 1). In contrast to Proposition 19.10, beingψ high amplitude is not a sufficient condition for having a decomposition. Indeed, it may be the case that the charge has unbounded growth, which then might cause the word to be very short. Fortunately, if this is the case, then Lemma 16.6 already gives us unbounded potential, w...

work page
[64]

t = Ramsey(GTyp(d + 1,i ), 3) + 1

work page
[65]

For every0<j <j′≤t we have ψ(w1vj) = ψ(w1vj′)

work page
[66]

For every0≤j≤t we have that|uj|is a multiple ofE

work page
[67]

|u0|≥GLen(d + 1,i + 1)

work page
[68]

▶ Proposition 20.7(From bounded amplitude toψ-bounded decomposition)

For every 0 < j≤t and prefixx of uj with|x|multiple of E we have ψ(w1vjx)≥ ψ(w1vj+1). ▶ Proposition 20.7(From bounded amplitude toψ-bounded decomposition). Every ψ-bounded word has aψ-bounded (d,i )-decomposition. Proof. Consider a ψ-bounded word w1w2w3. By Definition 20.3 we have that |w2|= 1 32m2 GLen(d + 1,i ) and for every prefixx of w2 it holds that ...

work page 2026
[69]

w′ 2 has atT + 1 prefixes z0,z 1,...,zT where ψ(w1u0zk) = ψ(w1)−P for everyk≥0 (where the prefixes are concatenations of thexjs)

work page
[70]

Moreover, ifP =−GAmp(d+1,i )thenwetriviallyhavethefirstcase, provided |w′ 2|≥E·(T +1)

There is an infixw′′ 2 of w2 that isP−1-lower bounded, and|w′′ 2|≥E·t′ T+2. Moreover, ifP =−GAmp(d+1,i )thenwetriviallyhavethefirstcase, provided |w′ 2|≥E·(T +1). Recall thatt′≥(T + 2)2GAmp(d+1,i)+1 and thatw2 is GAmp(d + 1,i )-lower bounded. We can therefore apply the reasoning above inductively, starting fromP = GAmp(d + 1,i ). Since we divide the lengt...

work page
[71]

w1w2w3 =uxyv whereuxyv is a GSRI withdep(x) =d, andxy is an infix ofw2

work page
[72]

w1w2w2 = w′ 1w′ 2w′ 3 where w′ 1w′ 2w′ 3 is a ψ−(d−1, 1)-fit well-separated word (Defini- tion 20.3) and|w′ 2|= 1 32m2 Len(d, 1). Proof. Let vj denoteu0···uj as per Definitions 20.4 and 20.6. We begin by identifying a structure that repeats twice along the decomposition. Letb = 2GCov(d + 1,i ), and consider a complete graph on the vertices{1,...,t}. We de...

work page
[73]

supp(cu) = supp(cux) = supp(cuxy) = B: since the decomposition is a cover, then as noted in Definition 20.8, every reachable state is near some independent run, and in particular the equivalentdiff_typeb implies the same support

work page
[74]

Then, the fact thatψ(u) = ψ(ux) iff ψ(ux) = ψ(uxy) is actually implied by the definition, in particular by Item 4 below

In the case of aψ-decreasing decomposition (Definition 20.4),ψ(u)≥ψ(ux)≥ψ(uxy) follows immediately. Then, the fact thatψ(u) = ψ(ux) iff ψ(ux) = ψ(uxy) is actually implied by the definition, in particular by Item 4 below. In the case of aψ-bounded decomposition, we already haveψ(u) = ψ(ux) = ψ(uxy). Note that this is the only place where we treat the two t...

work page
[75]

|x|≤1 mLgen(dep(x) + 1) = 1 m GLen(d + 1, 1): this is immediate from the requirement in Definition 20.2 that|w2|≤1 32m2 GLen(d+1,i )≤1 m GLen(d+1, 1) (recall that the inductive definition of GLen(d + 1,i ) is with increasingi)

work page
[76]

That is, setVj = supp(nearb(ρj,x )) for b = GCov(d + 1,i ) where I ={ρ1 <...<ρi}

We partitionB = V1∪...∪Vi according to the independent runs. That is, setVj = supp(nearb(ρj,x )) for b = GCov(d + 1,i ) where I ={ρ1 <...<ρi}. By Definition 20.8 this is indeed a partition. The gaps betweenVj and Vj+1 are higher than 4|S|mmax_eff(xy)+H: byDefinition20.3theset I hasgapatleast 4m2(GMaxWt(d)GLen(d, 1)GLen(d+ 1,i ) + GCov(d + 1,i ) + H) Notic...

work page 2026
[77]

This concludes thatuxyv is an GSRI

The seamless baseline run exists by Definition 20.1. This concludes thatuxyv is an GSRI. If dep(x)<d . In this case we treat the two types of decomposition separately. The case of aψ-decreasing decomposition is simple: we just restrict attention to an infix ofw2, as follows. Definew′ 2 to be the suffix ofx of length 1 32m2 GLen(d, 1), and letw′ 1,w′ 3 be ...

work page
[78]

Still by Definition 20.4 we haveψ(w′ 1)≥ψ(w′ 1w′

Note that there is such a suffix since|x|≥GLen(d, 1) as a concatenation of uj’s, and by Definition 20.4. Still by Definition 20.4 we haveψ(w′ 1)≥ψ(w′ 1w′

work page
[79]

TakeI′={ρ1}(i.e., arbitrarily choose a single independent run from I) sow′ 1w′ 2w′ 3 with I′is a ψ−(d−1, 1) fit word, as per Definition 20.2

(viewing w′ 2 as a prefix ofuj′). TakeI′={ρ1}(i.e., arbitrarily choose a single independent run from I) sow′ 1w′ 2w′ 3 with I′is a ψ−(d−1, 1) fit word, as per Definition 20.2. The case ofψ bounded decomposition is slightly more delicate. We still takew′ 2 to be the suffix ofx of length 1 32m2 GLen(d, 1). This is possible since each part in the decompositi...

work page
[80]

We can now proceed as above by takingI′={ρ1}, and we are done

(although between them the charge may decrease, but this does not concern us). We can now proceed as above by takingI′={ρ1}, and we are done. ◀ 20.1 From Well Separation to GSRI We now have the tools to show that given aψ well-separated word, we can obtain a GSRI from it. To do so, we use a similar zooming argument as in Section 19.1. Note that the caveat...

work page
[81]

w1w2w3 =uxyv whereuxyv is an GSRI withdep(x) =d and xy is an infix ofw2

work page
[82]

forgotten

w1w2w2 = w′ 1w′ 2w′ 3 where w′ 1w′ 2w′ 3 is a ψ−(d−1, 1)-fit well-separated word (Defini- tion 20.3) andw′ 2 is an infix ofw2 with|w′ 2|= 1 32m2 GLen(d, 1). Proof. Assume there is no wordw′∈(Γ0 0)∗such that ϕ(w′)> H (otherwise we are done). Consider therefore a ψ−(d,i )-fit well-separated wordw1w2w3. Let I ={ρ1 < ... < ρi} be the set of independent runs a...

work page 2026

[1] [1]

If there existsB∈N such that there is noB-gap witness overΣ, thenA is determinisable

work page

[2] [2]

suggested

If there is a finite alphabetΣ′⊆Σ such that for everyB∈N there is aB-gap witness over Σ′, thenA is undeterminisable. Observe that for WFAs over a finite alphabet, Theorem 10.3 provides an exact character- isation of determinisability. 11 The Baseline-Augmented Subset Construction We recall a construction from [1] of a WFAˆA that augmentsA with additional ...

work page 2026

[3] [3]

If (s,r ) /∈GrnPairs(S′,w ) then mwt(s wm·2m, −−−−−→r)>n

work page

[4] [4]

13 The Cactus Extension Intuitively, when reaching a stable cycle, we wish to mimic its long-term behaviour with a single letter

If (s,r )∈GrnPairs(S′,w ) with grounding stateg, then mwt(s wm·2m −−−−→r) = mwt(s wM0·2m −−−−−→r) = mwt(s wm −−→g wm −−→r) Moreover, we havemwt(s wm′·2m −−−−−→r)≤mwt(s wm −−→g wm −−→r) for everym′∈N. 13 The Cactus Extension Intuitively, when reaching a stable cycle, we wish to mimic its long-term behaviour with a single letter. This is the motivation behi...

work page 2026

[5] [5]

folding” parts of words into a cactus, “unfolding

We define the setghost-reachable states ofw from s as δ(s,w ) ={(p2,q 2,T′ 1)|p2∈T′ 1}. ▶ Remark 13.13 (Ghost States are implied by Reachable States).Note thatδ(s,w ) includes the ghost states as well as the standard reachable states. That is,δB(s,w )⊆δ(s,w ). Moreover, observe thatδ(s,w ) is determined byδB(s,w ), and therefore ifδB(s,w ) =δB(s′,w′) then...

work page 2026

[6] [6]

If q∈supp(c1) then c2(q) = c1(q)

work page

[7] [7]

Unfolding cactus letters is fairly “safe”:αS′,w is replaced with many iterations ofw

If q /∈supp(c1) then c2(q)>F −max_eff(xαS′,wy) (and could be∞). Unfolding cactus letters is fairly “safe”:αS′,w is replaced with many iterations ofw. However, we also want to unfold rebase letters. This turns out to be more involved. We refer to [1] for the details, as we do not need them here. Having the ability to unfold, we can apply it recursively unt...

work page

[8] [8]

If u∈(Γ0 ∞)∗then flatten(u≀F)∈(Γ0 0)∗(i.e., ifu has only cactus letters, the flattening has only Γ0 0 letters)

work page

[9] [9]

relevant

If u has rebase letters, then flatten(u≀F)∈(Γ0 0∪JL)∗(i.e., flattening rebase letters introduces jump letters). The following holds: letc = xconf(s0,u ) and d = xconf(s0, flatten(u≀F)). Then δB(s0,u ) = supp(c)⊆supp(d) =δB(s0, flatten(u≀F )) =δ(s0, flatten(u≀F)) =δ(s0,u ) and for every q ∈supp(d), if q ∈supp(c) then c(q) = d(q), and otherwise d(q)≥ max{c(...

work page 2026

[10] [10]

The potential of w is ϕ(w) = dom_val(cw)

work page

[11] [11]

violently

The charge of w is ψ(w) =−min{cw(q)|q∈Q}. Note that ϕ(w) and ψ(w) are always nonnegative (when they are defined), since the minimal run is of weight at most0, due to the seamless baseline run. The notions of dominant state, potential and charge are depicted in Figure 15 Figure 15The stateq reached after readingw is dominant: there exists a finite-run on a...

work page 2026

[12] [12]

The baseline run ofxconf(d,w ) is seamless

work page

[13] [13]

ϕ(xconf(c,w ))≤ϕ(xconf(d,w ))

work page

[14] [14]

pumpable infix

ψ(xconf(c,w ))≥ψ(xconf(d,w )) LICS 2026 16:46 A Complexity Bound for Determinisation of Min-Plus Weighted Automata 17 A Witness for Undeterminisability The characterisation of undeterminisability given in [1] is by means ofwitnesses – a word containing a cactus letter whose various unfoldings serve to induce arbitrarily large gap witnesses as per Definiti...

work page 2026

[15] [15]

αS1,w2∈Υ 1 simp,1 for type-1), and w3∈(Υ 1 simp,0+JL)∗·Υ 1 gen,1

w1∈(Υ 0 simp,0)∗, S1 = δ(s0,w 1), αS1,w2∈Υ 0 simp,0 (resp. αS1,w2∈Υ 1 simp,1 for type-1), and w3∈(Υ 1 simp,0+JL)∗·Υ 1 gen,1

work page

[16] [16]

δB(s0,w 1) =δB(s0,w 1·w2m 2 ) (i.e., w2m 2 cycles on the reachable states)

work page

[17] [17]

The main characterisation proved in [1] is thatˆA∞ ∞is undeterminisable if and only if it has a witness

mwt(s0 w1·w2m 2 ·w3 −−−−−−−→S)<∞whereas mwt(s0 w1αS1,w2w3 −−−−−−−−→S) =∞. The main characterisation proved in [1] is thatˆA∞ ∞is undeterminisable if and only if it has a witness. Our modified definition is more restrictive than in [1], hence the challenge is in proving the completeness of this characterisation. The soundness, however, follows directly fro...

work page

[18] [18]

xconf(s0,ux 2mM0v′)≤xconf(s0,uαB,xv′). S. Almagor, G. Arbel and S. Sheinvald 16:47

work page

[19] [19]

Either ˆA∞ ∞has a type-0 witness, or ϕ(ux2mM0v′) = ϕ(uαB,xv′). Proof. The proof structure is almost identical to the analogous claim in [1], but some changes need to be made to account for the new definitions of dominance (Definition 16.1) and of witnesses. Naturally, we tailor both definitions so that this proof carries out smoothly. Item 1 follows immed...

work page

[20] [20]

very high

By Definition 16.1, this means that there existsz∈(Υ 1 simp,0+JL)∗Υ 1 gen,1 such that mwt(q z − →S) <∞whereas for everyp∈S with c′ 2(p)< c′ 2(q) we havemwt(p z − →S) =∞. We now split to cases according to whether q∈S′ 2\S2 (i.e., q is “very high”) orq∈S2 (i.e., q is “low”). Dominant State is Very High If q∈S′ 2\S2, we claim that (ux2mM0,αB,x,z ) is a type...

work page 2026

[21] [21]

Also, note thatB = δ(s0,u ) =δ(s0,ux ) =δ(s0,ux 2mM0) since αB,x is a stable cycle readable afteru

ux2mM0∈(Υ 0 simp,0)∗,αB,x∈Υ 0 simp,0 and z∈(Υ 1 simp,0+JL)∗Υ 1 gen,1. Also, note thatB = δ(s0,u ) =δ(s0,ux ) =δ(s0,ux 2mM0) since αB,x is a stable cycle readable afteru

work page

[22] [22]

By Proposition 12.5 we have that δB(s0,ux 2mM0) =δB(s0,ux 2m(M0+1)) =δB(s0,ux 2mM0x2m)

work page

[23] [23]

In particular, mwt(s0 ux2mM0x2m −−−−−−−−→q)<∞

Since q∈S′ 2 = δB(s0,ux 2mM0) then by Item 2 above we haveq∈δB(s0,ux 2mM0x2m). In particular, mwt(s0 ux2mM0x2m −−−−−−−−→q)<∞. Since z satisfies that mwt(q z − →S)<∞, we conclude that: mwt(s0 ux2mM0·x2m·z −−−−−−−−−→S)≤ mwt(s0 ux2mM0x2m −−−−−−−−→q) + mwt(q z − →S)<∞ It therefore remains to prove thatmwt(s0 ux2mM0·αB,x·z −−−−−−−−−−→S) =∞. To this end, we cla...

work page

[24] [24]

Then, by the observationsabove, wehave c′ 2(q) = c2(q)

=S′ 2). Then, by the observationsabove, wehave c′ 2(q) = c2(q). We claim that for every prefixv′ofv it holds thatϕ(ux2mM0v′) = ϕ(uαB,xv′). Indeed, fix such a prefixv′and denote c3 = xconf(s0,uαB,xv′) = xconf(c2,v′) S3 = supp(c3) c′ 3 = xconf(s0,ux 2mM0v′) = xconf(c′ 2,v′) S′ 3 = supp(c3) Similarly to the above, we haveS3⊆S′ 3, and due to the choice ofF as...

work page

[25] [25]

xconf(s0,w )≤xconf(s0,w′)

work page

[26] [26]

EitherˆA∞ ∞has a type-0 witness, or

ϕ(w) = ϕ(w′) (if the potential is defined, with respect to the given initial states0). ▶ Remark 17.6 (The Prefix “EitherˆA∞ ∞has a type-0 witness, or...”).Most of our reasoning about potential in the coming sections is ultimately based on Lemma 17.4. Therefore, the prefix “EitherˆA∞ ∞has a type-0 witness, or the following holds” appears in many statements...

work page 2026

[27] [27]

That is, the subsets of states reached afteru,ux,uxy are the same

supp(cu) = supp(cux) = supp(cuxy) =B for some subsetB⊆S. That is, the subsets of states reached afteru,ux,uxy are the same

work page

[28] [28]

|x|≤1 mL(dep(x) + 1)

work page

[29] [29]

Then B can be partitioned to B =V1∪...∪Vℓfor someℓsuch that the following hold

Define G = { 4|S|mmax_eff(xy) if L =Lsimp, 4|S|mmax_eff(xy) + H if L =Lgen. . Then B can be partitioned to B =V1∪...∪Vℓfor someℓsuch that the following hold. a. For every 1≤j < ℓ, every s∈Vj,s′∈Vj+1 and every ξ∈{u,ux,uxy}we have cξ(s′)−cξ(s) > G. That is, the values assigned to states inVj+1 are significantly larger than those assigned toVj in the configu...

work page

[30] [30]

positive

There is a seamless baseline runρ:s0 uxyv −−−→s for somes. The definition of SRI is structural. We now specialise it with a restriction onϕ or on ψ, as follows. ▶ Definition 18.2. Consider an SRIuxyz over L. It is aSimple SRI (SSRI)if L = Lsimp and in addition ϕ(u)≤ϕ(ux)≤ϕ(uxy), and ϕ(u) = ϕ(ux) iff ϕ(ux) = ϕ(uxy). It is aGeneral SRI (GSRI)if L =Lgen and ...

work page 2026

[31] [31]

In step 4 we reach a contradiction, since this negative run is lower thanVj

so it becomes a negative run. In step 4 we reach a contradiction, since this negative run is lower thanVj. We now turn to the precise details. Letρ:s xk −→s with s∈δ(s0,u ) and k≤|S|be a negative minimal-slope run. Note that(δ(s0,u ),x ) is a reflexive cycle. Indeed, by Definition 18.1 we haveδB(B,x ) = B for B =δB(s0,u ), and by Remark 13.13 the ghost-re...

work page 2026

[32] [32]

For everyt∈S it holds thatmwt(s0 w − →t)≤mwt(s0 w′ −→t)

work page

[33] [33]

interfere

Either there is a type-0 witness, orϕ(w)≤ϕ(w′). Proof. Conceptually, the proof is an adaptation of the analogue in [1]. Technically, however, the proof is supported by the careful choice of bounds in Definition 18.1, which are different from those in [1]. Denote S′=δ(s0,u ), we therefore consider replacing the infixxy with αS′,x. Step 1: Fromy to x∗ The f...

work page 2026

[34] [34]

way above

and cu′′x′(s′′). If cu′x′′(s2)< cu′x′′(s′′) then by the dominance ofs′′we have thatmwt(s2 z′′ −→S) =∞, in contradiction towt(τ′)<∞. Ifs2∈V′ d (recall thats′′∈V′ d ass∈Vd, wheres is the corresponding maximal dominant state in cux), thens2∈Vd. By Proposition 18.5 we haves1∈Vd. Sinces1 xkm − −− →r and r xkm − −− →s2, we haver∈Vd as well (otherwise eithers1 o...

work page 2026

[35] [35]

t = Ramsey(Typ(d + 1,i ), 3)

work page

[36] [36]

For every0≤j <j′≤t we have ϕ(w1vj)< ϕ(w1vj′)

work page

[37] [37]

For every1≤j≤t and prefixx of uj we have ϕ(w1vj−1x)≤ϕ(w1vj)

work page

[38] [39]

For every1≤j≤t we have|ui|≥Len(d, 1). Intuitively, aϕ-increasing decomposition has the following properties: there are enough segments to apply some Ramsey argument (Item 1), the potential when moving from one end of a segment to the next end of a segment strictly increases (Item 2), while in all prefixes between such ends the potential might decrease, bu...

work page

[39] [40]

t = Ramsey(Typ(d + 1,i ), 3) + 1

work page

[40] [41]

For every0<j <j′≤t we have ϕ(w1vj) = ϕ(w1vj′)

work page

[41] [43]

|u0|≥Len(d + 1,i + 1)

work page

[42] [44]

artificially

For every 0 < j≤t and prefixx of uj with|x|multiple of E we have ϕ(w1vjx)≤ ϕ(w1vj+1). Analogously to Proposition 19.10, we show that every bounded-amplitude word can be decomposed. The proof, however, is more intricate. Intuitively, this is because we no longer have the increasing potential to decompose by, so we need to introduce the decomposition indice...

work page 2026

[43] [45]

w′ 2 has atT + 1 prefixes z0,z 1,...,zT where ϕ(w1u0zk) = ϕ(w1) +P for everyk≥0 (where the prefixes are concatenations of thexjs)

work page

[44] [46]

Moreover, ifP =−Amp(d+1,i ) then we trivially have the first case, provided|w′ 2|≥E·(T +1)

There is an infixw′′ 2 of w2 that isP−1-upper bounded, and|w′′ 2|≥E·t′ T+2. Moreover, ifP =−Amp(d+1,i ) then we trivially have the first case, provided|w′ 2|≥E·(T +1). Recall thatt′≥(T + 2)2Amp(d+1,i)+1 and thatw2 is Amp(d + 1,i )-upper bounded. We can therefore apply the reasoning above inductively, starting fromP = Amp(d + 1,i ). Since we divide the len...

work page

[45] [48]

w1w2w2 =w′ 1w′ 2w′ 3 wherew′ 1w′ 2w′ 3 is a (d−1, 1)-fit well-separated word (Definition 19.8) and w′ 2 is an infix ofw2 with|w′ 2|= 1 32m2 Len(d, 1). Proof. Let vj denote u0···uj as per Definitions 19.9 and 19.11. We begin by identifying a structure that repeats twice along the decomposition. Letb = 2Cov(d + 1,i ), and consider a complete graph on the ve...

work page

[46] [49]

supp(cu) = supp(cux) = supp(cuxy) = B: since the decomposition is a cover, then as noted in Definition 19.13, every reachable state is near some independent run, and in particular the equivalentdiff_typeb implies the same support

work page

[47] [50]

Then, the fact thatϕ(u) = ϕ(ux) iff ϕ(ux) = ϕ(uxy) is actually implied by the definition, in particular by Item 4 below

In the case of aϕ-increasing decomposition (Definition 19.9),ϕ(u)≤ϕ(ux)≤ϕ(uxy) follows immediately. Then, the fact thatϕ(u) = ϕ(ux) iff ϕ(ux) = ϕ(uxy) is actually implied by the definition, in particular by Item 4 below. In the case of aϕ-bounded decomposition, we already haveϕ(u) = ϕ(ux) = ϕ(uxy). Note that this is the only place where we treat the two t...

work page

[48] [51]

|x|≤1 mLsimp(dep(x) + 1) = 1 m Len(d + 1, 1): this is immediate from the requirement in Definition 19.7 that|w2|≤1 32m2 Len(d + 1,i )≤1 m Len(d + 1, 1) (recall that the inductive definition of Len(d + 1,i ) is with increasingi)

work page

[49] [52]

That is, setVj = supp(nearb(ρj,x )) for b = Cov(d + 1,i ) where I ={ρ1 <

We partitionB = V1∪...∪Vi according to the independent runs. That is, setVj = supp(nearb(ρj,x )) for b = Cov(d + 1,i ) where I ={ρ1 <... <ρi}. By Definition 19.13 this is indeed a partition. The gaps betweenVj and Vj+1 are higher than 4|S|mmax_eff(xy): byDefinition19.8theset I hasgapatleast 4m2(MaxWt(d)Len(d, 1)Len(d+ 1,i ) + Cov(d + 1,i )) Notice that|xy...

work page

[50] [53]

This concludes thatuxyv is an SSRI

The seamless baseline run exists by Definition 19.6. This concludes thatuxyv is an SSRI. LICS 2026 16:72 A Complexity Bound for Determinisation of Min-Plus Weighted Automata If dep(x)<d . In this case we treat the two types of decomposition separately. The case of aϕ-increasing decomposition is simple: we just restrict attention to an infix ofw2, as follo...

work page 2026

[51] [54]

Still by Definition 19.9 we haveϕ(w′ 1)≤ϕ(w′ 1w′

Note that there is such a suffix since|x|≥Len(d, 1) as a concatenation of uj’s, and by Definition 19.9. Still by Definition 19.9 we haveϕ(w′ 1)≤ϕ(w′ 1w′

work page

[52] [55]

TakeI′={ρ1}(i.e., arbitrarily choose a single independent run from I) sow′ 1w′ 2w′ 3 with I′is a (d−1, 1) fit word, as per Definition 19.7

(viewing w′ 2 as a prefix ofuj′). TakeI′={ρ1}(i.e., arbitrarily choose a single independent run from I) sow′ 1w′ 2w′ 3 with I′is a (d−1, 1) fit word, as per Definition 19.7. The case ofϕ-bounded decomposition is slightly more delicate. We still takew′ 2 to be the suffix ofx of length 1 32m2 Len(d, 1). This is possible since each part in the decomposition ...

work page

[53] [56]

We can now proceed as above by taking I′={ρ1}, and we are done

(although between them the potential may increase, but this does not concern us). We can now proceed as above by taking I′={ρ1}, and we are done. ◀ 19.1 From Well Separation to SSRI We now have the tools to show that given a well-separated word, we can obtain an SSRI from it. To do so, we develop an effective version of theZooming Techniqueintroduced in [...

work page

[54] [57]

w1w2w3 =uxyv whereuxyv is an SSRI withdep(x) =d and xy is an infix ofw2

work page

[55] [58]

w1w2w2 =w′ 1w′ 2w′ 3 wherew′ 1w′ 2w′ 3 is a (d−1, 1)-fit well-separated word (Definition 19.8) and w′ 2 is an infix ofw2 with|w′ 2|= 1 32m2 Len(d, 1). Proof. Let I ={ρ1 < ... < ρi}be the set of independent runs associated withw1w2w3 (Definition 19.2). Consider the behaviour ofϕ along w2 as per Definition 19.8. We claim there are two cases: eitherw1w2w3 is...

work page 2026

[56] [59]

t = Ramsey(GTyp(d + 1,i ), 3)

work page

[57] [60]

For every0≤j <j′≤t we have ψ(w1vj)> ψ(w1vj′)

work page

[58] [61]

For every1≤j≤t and prefixx of uj we have ψ(w1vj−1x)≥ψ(w1vj)

work page

[59] [63]

In contrast to Proposition 19.10, beingψ high amplitude is not a sufficient condition for having a decomposition

For every1≤j≤t we have|ui|≥GLen(d, 1). In contrast to Proposition 19.10, beingψ high amplitude is not a sufficient condition for having a decomposition. Indeed, it may be the case that the charge has unbounded growth, which then might cause the word to be very short. Fortunately, if this is the case, then Lemma 16.6 already gives us unbounded potential, w...

work page

[60] [64]

t = Ramsey(GTyp(d + 1,i ), 3) + 1

work page

[61] [65]

For every0<j <j′≤t we have ψ(w1vj) = ψ(w1vj′)

work page

[62] [66]

For every0≤j≤t we have that|uj|is a multiple ofE

work page

[63] [67]

|u0|≥GLen(d + 1,i + 1)

work page

[64] [68]

▶ Proposition 20.7(From bounded amplitude toψ-bounded decomposition)

For every 0 < j≤t and prefixx of uj with|x|multiple of E we have ψ(w1vjx)≥ ψ(w1vj+1). ▶ Proposition 20.7(From bounded amplitude toψ-bounded decomposition). Every ψ-bounded word has aψ-bounded (d,i )-decomposition. Proof. Consider a ψ-bounded word w1w2w3. By Definition 20.3 we have that |w2|= 1 32m2 GLen(d + 1,i ) and for every prefixx of w2 it holds that ...

work page 2026

[65] [69]

w′ 2 has atT + 1 prefixes z0,z 1,...,zT where ψ(w1u0zk) = ψ(w1)−P for everyk≥0 (where the prefixes are concatenations of thexjs)

work page

[66] [70]

Moreover, ifP =−GAmp(d+1,i )thenwetriviallyhavethefirstcase, provided |w′ 2|≥E·(T +1)

There is an infixw′′ 2 of w2 that isP−1-lower bounded, and|w′′ 2|≥E·t′ T+2. Moreover, ifP =−GAmp(d+1,i )thenwetriviallyhavethefirstcase, provided |w′ 2|≥E·(T +1). Recall thatt′≥(T + 2)2GAmp(d+1,i)+1 and thatw2 is GAmp(d + 1,i )-lower bounded. We can therefore apply the reasoning above inductively, starting fromP = GAmp(d + 1,i ). Since we divide the lengt...

work page

[67] [71]

w1w2w3 =uxyv whereuxyv is a GSRI withdep(x) =d, andxy is an infix ofw2

work page

[68] [72]

w1w2w2 = w′ 1w′ 2w′ 3 where w′ 1w′ 2w′ 3 is a ψ−(d−1, 1)-fit well-separated word (Defini- tion 20.3) and|w′ 2|= 1 32m2 Len(d, 1). Proof. Let vj denoteu0···uj as per Definitions 20.4 and 20.6. We begin by identifying a structure that repeats twice along the decomposition. Letb = 2GCov(d + 1,i ), and consider a complete graph on the vertices{1,...,t}. We de...

work page

[69] [73]

supp(cu) = supp(cux) = supp(cuxy) = B: since the decomposition is a cover, then as noted in Definition 20.8, every reachable state is near some independent run, and in particular the equivalentdiff_typeb implies the same support

work page

[70] [74]

Then, the fact thatψ(u) = ψ(ux) iff ψ(ux) = ψ(uxy) is actually implied by the definition, in particular by Item 4 below

In the case of aψ-decreasing decomposition (Definition 20.4),ψ(u)≥ψ(ux)≥ψ(uxy) follows immediately. Then, the fact thatψ(u) = ψ(ux) iff ψ(ux) = ψ(uxy) is actually implied by the definition, in particular by Item 4 below. In the case of aψ-bounded decomposition, we already haveψ(u) = ψ(ux) = ψ(uxy). Note that this is the only place where we treat the two t...

work page

[71] [75]

|x|≤1 mLgen(dep(x) + 1) = 1 m GLen(d + 1, 1): this is immediate from the requirement in Definition 20.2 that|w2|≤1 32m2 GLen(d+1,i )≤1 m GLen(d+1, 1) (recall that the inductive definition of GLen(d + 1,i ) is with increasingi)

work page

[72] [76]

That is, setVj = supp(nearb(ρj,x )) for b = GCov(d + 1,i ) where I ={ρ1 <...<ρi}

We partitionB = V1∪...∪Vi according to the independent runs. That is, setVj = supp(nearb(ρj,x )) for b = GCov(d + 1,i ) where I ={ρ1 <...<ρi}. By Definition 20.8 this is indeed a partition. The gaps betweenVj and Vj+1 are higher than 4|S|mmax_eff(xy)+H: byDefinition20.3theset I hasgapatleast 4m2(GMaxWt(d)GLen(d, 1)GLen(d+ 1,i ) + GCov(d + 1,i ) + H) Notic...

work page 2026

[73] [77]

This concludes thatuxyv is an GSRI

The seamless baseline run exists by Definition 20.1. This concludes thatuxyv is an GSRI. If dep(x)<d . In this case we treat the two types of decomposition separately. The case of aψ-decreasing decomposition is simple: we just restrict attention to an infix ofw2, as follows. Definew′ 2 to be the suffix ofx of length 1 32m2 GLen(d, 1), and letw′ 1,w′ 3 be ...

work page

[74] [78]

Still by Definition 20.4 we haveψ(w′ 1)≥ψ(w′ 1w′

Note that there is such a suffix since|x|≥GLen(d, 1) as a concatenation of uj’s, and by Definition 20.4. Still by Definition 20.4 we haveψ(w′ 1)≥ψ(w′ 1w′

work page

[75] [79]

TakeI′={ρ1}(i.e., arbitrarily choose a single independent run from I) sow′ 1w′ 2w′ 3 with I′is a ψ−(d−1, 1) fit word, as per Definition 20.2

(viewing w′ 2 as a prefix ofuj′). TakeI′={ρ1}(i.e., arbitrarily choose a single independent run from I) sow′ 1w′ 2w′ 3 with I′is a ψ−(d−1, 1) fit word, as per Definition 20.2. The case ofψ bounded decomposition is slightly more delicate. We still takew′ 2 to be the suffix ofx of length 1 32m2 GLen(d, 1). This is possible since each part in the decompositi...

work page

[76] [80]

We can now proceed as above by takingI′={ρ1}, and we are done

(although between them the charge may decrease, but this does not concern us). We can now proceed as above by takingI′={ρ1}, and we are done. ◀ 20.1 From Well Separation to GSRI We now have the tools to show that given aψ well-separated word, we can obtain a GSRI from it. To do so, we use a similar zooming argument as in Section 19.1. Note that the caveat...

work page

[77] [81]

w1w2w3 =uxyv whereuxyv is an GSRI withdep(x) =d and xy is an infix ofw2

work page

[78] [82]

forgotten

w1w2w2 = w′ 1w′ 2w′ 3 where w′ 1w′ 2w′ 3 is a ψ−(d−1, 1)-fit well-separated word (Defini- tion 20.3) andw′ 2 is an infix ofw2 with|w′ 2|= 1 32m2 GLen(d, 1). Proof. Assume there is no wordw′∈(Γ0 0)∗such that ϕ(w′)> H (otherwise we are done). Consider therefore a ψ−(d,i )-fit well-separated wordw1w2w3. Let I ={ρ1 < ... < ρi} be the set of independent runs a...

work page 2026