English

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

Data Structures and Algorithms 2024-07-03 v2 Computational Complexity Logic in Computer Science

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 dd-dimensional vector addition systems under unary encoding to n2O(d)n^{2^{O(d)}}, improving on Rackoff's n2O(dlgd)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 Nd\mathbb{N}^d that arise from the dual backward coverability algorithm of Lazi\'c and Schmitz on dd-dimensional unary vector addition systems also enjoy this tight n2O(d)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.

Keywords

Cite

@article{arxiv.2310.02847,
  title  = {On the Length of Strongly Monotone Descending Chains over $\mathbb{N}^d$},
  author = {Sylvain Schmitz and Lia Schütze},
  journal= {arXiv preprint arXiv:2310.02847},
  year   = {2024}
}