Theoretical computer science · Result 129

Exponential state costs for two-way automata

2 papersLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 2

An exponential state lower bound for two-way nondeterministic complementation

OpenAI · 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.

Read PDF Download Source

Cite

@misc{OAI:An-exponential-state-lower-bound-for-two-way-nondeterministic-complementation-September-25-2026,
  author = {{OpenAI}},
  title = {{An exponential state lower bound for two-way nondeterministic complementation}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/An-exponential-state-lower-bound-for-two-way-nondeterministic-complementation-September-25-2026/paper.pdf}{OAI:An-exponential-state-lower-bound-for-two-way-nondeterministic-complementation-September-25-2026}},
  year = {2026}
}

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

OpenAI · 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.

Read PDF Download Source

Cite

@misc{OAI:An-exponential-two-way-deterministic-state-lower-bound-for-one-way-liveness-September-25-2026,
  author = {{OpenAI}},
  title = {{An exponential two-way deterministic state lower bound for one-way liveness}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/An-exponential-two-way-deterministic-state-lower-bound-for-one-way-liveness-September-25-2026/main.pdf}{OAI:An-exponential-two-way-deterministic-state-lower-bound-for-one-way-liveness-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The paper asks how many states are needed to complement or determinize two-way nondeterministic finite automata. The formalization gives, for every \(n\ge4\), an explicit \(n\)-state automaton whose complement requires at least \(\tfrac12 2^{\lfloor(n-4)/127\rfloor}-1\) states. For the same family of relational languages and every \(n\ge131\), every equivalent deterministic two-way automaton requires at least \(\tfrac12 2^{\lfloor(n-4)/127\rfloor}\) states.

The alphabet grows with \(n\), so neither complementation nor determinization has a polynomial state bound uniform over alphabets. The model has two endmarkers, left, right, and stay moves, and acceptance by a finite run. The separate results about one-way liveness and the Sakoda–Sipser problem are outside this scope.

The formalization gives a family of one-way nondeterministic automata with \(h+3\) states whose languages require exponentially many states for two-way deterministic recognition. For every \(h\ge2\), a deterministic recognizer with \(s\) states satisfies \(2^{\lfloor(h-2)/31\rfloor}\le4(s+2)^2\) under both acceptance conventions considered in the paper; one convention has the sharper factor \(4(s+1)^2\). The alphabet may grow with \(h\), so no alphabet-independent polynomial simulation bound holds.

Comparator links

Result	Comparator statement
Two-way nondeterministic complementation lower bound	TwoWayComplementation.lean
Same-family determinization lower bound	TwoWayDeterminization.lean
Exponential deterministic state lower bound for liveness	OneWayLiveness.lean

Scope note on GitHub →