Language Equivalence Between Deterministic and Nondeterministic One-Counter Nets Is Decidable
Alp Eren Bütün · Zenodo (CERN European Organization for Nuclear Research) · 2026
We prove that language equivalence between deterministic and nondeterministic one-counter nets is decidable. The work grew out of our earlier research on deterministic pushdown normalization, residual and quotient geometry, shortest completions, and decision and decomposition problems for deterministic one-counter automata, including the Prime-DOCA and Two-Factor DOCA projects. The proof develops exact forward envelopes and backward completion requirements, together with well-quasi-order, source-sink, max-plus, bounded-return, terminal-ladder, and LOW-state techniques, to obtain a computable small-witness bound for the difficult inclusion direction. Combined with the known deterministic-right inclusion result, this yields a decision procedure for language equivalence. The problem is recorded as Automata Exchange Problem 24.04(B) and was explicitly discussed as open by Patrick Totzke in 2023. Our literature search through September 2026 found no public paper or preprint resolving the problem. The corresponding zero-test version, where the deterministic machine is a one-counter automaton rather than a one-counter net, remains the natural next frontier.