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 <math>O(2^{p(n)})</math> space, where <math>p(n)</math> is a polynomial function of <math>n</math>. Some authors restrict <math>p(n)</math> 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. It contains Template:Sans-serif and is believed to strictly contain it, but this is unproven.

Formal definition

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

<math>\mathsf{EXPSPACE} = \bigcup_{k\in\mathbb{N}} \mathsf{DSPACE}\left(2^{n^k}\right) = \bigcup_{k\in\mathbb{N}} \mathsf{NSPACE}\left(2^{n^k}\right)</math>

Examples of problems

Formal languages

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).<ref>Meyer, A.R. and L. Stockmeyer. The equivalence problem for regular expressions with squaring requires exponential space. 13th IEEE Symposium on Switching and Automata Theory, Oct 1972, pp.125–129.</ref>

Logic

Alur and Henzinger extended linear temporal logic with times (integer) and prove that the validity problem of their logic is EXPSPACE-complete.<ref>Template:Cite journal</ref>

Reasoning in the first-order theory of the real numbers with +, ×, = is in EXPSPACE and was conjectured to be EXPSPACE-complete in 1986.<ref>Template:Cite journal</ref>

Petri nets

The coverability problem for Petri Nets is Template:Sans-serif-complete.<ref>Template:Cite journal</ref>

The reachability problem for Petri nets was known to be Template:Sans-serif-hard for a long time,<ref>Template:Cite journal</ref> but shown to be nonelementary,<ref>Template:Cite conference</ref> so probably not in Template:Sans-serif. In 2022 it was shown to be Ackermann-complete.<ref name=":1">Template:Cite book</ref><ref name=":0">{{#invoke:citation/CS1|citation |CitationClass=web }}</ref>

See also

• Game complexity

References

<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.