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 . It contains and is believed to strictly contain it, but this is unproven.

Formal definition In terms of and ,

Examples of problems

Formal languages 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 (zero or more copies of an expression), and squaring (two copies of an expression).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.

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

Reasoning in the first-order theory of the real numbers with +, ×, = is in EXPSPACE and was conjectured to be EXPSPACE-complete in 1986.

Petri nets

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 nonelementary, so probably not in . In 2022 it was shown to be Ackermann-complete.

It is EXPSPACE-complete to decide whether the reachability of a given vector addition system is finite.

EXPSPACE

Bron en licentie