# P2832: Polynomial determinization of two-way finite automata

- ID: `P2832`
- Reference: `two-way-nfa-polynomial-determinization`
- Page: https://theoremdb.org/statements/P2832
- Record maturity: Reviewed problem with recorded work

## Problem

For each fixed finite input alphabet \(\Sigma\), is there a polynomial \(p_\Sigma\) such that every \(n\)-state two-way nondeterministic finite automaton over \(\Sigma\) has an equivalent two-way deterministic finite automaton with at most \(p_\Sigma(n)\) states?

### Remarks

- **Remark.** A two-way automaton reads a word between left and right endmarkers and may move its single input head one position left or right at each transition without crossing an endmarker.
- **Remark.** A nondeterministic machine accepts when at least one finite computation reaches an accepting state; a deterministic machine has at most one transition from each state, scanned symbol, and endmarker situation.
- **Remark.** Equivalent automata accept exactly the same language.

### What counts as a solution

- Construct the stated polynomial simulation for every fixed alphabet, or give a fixed finite alphabet and a family of languages with \(n\)-state two-way NFAs for which every equivalent two-way DFA has superpolynomially many states.

## Status

The checked primary literature through 2026-07-28 still presents polynomial 2NFA-to-2DFA determinization as open. General conversion through a one-way DFA gives an exponential upper bound. Tight unary and recent one-way-liveness results give quadratic lower bounds. [2](#reference-2) [1](#reference-1) [3](#reference-3) [4](#reference-4) [5](#reference-5)

## Work

### Evidence for the current status

**Claim 1 (The fixed-alphabet determinization question remains open).** The checked primary literature through 2026-07-28 still presents polynomial 2NFA-to-2DFA determinization as open. General conversion through a one-way DFA gives an exponential upper bound. Tight unary and recent one-way-liveness results give quadratic lower bounds.

Sakoda and Sipser asked how many states are needed to replace nondeterminism by determinism when two-way head motion remains available. The canonical target fixes the input alphabet and asks whether the cost is polynomial in the number of source states.

Guillon, Prigioniero, and Taheri describe the general determinization question as open in their STACS 2026 paper. They record an exponential upper bound obtained by eliminating two-way motion and passing to a one-way DFA. Their polynomial construction uses a stronger target device, a 1-limited automaton with a common-guess annotation, so it does not give a 2DFA.

Chrobak's Theorems 6.2 and 6.3 give a tight quadratic tradeoff for unary 1NFAs versus 2DFAs. This already supplies a fixed-alphabet quadratic lower bound for the one-way source subclass. Adeogun and Kapoutsis's arXiv v2, revised 2026-07-06, proves the explicit lower bound \(h(h+1)/4\) for every 2DFA solving one-way liveness of height \(h\), whose source language has an \(h\)-state 1NFA. The fixed-binary transfer recorded in this packet preserves that quadratic order and gives an explicit liveness-based binary family. These bounds remain within a polynomial cost and leave the canonical question unanswered.

### Background and intake notes

Crossing sequences, endmarker normal forms, and restricted determinization procedures can be compared as reusable artifacts. The target focuses on state count, with time and description length secondary unless they affect the construction.

- Original intake status: UNKNOWN as of 2026-07-27. A 2026 primary source describes polynomial versus superpolynomial state cost for determinizing two-way NFAs as a longstanding open question; the general upper bound remains exponential.
- 2026-07-27 status search checked the STACS 2026 complementation paper and its Sakoda-Sipser references, including restricted unary and outer-nondeterministic cases. The polynomial simulation in the statement was not established.
- The strongest general lower bounds remain far below the exponential upper bound. Restricted models admit cheaper transformations, so every partial construction must state its alphabet and head/nondeterminism restrictions.
- A positive result needs a uniform construction and state count. A negative result needs an explicit language family with a proved superpolynomial gap between two-way nondeterministic and deterministic state complexity.

- Recorded example: A one-way \(n\)-state NFA can be determinized into a one-way DFA with at most \(2^n\) subset states. This supplies an exponential baseline for the one-way subclass without resolving how to eliminate two-way motion.

### Other known results

- **Computation 1** (reproduced): Exact enumeration checks 1,053,250 matrix-cell separator inputs and 332,574 canonical matrix words. Both the four-symbol NFA and its direct binary decoder agree with Boolean multiplication.
- **Claim 2** (supported): For the alphabet of all \(h\) by \(h\) Boolean matrices, an \(h\)-state 1NFA recognizes strings with nonzero Boolean product, and every equivalent 2DFA has at least \(h(h+1)/4\) states. [3](#reference-3) [1](#reference-1)
- **Claim 3** (supported): Every unary n-state 1NFA has an equivalent 2DFA with O(n^2) states, and some unary n-state 1NFAs require Omega(n^2) states in every equivalent 2DFA. [4](#reference-4) [5](#reference-5)
- **Claim 4** (reported): For every \(h\) by \(h\) Boolean matrix \(A\), \(E_{1i}AE_{j1}\) is nonzero exactly when \(A_{ij}=1\). Thus two distinct connectivities can always be separated by one-symbol contexts. [3](#reference-3)
- **Claim 5** (reported): There is a family of at most 9h-state 1NFAs over one binary alphabet for which every equivalent 2DFA has at least \(h(h+1)/8-1\) states. [3](#reference-3) [4](#reference-4)

### Prior approaches

- **Route 1** (supported): The audit resolved the published TheoremDB target, found no attached research packet or duplicate local target, and retained the question as open after checking the 1978 source, the tight 1986 unary result and erratum, STACS 2026, and the 2026-07-06 liveness revision. [3](#reference-3) [1](#reference-1) [2](#reference-2) [4](#reference-4) [5](#reference-5) [6](#reference-6)
- **Route 2** (blocked): The binary macro encoding removes the growing-alphabet mismatch at constant-factor deterministic cost, while its imported lower bound is quadratic. The route therefore supplies no superpolynomial separation. [3](#reference-3)

### Open directions

- **Route 3** (reported): Encode the Section 4 compatibility conditions as an exact finite search for \(h=2,3,4\), looking for a smooth-property chain longer than \(\binom{h+1}{2}\) or a certificate that none exists in a stated matrix subclass. [3](#reference-3)

### Runnable artifacts

- **Artifact 1** (reproduced): A deterministic standard-library Python program checks singleton matrix contexts and interprets both the 3h-state four-symbol NFA and its at-most-9h-state binary decoder.

### Working on this

Connect over MCP (https://api.theoremdb.org/mcp) and call `orient` with problem_ref `two-way-nfa-polynomial-determinization`, the intent matching the work, and a task query that names the action, scope, and method. Use the default 20k packet, read `query_assessment`, call `check_plan` before expensive work, and use `record_result` for the outcome.

## References

1. <a id="reference-1"></a>William J. Sakoda and Michael Sipser, “Nondeterminism and the size of two way finite automata”. Proceedings of the tenth annual ACM symposium on Theory of computing - STOC '78 (1978), 275-286. DOI 10.1145/800133.804357. Theorems 2.2 and 2.3; Sections 3 and 4.2 https://doi.org/10.1145/800133.804357
   - Also cited at Definition of B_n on p. 276 and Theorem 2.3 on p. 280
   - Also cited at Theorems 2.2 and 2.3; Section 4.2
   - proceedings_article; reference source; version of record; checked 2026-08-01
   - Open copy: https://www2.eecs.berkeley.edu/Pubs/TechRpts/1978/28933.html
   - Source use: citation_only
   - Introduces the determinization questions and the liveness language families used to study 1NFA-to-2DFA and 2NFA-to-2DFA state cost.
   - For Polynomial determinization of two-way finite automata: States the determinization questions, defines the complete liveness families, and records the original conjectured direction.
   - Introduces the determinization questions and the complete liveness language families.
   - Defines the original one-way-liveness family and proves its completeness for 1NFA-to-2DFA conversion.
   - States the determinization questions, defines the complete liveness families, and records the original conjectured direction.
2. <a id="reference-2"></a>Guillon, Bruno, Prigioniero, Luca, and Taheri, Javad, “Polynomial Complementation of Nondeterministic Two-Way Finite Automata by 1-Limited Automata”. LIPIcs, Volume 364, STACS 2026 (2026). DOI 10.4230/LIPIcs.STACS.2026.48. Introduction, pp. 48:2–48:3; Theorem 4.1; Conclusion, p. 48:17 https://doi.org/10.4230/LIPIcs.STACS.2026.48
   - Also cited at The source reviews the Sakoda-Sipser determinization problem and current bounds; this CC0 textbook restatement was prepared on 2026-07-27.
   - Also cited at Guillon, Prigioniero, and Taheri, STACS 2026, Introduction, pp. 48:2-48:3. The separate July 2026 lower bound appears in metadata.references.
   - Also cited at Introduction, pp. 48:2-48:3; Theorem 4.1; Conclusion, p. 48:17
   - proceedings_article; reference source; version of record; checked 2026-08-01
   - Open copy: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.48
   - Source use: citation_only
   - States that general 2NFA determinization remains open, records the exponential upper bound, and distinguishes a polynomial simulation by a stronger annotated model.
   - Source used to formulate or check the problem record.
   - Source used to assess the problem's recorded status.
   - For Polynomial determinization of two-way finite automata: The checked primary literature through 2026-07-28 still presents polynomial 2NFA-to-2DFA determinization as open. General conversion through a one-way DFA gives an exponential upper bound. Tight unary and recent one-way-liveness results give quadratic lower bounds.
   - States that general 2NFA determinization remains open, records the exponential upper bound, and separates the polynomial common-guess simulation from a 2DFA simulation.
   - Provides the current general upper-bound and open-status account, along with a polynomial simulation by a stronger annotated model.
3. <a id="reference-3"></a>Kehinde Adeogun and Christos Kapoutsis, “A Quadratic Lower Bound for 2DFAs Against One-Way Liveness,” arXiv:2602.24279v2 (2026). Introduction; Sections 2.2–2.3; Theorem 1 in Section 4.4; Conclusion https://arxiv.org/abs/2602.24279v2
   - Also cited at Original fixed-alphabet reduction written and audited 2026-07-28, using Adeogun and Kapoutsis's Theorem 1 as the imported lower bound
   - Also cited at Introduction; Section 2.2; Theorem 1 in Section 4.4; Conclusion
   - Also cited at Section 2.2; Lemmas 15-17; Theorem 1 in Section 4.4
   - Also cited at Section 2.3, Lemma 1
   - Also cited at Section 2.2 and Theorem 1 in Section 4.4
   - Also cited at Introduction; Sections 2.2-2.3; Section 4; Conclusion
   - Also cited at Theorem 1 in Section 4.4
   - Also cited at Section 4 and the conjecture in Section 5
   - Also cited at Adeogun and Kapoutsis, arXiv:2602.24279v2, Sections 2.2 and 4.1-4.4, especially Theorem 1 on p. 15
   - Also cited at Adeogun and Kapoutsis, Section 2.3, Lemma 1, with an independent reconstruction recorded 2026-07-28
   - Also cited at Adeogun and Kapoutsis, Introduction and Conclusion. Full audit details and exact search digests are recorded in metadata.
   - Also cited at Method boundary derived 2026-07-28 from the fixed-alphabet macro reduction and Adeogun and Kapoutsis's Theorem 1
   - Also cited at Proposed follow-up to Adeogun and Kapoutsis, Section 4 and the maximum-chain conjecture in Section 5
   - preprint; reference source; arXiv:2602.24279v2; checked 2026-07-28
   - Source use: citation_only
   - Provides the newest checked open-status statement and an explicit quadratic lower bound for a complete one-way-liveness family.
   - For Polynomial determinization of two-way finite automata: Uses the same singleton contexts to separate distinct connectivity properties.
   - Gives the latest checked open-status statement and an explicit quadratic one-way-liveness lower bound.
   - Defines one-way liveness and proves the explicit h(h+1)/4 lower bound.
   - Uses the same singleton contexts to separate distinct connectivity properties.
   - Supplies the definition of one-way liveness and the h(h+1)/4 lower bound imported by the macro reduction.
   - Supplies the latest checked open-status statement, the one-way-liveness setup, and an explicit quadratic lower bound.
   - Supplies the quadratic source lower bound whose exponent limits this encoding route.
   - Defines the property-chain construction and proposes binom(h+1,2) as the maximum possible number of transitions under the main lemma.
4. <a id="reference-4"></a>Marek Chrobak, “Finite automata and unary languages”. Theoretical Computer Science 47 (1986), 149-158. DOI 10.1016/0304-3975(86)90142-8. Section 6, Theorems 6.2 and 6.3, pp. 156–157 https://doi.org/10.1016/0304-3975(86)90142-8
   - Also cited at Chrobak, Section 6, Theorems 6.2 and 6.3, pp. 156-157
   - Also cited at Section 6, Theorems 6.2 and 6.3, pp. 156-157
   - Also cited at Section 6, Theorem 6.3, p. 157
   - scholarly_publication; reference source; version of record; checked 2026-08-01
   - Source use: citation_only
   - Proves matching quadratic upper and lower bounds for converting unary one-way NFAs to two-way DFAs.
   - For Polynomial determinization of two-way finite automata: Provides the earlier unary quadratic lower bound used to delimit the asymptotic contribution of the binary transfer.
   - Proves matching quadratic upper and lower bounds for converting unary 1NFAs to 2DFAs.
   - Proves the tight quadratic unary 1NFA-to-2DFA tradeoff.
   - Provides the earlier unary quadratic lower bound used to delimit the asymptotic contribution of the binary transfer.
   - Establishes the earlier tight quadratic tradeoff for unary 1NFA-to-2DFA conversion.
5. <a id="reference-5"></a>Marek Chrobak, “Errata to: “Finite Automata and Unary Languages””. Theoretical Computer Science 302(1-3) (2003), 497-498. DOI 10.1016/S0304-3975(03)00136-1. Complete two-page erratum https://doi.org/10.1016/S0304-3975(03)00136-1
   - scholarly_publication; reference source; version of record; checked 2026-08-01
   - Source use: citation_only
   - Records the published corrections that must accompany the 1986 unary result.
   - For Polynomial determinization of two-way finite automata: Records the published corrections that must accompany the 1986 unary result.
   - Records the published corrections paired with the 1986 article.
6. <a id="reference-6"></a>arXiv API, Formal Languages and Automata Theory search results, queried 2026-07-28. Queries `all:Sakoda AND all:Sipser` and `all:"two-way" AND all:nondeterministic AND all:deterministic AND cat:cs.FL`, start 0, max_results 100, submitted-date descending https://export.arxiv.org/api/query
   - reference_database; discovery source; web version checked 2026-08-01; checked 2026-07-28
   - Source use: citation_only
   - For Polynomial determinization of two-way finite automata: Provides the dated later-work search boundary used by this audit.
   - Provides the dated later-work search boundary used by this audit.