In computational complexity theory, EXPSPACE is the set of all decision problems solvable by a deterministic Turing machine in exponential space, i.e., in
to be a linear function, but most authors instead call the resulting class ESPACE.
If we use a nondeterministic machine instead, we get the class NEXPSPACE, which is equal to EXPSPACE by Savitch's theorem.
[1] Alur and Henzinger extended linear temporal logic with times (integer) and prove that the validity problem of their logic is EXPSPACE-complete.
[3] The reachability problem for Petri nets was known to be EXPSPACE-hard for a long time,[4] but shown to be nonelementary,[5] so probably not in EXPSPACE.