On the Length of Strongly Monotone Descending Chains over $\mathbb{N}^d$

TL;DR

This paper demonstrates that the length of certain strongly monotone descending chains in $ ^d$ aligns with recent bounds on coverability problems, leading to improved complexity bounds for backward coverability algorithms in vector addition systems.

Contribution

It shows that the tight $n^{2^{O(d)}}$ bound applies to chains from the backward coverability algorithm, extending the analysis to more general settings and improving complexity bounds.

Findings

Bound on chain length matches recent coverability bounds

Backward coverability algorithm's runtime is tightly bounded

Improved complexity bounds for invertible affine nets

Abstract

A recent breakthrough by K\"unnemann, Mazowiecki, Sch\"utze, Sinclair-Banks, and Wegrzycki (ICALP, 2023) bounds the running time for the coverability problem in $d$-dimensional vector addition systems under unary encoding to $n^{2^{O(d)}}$, improving on Rackoff's $n^{2^{O(d\lg d)}}$ upper bound (Theor. Comput. Sci., 1978), and provides conditional matching lower bounds. In this paper, we revisit Lazi\'c and Schmitz' "ideal view" of the backward coverability algorithm (Inform. Comput., 2021) in the light of this breakthrough. We show that the controlled strongly monotone descending chains of downwards-closed sets over $\mathbb{N}^d$ that arise from the dual backward coverability algorithm of Lazi\'c and Schmitz on $d$-dimensional unary vector addition systems also enjoy this tight $n^{2^{O(d)}}$ upper bound on their length, and that this also translates into the same bound on the running time of the backward coverability algorithm. Furthermore, our analysis takes place in a more general setting than that of Lazi\'c and Schmitz, which allows to show the same results and improve on the 2EXPSPACE upper bound derived by Benedikt, Duff, Sharad, and Worrell (LICS, 2017) for the coverability problem in invertible affine nets.