EXPSPACE


In computational complexity theory, is the set of all decision problems solvable by a deterministic Turing machine in exponential space, i.e., in space, where is a polynomial function of. Some authors restrict to be a linear function, but most authors instead call the resulting class. If we use a nondeterministic machine instead, we get the class, which is equal to by Savitch's theorem.
A decision problem is if it is in, and every problem in has a polynomial-time many-one reduction to it. In other words, there is a polynomial-time algorithm that transforms instances of one to instances of the other with the same answer. problems might be thought of as the hardest problems in.
is a strict superset of,, and and is believed to be a strict superset of.

Formal definition

In terms of and,

Examples of problems

An example of an problem is the problem of recognizing whether two regular expressions represent different languages, where the expressions are limited to four operators: union, concatenation, the Kleene star, and squaring.
If the Kleene star is left out, then that problem becomes, which is like, except it is defined in terms of non-deterministic Turing machines rather than deterministic.
It has also been shown by L. Berman in 1980 that the problem of verifying/falsifying any first-order statement about real numbers that involves only addition and comparison is in.
Alur and Henzinger extended Linear temporal logic with times and prove that the validity problem of their logic is EXPSPACE-complete.
The coverability problem for Petri Nets is -complete
. The reachability problem for Petri nets was known to be -hard for a long time, but shown to be non-elementary, so it is provably not in.

Relationship to other classes

is known to be a strict superset of,, and. It is further suspected to be a strict superset of, however this is not known.