Menu
Home
People
Places
Arts
History
Plants & Animals
Science
Life & Culture
Technology
Reference.org
EXPSPACE
open-in-new
<h2 id="formal-definition">Formal definition</h2> <p>In terms of <a href="/facts/DSPACE/co9rzRQd">DSPACE</a> and <a href="/facts/NSPACE/ICDSmk4S">NSPACE</a>, </p> E X P S P A C E = ⋃ k ∈ N D S P A C E ( 2 n k ) = ⋃ k ∈ N N S P A C E ( 2 n k ) {\displaystyle {\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)} <h2 id="examples-of-problems">Examples of problems</h2> <h3>Formal languages</h3> <p>An example of an EXPSPACE-complete problem is the problem of recognizing whether two <a href="/facts/Regular_expression/KFL3veHX">regular expressions</a> represent different languages, where the expressions are limited to four operators: union, <a href="/facts/Concatenation/1npYg6rc">concatenation</a>, the <a href="/facts/Kleene_star/I6SX0f2Y">Kleene star</a> (zero or more copies of an expression), and squaring (two copies of an expression).<a class="footnote-ref" id="fnref:1" href="#fn:1"><sup>1</sup></a> </p> <h3>Logic</h3> <p>Alur and Henzinger extended <a href="/facts/Linear_temporal_logic/Gh5yxXK7">linear temporal logic</a> with times (integer) and prove that the validity problem of their logic is EXPSPACE-complete.<a class="footnote-ref" id="fnref:2" href="#fn:2"><sup>2</sup></a> </p><p>Reasoning in the first-order theor of the real numbers with +, ×, = is in EXPSPACE and was conjectured to be EXPSPACE-complete in 1986.<a class="footnote-ref" id="fnref:3" href="#fn:3"><sup>3</sup></a> </p> <h3>Petri nets</h3> <p>The coverability problem for <a href="/facts/Petri_Nets/BK7eTHNm">Petri Nets</a> is EXPSPACE-complete.<a class="footnote-ref" id="fnref:4" href="#fn:4"><sup>4</sup></a> </p><p>The <a href="/facts/Reachability_problem/jlBpsn98">reachability problem</a> for Petri nets was known to be EXPSPACE-hard for a long time,<a class="footnote-ref" id="fnref:5" href="#fn:5"><sup>5</sup></a> but shown to be <a href="/facts/Nonelementary_problem/PYLSyvHo">nonelementary</a>,<a class="footnote-ref" id="fnref:6" href="#fn:6"><sup>6</sup></a> so probably not in EXPSPACE. In 2022 it was shown to be <a href="/facts/Ackermann_function/WQNpCWHn">Ackermann</a>-complete.<a class="footnote-ref" id="fnref:7" href="#fn:7"><sup>7</sup></a><a class="footnote-ref" id="fnref:8" href="#fn:8"><sup>8</sup></a> </p> <h2 id="see-also">See also</h2> <ul><li><a href="/facts/Game_complexity/r5Gqrqy7">Game complexity</a></li></ul> <ul><li>Berman, Leonard (1 May 1980). <a href="https://doi.org/10.1016%2F0304-3975%2880%2990037-7">"The complexity of logical theories"</a>. <i>Theoretical Computer Science</i>. 11 (1): 71–77. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1016%2F0304-3975%2880%2990037-7">10.1016/0304-3975(80)90037-7</a>.</li> <li><a href="/facts/Michael_Sipser/h5Wg22bh">Michael Sipser</a> (1997). <a href="https://archive.org/details/introductiontoth00sips"><i>Introduction to the Theory of Computation</i></a>. PWS Publishing. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 0-534-94728-X. Section 9.1.1: Exponential space completeness, pp. 313–317. Demonstrates that determining equivalence of regular expressions with exponentiation is EXPSPACE-complete.</li></ul> <h2 id="references">References</h2> <ol> <li id="fn:1"><p>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. <a href="/wiki/Larry_Stockmeyer" target="_blank">/wiki/Larry_Stockmeyer</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li> <li id="fn:2"><p>Alur, Rajeev; Henzinger, Thomas A. (1994-01-01). "A Really Temporal Logic". J. ACM. 41 (1): 181–203. doi:10.1145/174644.174651. ISSN 0004-5411. <a href="https://doi.org/10.1145%2F174644.174651" target="_blank">https://doi.org/10.1145%2F174644.174651</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li> <li id="fn:3"><p>Ben-Or, Michael; Kozen, Dexter; Reif, John (1986-04-01). "The complexity of elementary algebra and geometry". Journal of Computer and System Sciences. 32 (2): 251–264. doi:10.1016/0022-0000(86)90029-2. ISSN 0022-0000. <a href="https://www.sciencedirect.com/science/article/pii/0022000086900292" target="_blank">https://www.sciencedirect.com/science/article/pii/0022000086900292</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li> <li id="fn:4"><p>Charles Rackoff (1978). "The covering and boundedness problems for vector addition systems". Theoretical Computer Science: 223–231. <a href="#fnref:4" class="footnote-back-ref">↩</a></p></li> <li id="fn:5"><p>Lipton, R. (1976). "The Reachability Problem Requires Exponential Space". Technical Report 62. Yale University. <a href="http://citeseer.ist.psu.edu/contextsummary/115623/0" target="_blank">http://citeseer.ist.psu.edu/contextsummary/115623/0</a> <a href="#fnref:5" class="footnote-back-ref">↩</a></p></li> <li id="fn:6"><p>Wojciech Czerwiński Sławomir Lasota Ranko S Lazić Jérôme Leroux Filip Mazowiecki (2019). "The reachability problem for Petri nets is not elementary". STOC 19. <a href="#fnref:6" class="footnote-back-ref">↩</a></p></li> <li id="fn:7"><p>Leroux, Jerome (February 2022). "The Reachability Problem for Petri Nets is Not Primitive Recursive". 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS). IEEE. pp. 1241–1252. arXiv:2104.12695. doi:10.1109/FOCS52979.2021.00121. ISBN 978-1-6654-2055-6. <a href="978-1-6654-2055-6" target="_blank">978-1-6654-2055-6</a> <a href="#fnref:7" class="footnote-back-ref">↩</a></p></li> <li id="fn:8"><p>Brubaker, Ben (4 December 2023). "An Easy-Sounding Problem Yields Numbers Too Big for Our Universe". Quanta Magazine. <a href="https://www.quantamagazine.org/an-easy-sounding-problem-yields-numbers-too-big-for-our-universe-20231204/" target="_blank">https://www.quantamagazine.org/an-easy-sounding-problem-yields-numbers-too-big-for-our-universe-20231204/</a> <a href="#fnref:8" class="footnote-back-ref">↩</a></p></li> </ol>