I see other comments have appeared while I was writing mine. Let me still post it.

Tobias wrote:

> And as John's book explains on p.251, the complexity of reachability is at least doubly exponential.

No, I said that the complexity of deciding the validity of statements in Presburger arithmetic is at least doubly exponential. This is an axiom system for arithmetic that mentions addition and multiplication only. Unlike Peano arithmetic, it's decidable.

The situation for Petri net reachability is much less well understood. In 1976, [Roger Lipton showed that its complexity is at least exponential](http://www.cs.yale.edu/publications/techreports/tr63.pdf). More precisely, he showed the for any \\(c > 0\\) the worst-case run-time for deciding Petri net reachability exceeds \\(2^{cn}\\) where \\(n\\) is the size of the problem.

However, the best known _upper_ bound for the complexity is much worse. In 1981 Ernst Meyr found an algorithm that decides Petri net reachability. But its runtime grows faster than every primitive recursive function! For example, faster than this series

$$ 1, 2^2, 2^{2^2}, 2^{2^{2^2}}, \dots $$

but in fact much faster than that.

There's a tantalizing connection between Presburger arithmetic and Petri net reachability, discussed in my book, but it hasn't (yet) sufficed to get a doubly exponential algorithm for Petri net reachability.