2019/03/20 by Jérôme Leroux, Sylvain Schmitz · 63 citations
Computer Science · Mathematics · #Ackermann function #Combinatorics #Computer science #Dimension (graph theory) #Discrete mathematics #Formal Methods in Verification #Logic, programming, and type systems #Mathematics #Reachability #Security and Verification in Computing #Upper and lower bounds #cs.LO
paper · pdf · open access · doi:10.1109/lics.2019.8785796
published as 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019)
arxiv created 2019/03/20 · openalex publication_date 2019/06/01 · openalex created_date 2019/08/13 · arxiv updated 2019/08/20 · openalex updated_date 2026/07/29
The reachability problem in vector addition systems is a central question, not only for the static verification of these systems, but also for many inter-reducible decision problems occurring in various fields. The currently best known upper bound on this problem is not primitive-recursive, even when considering systems of fixed dimension. We provide significant refinements to the classical decomposition algorithm of Mayr, Kosaraju, and Lambert and to its termination proof, which yield an ACKERMANN upper bound in the general case, and primitive-recursive upper bounds in fixed dimension. While this does not match the currently best known TOWER lower bound for reachability, it is optimal for related problems.