pith. sign in

arxiv: 2512.09484 · v2 · submitted 2025-12-10 · 💻 cs.FL

Unambiguisability and Register Minimisation of Min-Plus Models

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

Pith reviewed 2026-05-16 23:43 UTC · model grok-4.3

classification 💻 cs.FL
keywords unambiguisabilitymin-plus automataweighted automatacost register automatadecidabilitycounter minimisationtropical semiring
0
0 comments X

The pith

Unambiguisability for min-plus weighted automata is decidable by reduction to determinisability.

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

The paper shows that it is possible to decide whether a given min-plus weighted automaton has an equivalent unambiguous version. The proof works by constructing a reduction to the determinisability problem, which had already been shown decidable. This settles a longstanding open question for the tropical semiring. On the other side, the paper proves that minimizing the number of counters in the equivalent cost register automaton model is undecidable, and the undecidability already holds when the number of registers is fixed at seven. A reader would care because these models describe quantitative properties of systems, and removing nondeterminism or registers affects what properties can be checked algorithmically.

Core claim

We show that WFA unambiguisability is decidable via reduction to WFA determinisability. On the negative side, we show that CRA counter minimisation is undecidable, even for a fixed number of registers (specifically, already for 7 registers).

What carries the argument

The reduction from the unambiguisability question to the determinisability question for min-plus weighted automata.

Load-bearing premise

The reduction from unambiguisability to determinisability correctly preserves the existence of an equivalent unambiguous automaton, and the prior decidability result for determinisability applies without additional restrictions on the min-plus semiring.

What would settle it

An explicit min-plus automaton for which the constructed reduction instance is determinisable but the original automaton has no equivalent unambiguous version, or vice versa.

read the original 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).

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.

Referee Report

2 major / 2 minor

Summary. The paper studies unambiguisability for min-plus weighted finite automata (WFAs) and counter-minimisation for equivalent tropical cost register automata (CRAs). It claims that WFA unambiguisability is decidable via a reduction to the recently shown decidable WFA determinisability problem, and that CRA counter minimisation is undecidable even when restricted to a fixed number of 7 registers.

Significance. Resolving the long-standing open problem of deciding unambiguisability for min-plus WFAs would be a significant contribution to automata theory over semirings. The positive result is obtained by a clean reduction to an externally established decidability result, which is a strength when the mapping is verified. The negative result on fixed-register CRAs provides a concrete bound that sharpens the computational complexity picture for register minimisation. If the reduction is shown to preserve equivalence under the idempotent min-plus operations, the work advances the decidability landscape for tropical models.

major comments (2)
  1. [Proof of decidability theorem (reduction construction)] The reduction from unambiguisability to determinisability (proof of the main positive theorem) must explicitly confirm preservation of equivalence for the min-plus semiring (R∪{∞}, min, +). The construction mapping WFA A to WFA B such that A is unambiguous iff B is determinizable should include a lemma verifying that multiple equal-weight accepting paths are encoded without introducing spurious nondeterminism or altering tropical sums, as unique path decomposition properties do not hold under idempotent addition.
  2. [Undecidability result for fixed registers] The undecidability reduction for CRA counter minimisation with exactly 7 registers requires a detailed encoding from the source undecidable problem (e.g., a register-machine halting problem or PCP variant). The manuscript should specify how register updates are restricted to min-plus operations while staying within the fixed register bound, to ensure the reduction does not implicitly rely on additional registers or non-tropical operations.
minor comments (2)
  1. [Abstract and introduction] The abstract states the undecidability holds 'already for 7 registers'; consider repeating this concrete bound in the introduction to emphasize the result's strength.
  2. [Preliminaries] Notation for the min-plus semiring and CRA register updates should be introduced with a short table or example in §2 to aid readers unfamiliar with tropical automata.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their thorough review and valuable suggestions. We address the major comments below and plan to revise the manuscript accordingly to incorporate the requested clarifications.

