Unambiguisability and Register Minimisation of Min-Plus Models

TL;DR

The work resolves a long-standing open problem by showing that WFA unambiguisability over the tropical semiring is decidable via a reduction to determinisation, leveraging recent results on tropical determinisation. It also proves that counter minimisation for tropical CRAs is undecidable, even with a fixed number of registers, by relating CRA registers to WFA width and applying a width-minimisation undecidability construction. By introducing U-type gap witnesses and connecting them to D-type gap witnesses, the authors establish a tight reduction framework between unambiguisability and determinisability. The results delineate a sharp boundary between decidable and undecidable forms of nondeterminism in tropical automata, with implications for both theory and applications involving resource-optimized automata. The paper also maps a precise equivalence between k-CRAs and width-k WFAs, providing a unified lens for studying nondeterminism minimisation across models.

Abstract

We study the unambiguisability problem for min-plus (tropical) weighted automata (WFAs), and the counter-minimisation problem for tropical Cost Register Automata (CRAs), which are expressively-equivalent to WFAs. Both problems ask whether the "amount of nondeterminism" in the model can be reduced. We show that WFA unambiguisability is decidable, thus resolving this long-standing open problem. Our proof is via reduction to WFA determinisability, which was recently shown to be decidable. On the negative side, we show that CRA counter minimisation is undecidable, even for a fixed number of registers (specifically, already for 7 registers).

Figures (5)

• Figure 1: Contradiction scenarios for \ref{['sec:unambig implies bounded gap']} (the $s$ component is omitted). In \ref{['fig:unambig to bounded gap negative case']} the run $\chi$ becomes too negative, so that a short suffix induces a negative run to $q'_2$. In \ref{['fig:unambig to bounded gap positive case']}, the run $\rho$ decreases too much between $p_1$ and $p_2$, causing a negative cycle, which again leads to a negative run to $q'_2$.
• Figure 2: \ref{['fig:unambiguisable WFA']} has gaps bounded by $2$. In \ref{['fig:unambiguisation construction']} we demonstrate the construction of \ref{['sec:bounded gap implies unambig']}, with the order $q_1\preceq q_2\preceq q_3 \preceq q_4\preceq q_5$. Crucially, note that the transition from $q_3$ to $q_5$ is removed in $\mathcal{U}$. This is due to the consistency check, and since $q_3\preceq q_4$.
• Figure 3: $B$-gap witness. The vertical height represents the weight. After reading $x$, the run $\chi$ is minimal, and $\rho$ is far above it. Upon reading $y$, $\rho$ continues to become a minimal run. In $\mathfrak{U}$-type witnesses, $\chi$ must also continue to become accepting. In $\mathfrak{D}$-type, there is no requirement on $\chi$ (but $q_1$ can reach $F$ via some word, since the automaton is trim).
• Figure 4: The reduction of \ref{['thm:main reduction']}. The WFA $\mathcal{A}$ is unambiguisable (as it is already unambiguous). The reduction output $\mathcal{D}$ adds the commitments and updates to the transitions. $\bot$ markings are omitted for clarity. For example, in order to take the $q\to p$ transition, the commitment specifies that $p$ leads to an accepting state, and that $r$ does not, thus fixing an explicit run DAG. Note that $\mathcal{D}$ is determinisable (as it is already deterministic).
• Figure 5: Construction of the WFA $\mathcal{A}'$ from $\mathcal{A}$. The letter $\sigma$ represents all "non-killing" letters in the transitions. Killing letters lead to $\times$. Intuitively, we start either at $\mathcal{A}$ or at $q_a$. In $q_a$ there is a self loop with weight $0$ on everything except $b$. From $q_0$ we can run as $\mathcal{A}$, but also move to the $\Circled{i}$ components on $\$$. In state $q_{\Circled{i}}$ we self loop with weight $-1$ on $\Circled{i}$, and with $0$ on all other letters except $\cancel{\Circled{i}}$. If $\mathcal{A}$ is unbounded, there is a self loop on $q_0$ with the word $x@$.

Theorems & Definitions (22)

• Remark 1: On initial and final weights and states
• Proposition 3
• Proposition 4
• Definition 5: $\mathfrak{U}$-type $B$-Gap Witness
• Theorem 6
• Example 7
• Lemma 8
• Lemma 9
• Definition 10: $\mathfrak{D}$-type $B$-Gap Witness
• Theorem 11