A Complexity Bound for Determinisation of Min-Plus Weighted Automata

TL;DR

This work provides the first primitive-recursive complexity bound for the determinisation problem of min-plus WFAs, placing the problem within the Fast-Growing Hierarchy and delivering a constructive, finite-alphabet framework. The authors replace non-constructive Ramsey pumping with quantitative zooming and Separated Repeating Infixes (SRI), coupled with a Baseline-Augmented Construction to reason about run trees and gaps in a finite, tractable setting. Central innovations include effective cactus letters, baseline-shift invariants, and a robust decomposition toolkit (SSRI/GSRI) that either yields witnesses or shortens words while preserving key potential/charge properties. The approach yields a concrete algorithm: compute GAmp(|S|,0), build a bounded-gap automaton, and test equivalence to decide determinisability; GAmp is shown to be in level $\mathbf{F}_6$, ensuring primitive-recursive (non-elementary) complexity. This advances practical understanding of determinisation and provides a versatile toolkit (Zooming, SRI, cactus techniques) potentially reusable for related counter-based models.

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 significantly simplifies the previous decidability argument and provides a tighter analysis, thus serving as a critical step towards a tight complexity bound.

Figures (23)

• Figure 1: A tropical WFA that assigns to $w\in \{a,b\}^*$ the minimum between the number of $a$'s and $b$'s in $w$.
• Figure 2: A $B$-gap witness: upon reading $x$, the minimal run on $x$ is at least $B$ below another run, but after reading $y$, the upper run becomes minimal.
• Figure 3: Cactus letters: $\alpha_1$ is of depth $1$ (and its inner word is of depth $0$). The word $u_1\alpha_1v_1$ (left) forms a cactus letter $\alpha_2$ of depth $2$ (center). Then, $u_2\alpha_2v_2$ forms a cactus letter $\alpha_3$ of depth $3$ (right). Notice that $u_2$ contains also the cactus letter $\alpha_4$.
• Figure 4: Shifting the baseline: $\rho_{\mathrm{base}}$ becomes the baseline run instead of $\pi$; the word $w$ changes to $w'=\mathsf{bshift}[{w}/{\rho_{\mathrm{base}}}]$, and the runs $\pi$ and $\tau$ change accordingly to $\pi' = \mathsf{bshift}[{\pi}/{\rho_{\mathrm{base}}}]$ and $\tau'=\mathsf{bshift}[{\tau}/{\rho_{\mathrm{base}}}]$, respectively. The shifted runs keep their relative distance from one another.
• Figure 5: An SRI. After reading $u$, the configuration is separated to sub-configurations corresponding to the $V_i$. Reading $x$ maintains this partition and the exact distances within each set. The same holds for $y$, but with different shifts. The gaps between the sub-configurations are much larger than the effect of $x$ and $y$. On the top is a positive SRI: all sub-configurations are trending upwards. On the bottom is a negative SRI: There exists a sub-configuration (the upper one in the figure) with a downwards slope.

Theorems & Definitions (167)

• Definition 2.1: $B$-Gap Witness
• Theorem 2.2: filiot2017delayalmagor2026determinization
• Lemma 3.1
• proof : Proof Sketch
• Lemma 4.1
• Definition 5.1
• Lemma 5.2
• Proposition 6.1
• proof : Proof Sketch
• Proposition 6.2