2013/10/07 by Ranko Lazić, Lazic, Ranko · 2 citations
Computer Science · #F.3.1 #F.4.3 #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1310.1767
openalex publication_date 2013/10/07 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.