Resolution of The Linear-Bounded Automata Question

This paper resolves a famous and longstanding open question in automata theory, i.e., the {\it linear-bounded automata question} (or shortly, LBA question), which can also be phrased succinctly in the language of computational complexity theory as $${\rm NSPACE}[n]\overset{?}{=}{\rm DSPACE}[n].$$ In fact, we prove a more general result that $${\rm DSPACE}[S(n)]\subsetneqq {\rm NSPACE}[S(n)]$$ where $S(n)\geq n$ is a space-constructible function. Our proof technique is based on diagonalization against deterministic $S(n)$ space-bounded Turing machines with a universal nondeterministic Turing machine and on other novel and interesting new techniques. Our proof also implies the following consequences, which resolve some famous open questions in complexity theory: (1). ${\rm DSPACE}[n]\subsetneqq {\rm NSPACE}[n]$; (2). $L\subsetneqq NL$; (3). $L\subsetneqq P$; (4). There exists no deterministic Turing machine working in $O(\log n)$ space deciding the $st$-connectivity question (STCON).