# Improved Ackermannian lower bound for the Petri nets reachability problem

arXiv: https://arxiv.org/abs/2105.08551 · HTML: https://mlsanity.com/paper/2105.08551/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 41 references that are in the map.
- First posted on arXiv 18 May 2021.

## Builds on (most cited first, 12 of 12)

- [Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension](https://mlsanity.com/paper/1903.08575/) (2019)
- [The Reachability Problem for Petri Nets is Not Primitive Recursive](https://mlsanity.com/paper/2104.12695/) (2021)
- [Demystifying Reachability in Vector Addition Systems](https://mlsanity.com/paper/1503.00745/) (2015)
- [The Reachability Problem for Petri Nets is Not Elementary](https://mlsanity.com/paper/1809.07115/) (2018)
- [Reachability in Vector Addition Systems is Ackermann-complete](https://mlsanity.com/paper/2104.13866/) (2021)
- [Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-complete](https://mlsanity.com/paper/1412.4259/) (2014)
- [VERIFAS: A Practical Verifier for Artifact Systems](https://mlsanity.com/paper/1705.10007/) (2017)
- [Complexity Hierarchies Beyond Elementary](https://mlsanity.com/paper/1312.5686/) (2013)
- [Linear Equations with Ordered Data](https://mlsanity.com/paper/1802.06660/) (2018)
- [Ordered Navigation on Multi-attributed Data Words](https://mlsanity.com/paper/1404.6064/) (2014)
- [Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete](https://mlsanity.com/paper/1602.00477/) (2016)
- [Reasoning about Data Repetitions with Counter Systems](https://mlsanity.com/paper/1604.02887/) (2016)

## Built on by (most cited first, 2 of 2)

- [Reachability in Symmetric VASS](https://mlsanity.com/paper/2506.23578/) (2025)
- [Solvability of orbit-finite systems of linear equations](https://mlsanity.com/paper/2201.09060/) (2022)

## Abstract (arXiv)

Petri nets, equivalently presentable as vector addition systems with states, are an established model of concurrency with widespread applications. The reachability problem, where we ask whether from a given initial configuration there exists a sequence of valid execution steps reaching a given final configuration, is the central algorithmic problem for this model. The complexity of the problem has remained, until recently, one of the hardest open questions in verification of concurrent systems. A first upper bound has been provided only in 2015 by Leroux and Schmitz, then refined by the same authors to non-primitive recursive Ackermannian upper bound in 2019. The exponential space lower bound, shown by Lipton already in 1976, remained the only known for over 40 years until a breakthrough non-elementary lower bound by Czerwi'nski, Lasota, Lazic, Leroux and Mazowiecki in 2019. Finally, a matching Ackermannian lower bound announced this year by Czerwi'nski and Orlikowski, and independently by Leroux, established the complexity of the problem. Our primary contribution is an improvement of the former construction, making it conceptually simpler and more direct. On the way we improve the lower bound for vector addition systems with states in fixed dimension (or, equivalently, Petri nets with fixed number of places): while Czerwi'nski and Orlikowski prove Fk-hardness (hardness for kth level in Grzegorczyk Hierarchy) in dimension 6k, our simplified construction yields Fk-hardness already in dimension 3k+2.