HackerPapers

arXiv:2104.13866cs.FL

Reachability in Vector Addition Systems is Ackermann-complete

Wojciech Czerwiński, Łukasz Orlikowski

Abstract

Vector Addition Systems and equivalent Petri nets are a well established models of concurrency. The central algorithmic problem for Vector Addition Systems with a long research history is the reachability problem asking whether there exists a run from one given configuration to another. We settle its complexity to be Ackermann-complete thus closing the problem open for 45 years. In particular we prove that the problem is $\mathcal{F}_k$-hard for Vector Addition Systems with States in dimension $6k$, where $\mathcal{F}_k$ is the $k$-th complexity class from the hierarchy of fast-growing complexity classes.

arXiv comments
Journal reference
DOI
Subjects
cs.FLFormal Languages and Automata Theory cs.LOLogic in Computer Science

On Hacker News

Linked by 2 identifiable commenters in 3 comments across 3 threads, from Dec 2023 to May 2026.

Comments linking this paper, per year.

Discussed in comments3 threads

    • As TLA+ uses state machines that can define infinite state spaces, checking arbitrary temporal logic formulas is undecidable in the general case. Using a TLC model checker to verify invariants or properties, finding a valid counterexample can scale non-elementarily. In fact, in…

      nyrikkiView on HNParent context

    • > Hmm.. I'd love to see a more formal statement of this, because it feels unintuitive. The problem is called "Vector Addition System Reachability", and the proof that it's Ackermann-complete is here: https://arxiv.org/pdf/2104.13866 (It's actually for "Vector Addition Systems…

      hwayneView on HNParent context

    • If you're up for the challenge, the original paper proving ACK-completeness is here: https://arxiv.org/pdf/2104.13866.pdf

      hwayneView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.