EXPSPACE

Template:Short description In computational complexity theory, Template:Sans-serif is the set of all decision problems solvable by a deterministic Turing machine in exponential space, i.e., in $O(2^{p(n)})$ space, where $p(n)$ is a polynomial function of $n$. Some authors restrict $p(n)$ to be a linear function, but most authors instead call the resulting class Template:Sans-serif. If we use a nondeterministic machine instead, we get the class Template:Sans-serif, which is equal to Template:Sans-serif by Savitch's theorem.

A decision problem is Template:Sans-serif if it is in Template:Sans-serif, and every problem in Template:Sans-serif 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. Template:Sans-serif problems might be thought of as the hardest problems in Template:Sans-serif.

Template:Sans-serif is a strict superset of Template:Sans-serif, Template:Sans-serif, and Template:Sans-serif and is believed to be a strict superset of Template:Sans-serif.

Formal definition

In terms of Template:Sans-serif and Template:Sans-serif,

$𝖤𝖷𝖯𝖲𝖯𝖠𝖢𝖤=\bigcup _{k\in \mathbb{N}}𝖣𝖲𝖯𝖠𝖢𝖤\left(2^{n^k}\right)=\bigcup _{k\in \mathbb{N}}𝖭𝖲𝖯𝖠𝖢𝖤\left(2^{n^k}\right)$

Examples of problems

Template:Anchor An example of an Template:Sans-serif 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 (zero or more copies of an expression), and squaring (two copies of an expression).

Alur and Henzinger extended linear temporal logic with times (integer) and prove that the validity problem of their logic is EXPSPACE-complete.

The coverability problem for Petri Nets is Template:Sans-serif-complete.

The reachability problem for Petri nets was known to be Template:Sans-serif-hard for a long time, but shown to be nonelementary, so probably not in Template:Sans-serif. In 2022 it was shown to be Ackermann-complete.

Relationship to other classes

Template:Sans-serif is known to be a strict superset of Template:Sans-serif, Template:Sans-serif, and Template:Sans-serif. It is further suspected to be a strict superset of Template:Sans-serif, however this is not known.

See also

• Game complexity

References

• Template:Cite journal
• Template:Cite book Section 9.1.1: Exponential space completeness, pp. 313–317. Demonstrates that determining equivalence of regular expressions with exponentiation is EXPSPACE-complete.