EXPSPACE

In computational complexity theory, {{Sans-serif|EXPSPACE}} 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 {{Sans-serif|ESPACE}}. If we use a nondeterministic machine instead, we get the class {{Sans-serif|NEXPSPACE}}, which is equal to {{Sans-serif|EXPSPACE}} by Savitch's theorem.

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

{{Sans-serif|EXPSPACE}} is a strict superset of {{Sans-serif|PSPACE}}, {{Sans-serif|NP}}, and {{Sans-serif|P}}. It contains {{Sans-serif|EXPTIME}} and is believed to strictly contain it, but this is unproven.

Formal definition

In terms of {{Sans-serif|DSPACE}} and {{Sans-serif|NSPACE}},

: $\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)$

Examples of problems

= Formal languages =

An example of an {{Sans-serif|EXPSPACE-complete}} 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. [https://people.csail.mit.edu/meyer/rsq.pdf 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.{{Cite journal|last1=Alur|first1=Rajeev|last2=Henzinger|first2=Thomas A.|date=1994-01-01|title=A Really Temporal Logic|journal=J. ACM|volume=41|issue=1|pages=181–203|doi=10.1145/174644.174651|issn=0004-5411|doi-access=free}}

Reasoning in the first-order theor of the real numbers with +, ×, = is in EXPSPACE and was conjectured to be EXPSPACE-complete in 1986.{{Cite journal |last=Ben-Or |first=Michael |last2=Kozen |first2=Dexter |last3=Reif |first3=John |date=1986-04-01 |title=The complexity of elementary algebra and geometry |url=https://www.sciencedirect.com/science/article/pii/0022000086900292 |journal=Journal of Computer and System Sciences |volume=32 |issue=2 |pages=251–264 |doi=10.1016/0022-0000(86)90029-2 |issn=0022-0000}}

= Petri nets =

The coverability problem for Petri Nets is {{Sans-serif|EXPSPACE}}-complete.{{cite journal |

author = Charles Rackoff |

title = The covering and boundedness problems for vector addition systems |

journal = Theoretical Computer Science |

pages = 223–231 |

date = 1978}}

The reachability problem for Petri nets was known to be {{Sans-serif|EXPSPACE}}-hard for a long time,{{cite journal | last = Lipton | first = R. | url = http://citeseer.ist.psu.edu/contextsummary/115623/0 | title = The Reachability Problem Requires Exponential Space | journal = Technical Report 62 | publisher = Yale University | date = 1976 }} but shown to be nonelementary,{{cite conference | author = Wojciech Czerwiński Sławomir Lasota Ranko S Lazić Jérôme Leroux Filip Mazowiecki

| title = The reachability problem for Petri nets is not elementary | book-title = STOC 19 | date = 2019}} so probably not in {{Sans-serif|EXPSPACE}}. In 2022 it was shown to be Ackermann-complete.{{Cite book |last=Leroux |first=Jerome |chapter=The Reachability Problem for Petri Nets is Not Primitive Recursive |date=February 2022 |title=2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS) |chapter-url=https://ieeexplore.ieee.org/document/9719763 |publisher=IEEE |pages=1241–1252 |doi=10.1109/FOCS52979.2021.00121 |isbn=978-1-6654-2055-6|arxiv=2104.12695 }}{{Cite web |last=Brubaker |first=Ben |date=4 December 2023 |title=An Easy-Sounding Problem Yields Numbers Too Big for Our Universe |url=https://www.quantamagazine.org/an-easy-sounding-problem-yields-numbers-too-big-for-our-universe-20231204/ |website=Quanta Magazine}}

References

{{cite journal |last1=Berman |first1=Leonard |title=The complexity of logical theories |journal=Theoretical Computer Science |date=1 May 1980 |volume=11 |issue=1 |pages=71–77 |doi=10.1016/0304-3975(80)90037-7|doi-access=free }}
{{cite book | author = Michael Sipser | year = 1997 | title = Introduction to the Theory of Computation | publisher = PWS Publishing | isbn = 0-534-94728-X | url-access = registration | url = https://archive.org/details/introductiontoth00sips | author-link = Michael Sipser }} Section 9.1.1: Exponential space completeness, pp. 313–317. Demonstrates that determining equivalence of regular expressions with exponentiation is EXPSPACE-complete.

Category:Complexity classes