Exponential state costs for two-way automata

Proves exponential lower bounds both for complementing two-way nondeterministic finite automata and for simulating one-way nondeterministic automata by two-way deterministic ones. The latter resolves the Sakoda–Sipser state-succinctness conjecture over growing finite alphabets; both results rule out polynomial state bounds independent of alphabet size. (Lean)

Manuscripts (2)

An exponential state lower bound for two-way nondeterministic complementation

September 25, 2026 · source · Lean formalization available · cite as \cite{OAI:An-exponential-state-lower-bound-for-two-way-nondeterministic-complementation-September-25-2026}

We prove that two-way nondeterministic finite automata cannot be complemented with a polynomial number of states independent of the alphabet. For each n ≥ 4 we construct an n-state automaton over a finite alphabet whose complement requires at least \tfrac12 2^{\lfloor(n-4)/127\rfloor}-1 states.

An exponential two-way deterministic state lower bound for one-way liveness

September 25, 2026 · source · Lean formalization available · cite as \cite{OAI:An-exponential-two-way-deterministic-state-lower-bound-for-one-way-liveness-September-25-2026}

One-way liveness on h points accepts a word of binary relations when their ordered product is nonempty. For every h ≥ 2, it has a nondeterministic automaton with h+3 states and no left moves, whereas every equivalent s-state two-way deterministic automaton satisfies 4(s+2)^2\ge2^{\lfloor(h-2)/31\rfloor}. Partial transition rules, stay moves, and nonaccepting infinite computations are allowed. The alphabets are finite and grow with h, so the result rules out an alphabet-independent polynomial state bound for deterministic two-way simulation, already for one-way nondeterministic sources.

Result 129 · Theoretical computer science. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.