Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Determinization of Min-Plus Weighted Automata is Decidable

Shaull Almagor, Guy Arbel, Sarai Sheinvald

TL;DR

The paper resolves the decidability of the determinization problem for min-plus (tropical) weighted finite automata by introducing a comprehensive toolbox to analyze nondeterministic run-structures. It combines a Baseline-Augmented Subset Construction with a cactus-based framework of stable cycles, cactus letters, and unfolding to pump and fold runs, enabling a precise gap-based characterization of determinizability. Central to the approach are the notions of potential and charge, which quantify how high runs can climb relative to the baseline and control growth across words; Ramsey-type results and zooming/fair decompositions are used to extract structured infixes that yield either unbounded potential or a concrete witness. Collectively, these ideas establish a decidability result (without immediate complexity bounds) and set the stage for potential future advances toward complexity characterization, with broad implications for tropical automata theory and related quantitative models.

Abstract

We show that the determinization problem for min-plus (tropical) weighted automata is decidable, thus resolving this long-standing open problem. In doing so, we develop a new toolbox for analyzing and reasoning about the run-structure of nondeterministic automata.

Determinization of Min-Plus Weighted Automata is Decidable

TL;DR

The paper resolves the decidability of the determinization problem for min-plus (tropical) weighted finite automata by introducing a comprehensive toolbox to analyze nondeterministic run-structures. It combines a Baseline-Augmented Subset Construction with a cactus-based framework of stable cycles, cactus letters, and unfolding to pump and fold runs, enabling a precise gap-based characterization of determinizability. Central to the approach are the notions of potential and charge, which quantify how high runs can climb relative to the baseline and control growth across words; Ramsey-type results and zooming/fair decompositions are used to extract structured infixes that yield either unbounded potential or a concrete witness. Collectively, these ideas establish a decidability result (without immediate complexity bounds) and set the stage for potential future advances toward complexity characterization, with broad implications for tropical automata theory and related quantitative models.

Abstract

We show that the determinization problem for min-plus (tropical) weighted automata is decidable, thus resolving this long-standing open problem. In doing so, we develop a new toolbox for analyzing and reasoning about the run-structure of nondeterministic automata.

Paper Structure

This paper contains 109 sections, 92 theorems, 171 equations, 32 figures, 1 table.

Table of Contents

  1. Introduction
  2. WFAs, Determinizability and Gaps
  3. WFAs
  4. Characterizing Determinizability by Gaps
  5. Constructions and Definitions
  6. The Baseline Augmented Construction (\ref{['sec:augmented construction']})
  7. Cactus Letters (\ref{['sec:stable cycles and bounded behaviours', 'sec:cactus extension']})
  8. A bound on chain depth
  9. Baseline shifts
  10. Cactus unfolding
  11. Potential and Charge (\ref{['sec:dominance and potential']})
  12. A Witness for Nondeterminizability (\ref{['sec:witness']})
  13. Nondeterminizable WFAs Have a Witness (\ref{['sec:final nondet implies witness']})
  14. If $\mathcal{A}$ is Nondeterminizable, Then the Potential is Unbounded
  15. If the Potential is Unbounded, then $\widehat{\mathcal{A}}_\infty$ Has a Witness
  16. ...and 94 more sections

Key Result

Theorem 2.1

$\mathcal{A}$ is nondeterminizable if and only if for every $B\in \mathbb{N}$, there is a $B$-gap witness.

Figures (32)

  • 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 tropical WFA $\mathcal{A}$. All the states are initial. \ref{['fig:abs:running dag example']} depicts a run DAG of $\mathcal{A}$.
  • Figure 3: After reading $bab^2ab^3ab^4ab^5a$, we arrive at the configuration $(0,0,5)$, as depicted. We then show how reading $b^6a$ increases the weight of $r$ by $1$. Note that this cannot be done with any shorter word.
  • Figure 4: A $B$-gap witness.
  • Figure 5: A stable cycle. The baseline $r$ is highlighted.
  • ...and 27 more figures

Theorems & Definitions (228)

  • Theorem 2.1
  • Example 1
  • Remark 8.1: On initial and final weights, and accepting states
  • Definition 8.3: $B$-Gap Witness
  • Theorem 8.4
  • Definition 9.1: Baseline States and Baseline Runs
  • Proposition 9.3
  • proof
  • Corollary 9.4
  • Remark 9.6
  • ...and 218 more