Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Sylvain Schmitz, Lia Schütze

TL;DR

The paper addresses the length of controlled strongly monotone descending chains over $\mathbb{N}^d$ that arise in backward coverability analyses for vector addition systems and related models. By extending the notion of thinness to a generalized setting, it proves a tight bound of $n^{2^{O(d)}}$ on the length of such chains, which directly yields the same bound on the running time of the backward coverability algorithm in unary-encoded $d$-dimensional VAS. The framework also applies to invertible affine nets, achieving identical length bounds and leading to EXPSPACE-completeness results for coverability when $d$ is part of the input, and to an improved upper bound for the algorithm in this broader setting. Overall, the work unifies a general theory of controlled sequences and thin order ideals to provide tighter, conditional-optimal complexity bounds across VAS, affine nets, and related WSTS, with implications for both theory and verification practice.

Abstract

A recent breakthrough by Künnemann, Mazowiecki, Schütze, 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ć 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ć 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ć 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.

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

TL;DR

The paper addresses the length of controlled strongly monotone descending chains over that arise in backward coverability analyses for vector addition systems and related models. By extending the notion of thinness to a generalized setting, it proves a tight bound of on the length of such chains, which directly yields the same bound on the running time of the backward coverability algorithm in unary-encoded -dimensional VAS. The framework also applies to invertible affine nets, achieving identical length bounds and leading to EXPSPACE-completeness results for coverability when is part of the input, and to an improved upper bound for the algorithm in this broader setting. Overall, the work unifies a general theory of controlled sequences and thin order ideals to provide tighter, conditional-optimal complexity bounds across VAS, affine nets, and related WSTS, with implications for both theory and verification practice.

Abstract

A recent breakthrough by Künnemann, Mazowiecki, Schütze, Sinclair-Banks, and Wegrzycki (ICALP, 2023) bounds the running time for the coverability problem in -dimensional vector addition systems under unary encoding to , improving on Rackoff's upper bound (Theor. Comput. Sci., 1978), and provides conditional matching lower bounds. In this paper, we revisit Lazić 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 that arise from the dual backward coverability algorithm of Lazić and Schmitz on -dimensional unary vector addition systems also enjoy this tight 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ć 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.
Paper Structure (31 sections, 11 theorems, 29 equations, 1 figure)

This paper contains 31 sections, 11 theorems, 29 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Well-Quasi-Orders
  3. Descending Chains.
  4. Fine-grained Bounds for VAS Coverability.
  5. Thinness.
  6. Contributions.
  7. Well-Quasi-Orders and Ideals
  8. Well-Quasi-Orders.
  9. Order Ideals.
  10. Effective Representations over $\mathbb{N}^d$.
  11. Proper Ideals and Monotonicity.
  12. Controlled Sequences.
  13. Main Result
  14. Thinness
  15. Thinness Lemma
  16. ...and 16 more sections

Key Result

Lemma 3.4

Consider a $(g,n_0)$-controlled strongly monotone descending chain $D_0 \supsetneq D_1\supsetneq\cdots$ of downwards-closed subsets of $\mathbb{N}^d$. If $I_\ell$ is a proper order ideal at some step $\ell$, then $I_\ell$ is thin and $\ell\leq L_{\mathrm{fdim}\,I_\ell}$.

Figures (1)

  • Figure 1: A descending chain $D_0\supsetneq D_1\supsetneq\cdots\supsetneq D_5$ over $\mathbb{N}^2$lazic21.

Theorems & Definitions (39)

  • Remark 3.1: Monotonicity of $(N_i)_{0\leq i\leq d}$ and $(L_{i})_{0\leq i\leq d}$
  • Definition 3.2: Thin order ideal
  • Remark 3.3: Number of thin order ideals
  • Lemma 3.4: Thinness
  • Claim 3.5
  • proof : Proof of \ref{['cl-thin']}
  • proof : Proof of \ref{['lem-thin']}
  • Theorem 3.6: Length function for strongly monotone descending chains
  • proof
  • Corollary 3.7
  • ...and 29 more