The reachability problem for vector addition systems with a stack is not elementary
arXiv:1310.1767
Abstract
By adapting the iterative yardstick construction of Stockmeyer, we show that the reachability problem for vector addition systems with a stack does not have elementary complexity. As a corollary, the same lower bound holds for the satisfiability problem for a two-variable first-order logic on trees in which unbounded data may label only leaf nodes. Whether the two problems are decidable remains an open question.
Informal presentation, 6th International Workshop on Reachability Problems (RP), Bordeaux, September 2012