A "natural" decidable problem not in $\mathsf{NP}$? [duplicate]

Are there any "natural" examples of decidable problems that are definitively known not to be in NP? The decidable languages I know of that are not contained in NP are usually derived from the time hierarchy theorem, which produces "artificial" languages based on diagonalization.

• other known examples are also based on diagonalization which can be "embedded/encoded" in problems that do not seem to refer to TMs directly.
– vzn
Mar 16 '13 at 5:39
• re duplicate status. dont agree this question is equivalent to the other question because this one asks for a "natural" problem, which has special meaning (but is not usually strictly formally defined or definable), & the other does not. so they are similar & there could be some overlap, but there may exist problems that fit the other question but not be "natural".
– vzn
Mar 19 '13 at 15:16
• Some of the answers there contain problems I would consider as "natural", e.g. equivalence of regular expressions, so you have to come up with a very narrow definition of "natural" to separate the questions. Mar 20 '13 at 16:36

From an answer to a related question on NP-hard problems which are not contained in NP: probably the most natural example is determining whether two regular expressions (including the Kleene star for arbitrary repetition, and a squaring operation to allow compact expressions of very large fixed numbers of repetitions) are equivalent. The resulting problem is EXPSPACE complete. Because EXPSPACE contains NEXP, which contains NP strictly (by the time hierarchy theorem), this is a decideable problem which is not in NP.

• nearly identical, determining if $L=\Sigma*$ for regular expressions with exponentiation
– vzn
Mar 16 '13 at 5:12
• Wikipedia's List of PSPACE-complete problems contains "Equivalence problem for regular expressions". The EXPSPACE-complete problem needs the additional operator of squaring, according to Wikipedia's EXPSPACE-page. Mar 16 '13 at 11:04
• @ThomasKlimpel: This doesn't really make sense to me. Can't squaring be achieved in-line anyway, by replacing e.g. $(a|bc)^2 = (a|bc)(a|bc)$? Mar 18 '13 at 14:11
• Yes, squaring can be achieved in-line. But this increases the size of the input, and complexity classes depend on how you measure the size of the input. It wouldn't matter if it were just a constant factor, but you can apply squaring multiple times. In effect, it's easy to see that squaring can be used to emulate exponentiation such that the size of the input only increases by a constant factor. Mar 18 '13 at 18:03

a variation of Posts Correspondence Problem for bounded length input (but not the standard "bounded" version eg in Garey/Johnson that is called "bounded PCP" that limits the number of blocks in the solution to the cardinality of the block set) is complete for NEXPSpace and therefore larger than NP which is properly in Pspace. 

ie let there also be an input parameter $n$ specified in binary that determines the maximal length of the PCP answer. this is apparently complete for NEXPSpace via a straightfwd proof. havent seen a proof in the literature. it proceeds in a way similar to the construction relating it to TMs in 

note that all problems that are known to be larger than NP are also larger than PSpace. otherwise it (a proof of a language that is not in NP but is still in PSpace) might be something close to a coNP$\neq$NP and therefore also P$\neq$NP proof (because P is closed under complement), or resolve some other "nearby" currently open complexity class separation.

• more directly a language not in NP but in PSpace would be a NP$\neq$PSpace proof (currently open).
– vzn
Mar 16 '13 at 15:07