A quadratic lower bound for 2DFAs against one-way liveness
Kehinde Adeogun, Christos Kapoutsis

TL;DR
This paper establishes a quadratic lower bound on the number of states needed for two-way deterministic finite automata to solve one-way liveness, extending known bounds to arbitrary alphabets and providing a versatile proof approach.
Contribution
It introduces a new quadratic lower bound for 2DFAs solving one-way liveness on arbitrary alphabets, generalizing previous unary-specific results with a novel proof technique.
Findings
2DFA solving one-way liveness requires Omega(h^2) states
Lower bound applies to arbitrary alphabet sizes
Proof technique is potentially reusable in other contexts
Abstract
We show that every two-way deterministic finite automaton (2DFA) that solves one-way liveness on height h has Omega(h^2) states. This implies a quadratic lower bound for converting one-way nondeterministic finite automata to 2DFAs, which asymptotically matches Chrobak's well-known lower bound for this conversion on unary languages. In contrast to Chrobak's simple proof, which relies on a 2DFA's inability to differentiate between any two sufficiently distant locations in a unary input, our argument works on alphabets of arbitrary size and is structured around a main lemma that is general enough to potentially be reused elsewhere.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
Topicssemigroups and automata theory · Formal Methods in Verification · DNA and Biological Computing
