Source-linked AI summary
Two-State Max-Plus Comparison Is Decidable
Keigo Oka
TL;DR
The paper addresses the open two-state endpoint of max-plus automata comparison, following a known undecidability result at 553 states. It analyzes the one-dimensional projective gap of two-state dynamics, derives an exact one-counter realization, and proves decidability when only the right-hand automaton has at most two states. Consequently, comparison, equivalence, and positivity are decidable, although no complexity bound is claimed and the mechanism is specific to two states.
Problem
Comparison of max-plus automata is undecidable in general and was known undecidable at 553 states, leaving the range from 2 to 552 states—including two states—open.
Method
The proof uses one-dimensional projective dynamics to classify tail transitions and compile the two-state automaton into an exact one-counter model.
Results
It is decidable whether an arbitrary finite max-plus automaton A is pointwise bounded by a max-plus automaton B with at most two states.
Takeaways & Limitations
Two-state max-plus comparison, equivalence, and positivity are decidable, even when the left-hand automaton is unrestricted.
Takeaways & Limitations
No complexity bound is claimed, and the proof mechanism is specific to the one-dimensional projective geometry of two states.
Abstract
from arXiv · showhide
Daviaud, Guillon, and Merlet proved that comparison of max-plus automata is undecidable under a fixed state bound of 553 and explicitly left the range from 2 to 552 states open. We resolve the two-state endpoint. More strongly, given an arbitrary finite max-plus automaton $A$ and a max-plus automaton $B$ with at most two states, it is decidable whether $[\![A]\!](w)\leq [\![B]\!](w)$ for every word $w$. The structural reason is a one-dimensional projective normal form for two-state dynamics. Outside an effective bounded region, a transition has one of three tail behaviors: it propagates the unbounded projective gap with gap-independent height increment, forgets the gap with gap-independent height increment, or reads the gap magnitude into the height increment and then forgets it. In particular, any transition whose output depends on the unbounded gap necessarily destroys that gap. This yields an exact one-counter realization of $B$. Effective semilinearity of context-free Parikh images then reduces comparison to Presburger arithmetic. As a consequence, two-state max-plus comparison, equivalence, and positivity are decidable.
1 Introduction
The paper closes the two-state endpoint of the bounded-state max-plus comparison problem and proves a stronger asymmetric decidability theorem. Its proof exploits one-dimensional projective dynamics and reduces the two-state automaton to an exact one-counter model.
- Motivation: 553 states marked the known undecidability bound, while the range from 2 to 552 states remained open.The paper specifically identifies the two-state case as difficult and unresolved.
- Main result: It is decidable whether an arbitrary finite max-plus automaton A is pointwise bounded by a max-plus automaton B with at most two states.Only the right-hand automaton is restricted to two states.
- Main result: The result is stronger than resolving comparison when both automata have at most two states, because A may have arbitrarily many states.The restriction applies only to the right-hand automaton.
- Consequences: Two-state comparison, equivalence, and positivity are all decidable consequences of the theorem.Equivalence is obtained from both comparison directions, and positivity from comparison with a constant-zero automaton.
- Proof strategy: The proof uses one-dimensional projective dynamics whose tail behavior supports an exact one-counter realization.The key property is that gap-dependent height increments cannot preserve the unbounded projective gap.
2 Two-state projective dynamics
For a two-state automaton, projective normalization leaves a single signed gap as the unbounded state information. Max-plus transitions update this gap through explicit maxima, with finite, infinite, and signed-gap cases handled uniformly.
- Projective normal form: After subtracting the common height, every finite projective state is represented by a vector with one coordinate zero and the other equal to a signed gap.One-sided infinite gaps represent states where exactly one coordinate is finite.
- Projective normal form: The unbounded projective information is one-dimensional because it is determined by the difference between the two forward-vector entries.This is the structural simplification specific to two states.
- Transition dynamics: For a finite signed gap, max-plus multiplication computes the successor through two maxima, with corresponding conventions for infinite gaps.The successor gap is obtained by subtracting the two resulting coordinate maxima.
- Transition dynamics: Subtracting the input height isolates a height cocycle that records the transition's increment independently of the normalized projective state.The cocycle is used alongside the gap update in the transition analysis.
- Transition dynamics: The transition formulas apply when the successor is nondead, while dead successors require separate support handling.The stated formulas are conditioned on a nondead successor.
3 The tail trichotomy
Beyond an effective bound K, every two-state transition has one of three tail behaviors: propagate, forget, or read-and-forget. The key restriction is that reading the unbounded gap into the height increment prevents that gap from being propagated.
- 3 The tail trichotomy: For gaps with magnitude n > K, each nondead letter transition is classified as propagate, forget, or read-and-forget.The propagate case updates n affinely as n′ = n + s; the other two make the successor projective state independent of n.
- 3 The tail trichotomy: In the propagate case, the successor gap is n′ = n + s and the height increment is a fixed constant independent of n.The shift s and successor tail side are fixed for the letter and tail side.
- 3 The tail trichotomy: In the forget case, the successor projective state and height increment are both independent of the old gap magnitude.The successor is either an infinite-gap state or a bounded finite-gap state.
- 3 The tail trichotomy: In the read-and-forget case, the height increment depends on the unbounded gap magnitude, but the successor projective state does not.For an inactive active-row pair, the height increment has the form C_M − z while the successor projective class is independent of z.
- 3 The tail trichotomy: Thus, any transition that reads the unbounded gap magnitude into the output necessarily destroys that magnitude for future projective evolution.The structural statement is a prohibition on simultaneously reading and propagating an unbounded magnitude, not a literal retain/read dichotomy.
- 3 The tail trichotomy: The one-dimensional result is specific to two states; with three states, two projective differences can coexist and one can be read while another is retained.This identifies the structural boundary of the tail argument.
4 Exact compilation to one counter
The tail classification is compiled into an effectively constructible deterministic one-counter transducer that exactly realizes the two-state automaton’s output. Its finite control handles bounded and infinite projective states, while the counter stores large gap magnitudes.
- 4 Exact compilation to one counter: An effectively constructible one-counter transducer T_B exactly realizes B on every word.It has no successful computation when B outputs −∞, and otherwise has a successful computation emitting exactly [[B]](w).
- 4 Exact compilation to one counter: Finite control represents bounded gaps and infinite-gap states, while the counter stores the magnitude n > K in tail states.The counter is zero in B_z, I+, and I−, and equals n in T+ and T−.
- 4 Exact compilation to one counter: For bounded current gaps, the construction uses finite lookup tables to obtain the exact successor projective state and height increment.If a lookup reaches a tail gap, the transducer loads its magnitude through unit counter increments.
- 4 Exact compilation to one counter: In propagate cases, the transducer emits a fixed constant and updates the counter by the fixed shift s without blocking because n > K > |s|.A deterministic probe distinguishes whether the updated counter has fallen back into the bounded region.
- 4 Exact compilation to one counter: Forget cases drain the counter silently, whereas read-and-forget cases drain it while emitting −1 per decrement, producing the required c − n contribution.Both routines restore the counter-zero invariant because their successor projective states are bounded or infinite.
- 4 Exact compilation to one counter: The construction is deterministic, with routines built from unit counter operations, zero tests, and fixed integer emissions.Correctness follows by induction on input prefixes, preserving the exact projective state, height, and successful-computation behavior.
5 Deciding comparison
Comparison is reduced to an effectively semilinear condition by synchronizing the arbitrary automaton with an exact one-counter transducer for the two-state automaton. Presburger decidability then establishes comparison, equivalence, and positivity results.
- Support separation: Finite-support mismatches are decidable immediately because each automaton’s finite-support language is regular.A word finite for A but equal to −∞ for B directly violates comparison.
- One-counter product: The construction synchronizes A with a functional one-counter transducer for B, encoding A’s finite initial, final, and transition weights.Internal transducer transitions leave A’s state unchanged, while letter-consuming transitions synchronize with matching finite-weight transitions of A.
- Semilinear reduction: Successful computations form an effectively constructible one-counter language whose Parikh image is effectively semilinear.Fresh symbols label product transitions, and constructive Parikh’s theorem supplies effective semilinearity.
- Violation criterion: A comparison violation exists exactly when a successful trace has a Parikh vector satisfying the weighted inequality condition.The synchronized trace represents an input word and an accepting run of A, so the inequality witnesses a genuine violation.
- Decidability consequences: Because the condition is existential Presburger arithmetic over an effectively given semilinear set, comparison is decidable.Equivalence follows from two comparison directions, and positivity follows by comparing against the one-state zero automaton.
6 Position relative to prior work
The paper closes the two-state comparison endpoint left open by prior bounded-state work, using a different restriction profile from nearby decidable problems. Its theorem allows unrestricted alphabets and left-hand automata while bounding only the right-hand automaton to two states.
- Prior boundary: Prior work established undecidability at 553 states and left the range from 2 to 552 states open.Theorem 1.1 resolves the two-state endpoint of that interval.
- Distinct mechanism: The proof differs from restrictions based on finite ambiguity, unary alphabets, or determinisability.Its decisive mechanism is an exact one-counter reduction.
- Scope: The alphabet and left-hand automaton are unrestricted, while only the right-hand automaton is limited to two states.This is the structural scope distinguishing the result from nearby decidable restrictions.
- Literature status: A literature review through September 1, 2026 reported no earlier resolution of the two-state case or equivalent arbitrary-left/two-state-right containment theorem.The review explicitly declines to make an absolute historical-priority claim.
7 Reproducibility and provenance
The manuscript provides a maintained version, regression code, and dated literature review. The code checks finite projective behavior and evaluator agreement, while the infinite theorem rests on the written proof.
- Materials: A maintained manuscript, public regression code, and dated literature review are available in the Exact Interaction Geometry research repository.
- Research provenance: The residual/interface viewpoint motivated isolating the one-dimensional projective gap and testing whether transitions can expose and preserve its magnitude.The theorem itself is ordinary weighted-automata mathematics and does not depend on EIG.
- Verification: The regression script checks projective formulas, classifies finite letter tails, and compares direct and projective/counter evaluation on hundreds of thousands of finite words.Finite enumeration supports regression only; the infinite theorem rests on the proof.
AI-assisted research disclosure
The work was developed through AI-assisted mathematical research, with models contributing to discovery, drafting, verification, and literature-review support. The author retains responsibility, and the written proof—not regression code or provenance—supports the theorem.
- AI-assisted research contributed to theorem discovery, proof drafting, verifier generation, and literature-review support.
- The author directed the research programme and takes responsibility for the manuscript.
- The result is intended to stand on the written proof, while model-assisted review and regression code provide provenance or finite regression rather than independent mathematical evidence.