read point-by-point responses

  1. Referee: [Proof of decidability theorem (reduction construction)] The reduction from unambiguisability to determinisability (proof of the main positive theorem) must explicitly confirm preservation of equivalence for the min-plus semiring (R∪{∞}, min, +). The construction mapping WFA A to WFA B such that A is unambiguous iff B is determinizable should include a lemma verifying that multiple equal-weight accepting paths are encoded without introducing spurious nondeterminism or altering tropical sums, as unique path decomposition properties do not hold under idempotent addition.

    Authors: We agree that the reduction requires an explicit lemma to confirm preservation under the min-plus semiring. The current manuscript outlines the construction in Section 3, but to address this, we will add Lemma 3.4 in the revised version. This lemma will verify that the mapping from WFA A to B preserves the property that A has multiple equal-weight accepting paths if and only if B has nondeterministic choices leading to the same min-weight, without introducing spurious paths. Since the semiring is idempotent, the min operation ensures that equal weights do not alter the sum, and the encoding uses state duplication to track path uniqueness without extra nondeterminism. revision: yes

  2. Referee: [Undecidability result for fixed registers] The undecidability reduction for CRA counter minimisation with exactly 7 registers requires a detailed encoding from the source undecidable problem (e.g., a register-machine halting problem or PCP variant). The manuscript should specify how register updates are restricted to min-plus operations while staying within the fixed register bound, to ensure the reduction does not implicitly rely on additional registers or non-tropical operations.

    Authors: We appreciate this comment and will provide more details on the reduction. The proof in Section 4 reduces from the Post Correspondence Problem (PCP), which is undecidable. We will expand the description to show explicitly how each PCP tile is simulated using min-plus operations on exactly 7 registers: two for tracking the current string lengths or positions, and others for encoding the choices and matches via min and additions of constants. All updates are of the form r := min(r, r + c) or similar, staying within the tropical semiring, and no extra registers are introduced. This ensures the reduction is valid for the fixed bound of 7. revision: yes

Circularity Check

0 steps flagged

No significant circularity; claims rest on external decidability and standard reductions.

full rationale

The paper proves decidability of WFA unambiguisability via a reduction to the decidability of WFA determinisability (cited as recently established in prior independent work) and proves undecidability of CRA counter minimisation via reduction from a known undecidable problem. No quoted step in the provided abstract or description reduces a central claim by construction to the paper's own fitted parameters, self-definitions, or unverified self-citations. The derivation chain is self-contained against external benchmarks and does not exhibit any of the enumerated circular patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The positive result rests on the external fact that WFA determinisability is decidable; the negative result rests on standard undecidability reductions from known undecidable problems in automata theory. No free parameters or invented entities are introduced.

axioms (1)
  • domain assumption WFA determinisability is decidable
    Invoked as the target of the reduction; cited as recently shown decidable.

pith-pipeline@v0.9.0 · 5417 in / 1223 out tokens · 28706 ms · 2026-05-16T23:43:30.242928+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

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

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

