Two-Factor Decomposition of Deterministic One-Counter Automata Is Undecidable
Alp Eren Bütün · Zenodo (CERN European Organization for Nuclear Research) · 2026
A deterministic one-counter automaton (DOCA) presentation is 2-factor composite if its language is the intersection of the languages of two DOCAs having strictly fewer control states. We prove that deciding this property is undecidable. The result reaches the smallest nontrivial intersection budget: the hardness does not rely on an unbounded family of factors, nor even on three factors. The proof combines an elementary-abelian prime core with half-size quotient factors and an alternating-sentinel synchronization mechanism. A branch-labelled two-counter computation is encoded in two staggered phases. While one factor temporarily exposes its physical counter in order to perform an exact zero/decrement test, the other factor retains a positive sentinel and carries the missing lexical information; the roles then reverse. Consequently the two factors jointly enforce finite-control consistency and both source-counter trajectories, although neither factor stores both counters. If the source machine halts, a fixed suffix exposes a prime permutation-DFA section of full index. If it does not halt, two explicit quotient DOCAs, each with exactly half as many control states as the target, intersect to the target language exactly. Undecidability already holds for complete real-time, ε-free DOCAs with one work symbol above a permanent bottom marker, all control states final, and counter updates in {−1, 0, +1}. The 2-factor-composite instances produced by the reduction form a nonrecursively-enumerable set. Under the standard convention that factors need not be distinct, the same construction yields undecidability for every fixed factor budget k ≥ 2.