Immerman–Szelepcsényi theorem

In computational complexity theory, the Immerman–Szelepcsényi theorem states that nondeterministic space complexity classes are closed under complementation. It was proven independently by Neil Immerman and Róbert Szelepcsényi in 1987, for which they shared the 1995 Gödel Prize. In its general form the theorem states that NSPACE(s(n)) = co-NSPACE(s(n)) for any function s(n) ≥ log n. The result is equivalently stated as NL = co-NL; although this is the special case when s(n) = log n, it implies the general theorem by a standard padding argument. The result solved the second LBA problem.

In other words, if a nondeterministic machine can solve a problem, another machine with the same resource bounds can solve its complement problem (with the yes and no answers reversed) in the same asymptotic amount of space. No similar result is known for the time complexity classes, and indeed it is conjectured that NP is not equal to co-NP.

The principle used to prove the theorem has become known as inductive counting. It has also been used to prove other theorems in computational complexity, including the closure of LOGCFL under complementation and the existence of error-free randomized logspace algorithms for USTCON.

The theorem can be proven by showing how to translate any nondeterministic logarithmic space Turing machine M into another nondeterministic logspace Turing machine that solves the complementary decision problem.

The states of M (described by the position of its head on the input tape and the configuration of the log-space working memory) can be thought of as the vertices of a directed graph, and the transitions of M can be thought of as edges in this graph. M accepts an input string whenever there exists a path in this graph from the vertex s that represents the starting state to a special vertex t that represents any accepting state. In this way, the existence of an accepting nondeterministic computation for M can be seen as a version of the st-connectivity problem, for implicit graphs rather than graphs given explicitly as an explicitly-represented input graph. In this graphical view, the goal of the proof is to find a nondeterministic logspace algorithm that accepts only when there does not exist a path from s to t in the same implicit graph.

...
Wikipedia