22 extracted references · 22 canonical work pages

  1. [1]

    Determinization of min-plus weighted automata is decidable

    Shaull Almagor, Guy Arbel, and Sarai Sheinvald. Determinization of min-plus weighted automata is decidable. In Symposium on Discrete Algorithms (SODA 2025, to appear) . SIAM, 2025. URL: https://arxiv.org/abs/2503.23826

    work page arXiv 2025

  2. [2]

    What's decidable about weighted automata? Information and Computation , 282:104651, 2020

    Shaull Almagor, Udi Boker, and Orna Kupferman. What's decidable about weighted automata? Information and Computation , 282:104651, 2020. Special issue on 9th International Workshop Weighted Automata: Theory and Applications (WATA 2018). URL: https://www.sciencedirect.com/science/article/pii/S0890540120301395, https://doi.org/10.1016/j.ic.2020.104651 doi:1...

    work page doi:10.1016/j.ic.2020.104651 2020

  3. [3]

    P \' e rez

    Shaull Almagor, Micha \" e l Cadilhac, Filip Mazowiecki, and Guillermo A. P \' e rez. Weak cost register automata are still powerful. Int. J. Found. Comput. Sci. , 31(6):689--709, 2020. https://doi.org/10.1142/S0129054120410026 doi:10.1142/S0129054120410026

    work page doi:10.1142/s0129054120410026 2020

  4. [4]

    Regular functions and cost register automata

    Rajeev Alur, Loris DAntoni, Jyotirmoy Deshmukh, Mukund Raghothaman, and Yifei Yuan. Regular functions and cost register automata. In 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science , pages 13--22. IEEE, 2013

    work page 2013

  5. [5]

    Computing the linear hull: Deciding deterministic? and unambiguous? for weighted automata over fields

    Jason P Bell and Daniel Smertnig. Computing the linear hull: Deciding deterministic? and unambiguous? for weighted automata over fields. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , pages 1--13. IEEE, 2023

    work page 2023

  6. [6]

    Minimizing cost register automata over a field

    Yahia Idriss Benalioua, Nathan Lhote, and Pierre-Alain Reynier. Minimizing cost register automata over a field. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024) , pages 23--1. Schloss Dagstuhl--Leibniz-Zentrum f \"u r Informatik, 2024

    work page 2024

  7. [7]

    Ambiguity in graphs and expressions

    Ronald Book, Shimon Even, Sheila Greibach, and Gene Ott. Ambiguity in graphs and expressions. IEEE Transactions on Computers , 100(2):149--153, 1971

    work page 1971

  8. [8]

    Quantitative languages

    Krishnendu Chatterjee, Laurent Doyen, and Thomas A Henzinger. Quantitative languages. ACM Transactions on Computational Logic (TOCL) , 11(4):1--38, 2010

    work page 2010

  9. [9]

    Register complexity and determinisation of max-plus automata

    Laure Daviaud. Register complexity and determinisation of max-plus automata. ACM SIGLOG News , 7(2):4--14, 2020

    work page 2020

  10. [10]

    Handbook of weighted automata

    Manfred Droste, Werner Kuich, and Heiko Vogler. Handbook of weighted automata . Springer Science & Business Media, 2009

    work page 2009

  11. [11]

    On delay and regret determinization of max-plus automata

    Emmanuel Filiot, Isma \"e l Jecker, Nathan Lhote, Guillermo A P \'e rez, and Jean-Fran c ois Raskin. On delay and regret determinization of max-plus automata. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , pages 1--12. IEEE, 2017

    work page 2017

  12. [12]

    Hashiguchi

    K. Hashiguchi. Limitedness theorem on finite automata with distance functions. Journal of computer and system sciences , 24(2):233--244, 1982

    work page 1982

  13. [13]

    Hashiguchi

    K. Hashiguchi. New upper bounds to the limitedness of distance automata. Theoretical Computer Science , 233(1-2):19--32, 2000

    work page 2000

  14. [14]

    Determinisation and unambiguisation of polynomially-ambiguous rational weighted automata

    Isma \"e l Jecker, Filip Mazowiecki, and David Purser. Determinisation and unambiguisation of polynomially-ambiguous rational weighted automata. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science , pages 1--13, 2024

    work page 2024

  15. [15]

    Distance desert automata and the star height problem

    Daniel Kirsten. Distance desert automata and the star height problem. RAIRO-Theoretical Informatics and Applications , 39(3):455--509, 2005

    work page 2005

  16. [16]

    Deciding unambiguity and sequentiality of polynomially ambiguous min-plus automata

    Daniel Kirsten and Sylvain Lombardy. Deciding unambiguity and sequentiality of polynomially ambiguous min-plus automata. In 26th International Symposium on Theoretical Aspects of Computer Science STACS 2009 , pages 589--600. IBFI Schloss Dagstuhl, 2009

    work page 2009

  17. [17]

    D. Krob. The equality problem for rational series with multiplicities in the tropical semiring is undecidable. International Journal of Algebra and Computation , 4(3):405--425, 1994

    work page 1994

  18. [18]

    Leung and V

    H. Leung and V. Podolskiy. The limitedness problem on distance automata: Hashiguchi's method revisited. Theoretical Computer Science , 310(1-3):147--158, 2004

    work page 2004

  19. [19]

    Compact representations by finite-state transducers

    Mehryar Mohri. Compact representations by finite-state transducers. In 32nd Annual Meeting of the Association for Computational Linguistics , pages 204--209, 1994

    work page 1994

  20. [20]

    Finite-state transducers in language and speech processing

    Mehryar Mohri. Finite-state transducers in language and speech processing. Computational linguistics , 23(2):269--311, 1997

    work page 1997

  21. [21]

    Introduction to probabilistic automata

    Azaria Paz. Introduction to probabilistic automata . Academic Press, 2014

    work page 2014

  22. [22]

    On the definition of a family of automata

    Marcel Paul Sch \"u tzenberger. On the definition of a family of automata. Inf. Control. , 4(2-3):245--270, 1961

    work page 1961