Browse › Theoretical computer science › 129 Exponential state costs for two-way automata
An exponential state lower bound for two-way nondeterministic complementation
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
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.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Follow-up works
- Sudais Arif, A Factor-Two Lower Bound for Complementing Two-Way Deterministic Finite Automata (arXiv:2610.18897, 10 Oct 2026). Cites this paper and its companion in its related-work paragraph for related descriptions of interval behavior, and states that "those papers concern different state-complexity questions"; the acknowledgments say the work was developed with assistance from an OpenAI model. [family-level]
Formalization
- OpenAI math release, Lean scope notes for family 129: Exponential state costs for two-way automata (lean/docs/129.md, October 2026). Describes the release's Lean formalization of the complementation lower bound for every $n\ge4$ and of the same-family 2DFA bound for $n\ge131$, with comparator statement
ComparatorChallenges/TwoWayComplementation.lean; its paragraph on the one-way-liveness bound follows a sentence excluding that result from scope. [family-level]
Possibly relevant literature (found by the agent, not checked)
- Giovanni Pighizzini, Two-Way Finite Automata: Old and Recent Results (arXiv:1208.2755, EPTCS 90, 2012). Survey of the Sakoda–Sipser question and related results, background for the paper's history paragraph on two-way state succinctness.
- Juraj Hromkovič and Georg Schnitger, Nondeterminism versus Determinism for Two-Way Finite Automata: Generalizations of Sipser's Separation (ICALP 2003, doi:10.1007/3-540-45061-0_36). Earlier exponential 2NFA-versus-restricted-2DFA separations (oblivious and nearly oblivious 2DFAs), related to the paper's corollary on 2DFAs for the same family.
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 129
Independent sites; their content is not reviewed here.
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}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/129.md. The Lean statements have not been checked by people against the paper's claims.
Family 129: 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.
Other papers in this family:
- An exponential two-way deterministic state lower bound for one-way liveness · September 25, 2026