Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Decidability and Complexity of Decision Problems for Affine Continuous VASS

A. R. Balasubramanian

TL;DR

This work introduces affine continuous VASS, extending continuous VASS with affine updates and fractional firings to model richer counter behaviors. It achieves an almost-complete classification of the decidability status for reachability, coverability, and state-reachability across matrix-classes, showing reachability is decidable only for permutation-matrix classes and state-reachability only for non-negative-matrix classes, with coverability undecidable in many natural settings but decidable in notable subfamilies; tight upper and lower bounds are provided for most cases. The authors develop techniques including support-abstraction graphs, pumping arguments, ELRA encodings, and reductions from Boolean programs to establish these results, yielding complexities from NP to NEXP and PSPACE. The findings illuminate the trade-offs between over-approximation power and decidability in affine-continuous models, guiding verification approaches for concurrent-counter systems and highlighting remaining gaps (notably the weighted/overlapping-edge case for coverability).

Abstract

Vector addition system with states (VASS) is a popular model for the verification of concurrent systems. VASS consists of finitely many control states and a set of counters which can be incremented and decremented, but not tested for zero. VASS is a relatively well-studied model of computation and many results regarding the decidability of decision problems for VASS are well-known. Given that the complexity of solving almost all problems for VASS is very high, various tractable over-approximations of the reachability relation of VASS have been proposed in the literature. One such tractable over-approximation is the so-called continuous VASS, in which counters are allowed to have non-negative rational values and whenever an update is performed, the update is first scaled by an arbitrary non-zero fraction. In this paper, we consider affine continuous VASS, which extend continuous VASS by allowing integer affine operations. Affine continuous VASS serve as an over-approximation to the model of affine VASS, in the same way that continuous VASS over-approximates the reachability relation of VASS. We investigate the tractability of affine continuous VASS with respect to the reachability, coverability and state-reachability problems for different classes of affine operations and we prove an almost-complete classification of the decidability of these problems. Namely, except for the coverability problem for a single family of classes of affine operations, we completely determine the decidability status of these problems for all classes. Furthermore, except for this single family, we also complement all of our decidability results with tight complexity-theoretic upper and lower bounds.

Decidability and Complexity of Decision Problems for Affine Continuous VASS

TL;DR

This work introduces affine continuous VASS, extending continuous VASS with affine updates and fractional firings to model richer counter behaviors. It achieves an almost-complete classification of the decidability status for reachability, coverability, and state-reachability across matrix-classes, showing reachability is decidable only for permutation-matrix classes and state-reachability only for non-negative-matrix classes, with coverability undecidable in many natural settings but decidable in notable subfamilies; tight upper and lower bounds are provided for most cases. The authors develop techniques including support-abstraction graphs, pumping arguments, ELRA encodings, and reductions from Boolean programs to establish these results, yielding complexities from NP to NEXP and PSPACE. The findings illuminate the trade-offs between over-approximation power and decidability in affine-continuous models, guiding verification approaches for concurrent-counter systems and highlighting remaining gaps (notably the weighted/overlapping-edge case for coverability).

Abstract

Vector addition system with states (VASS) is a popular model for the verification of concurrent systems. VASS consists of finitely many control states and a set of counters which can be incremented and decremented, but not tested for zero. VASS is a relatively well-studied model of computation and many results regarding the decidability of decision problems for VASS are well-known. Given that the complexity of solving almost all problems for VASS is very high, various tractable over-approximations of the reachability relation of VASS have been proposed in the literature. One such tractable over-approximation is the so-called continuous VASS, in which counters are allowed to have non-negative rational values and whenever an update is performed, the update is first scaled by an arbitrary non-zero fraction. In this paper, we consider affine continuous VASS, which extend continuous VASS by allowing integer affine operations. Affine continuous VASS serve as an over-approximation to the model of affine VASS, in the same way that continuous VASS over-approximates the reachability relation of VASS. We investigate the tractability of affine continuous VASS with respect to the reachability, coverability and state-reachability problems for different classes of affine operations and we prove an almost-complete classification of the decidability of these problems. Namely, except for the coverability problem for a single family of classes of affine operations, we completely determine the decidability status of these problems for all classes. Furthermore, except for this single family, we also complement all of our decidability results with tight complexity-theoretic upper and lower bounds.
Paper Structure (33 sections, 34 theorems, 16 equations, 1 table)

This paper contains 33 sections, 34 theorems, 16 equations, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Contribution Part I - Decidability results
  4. Contribution Part II - Complexity results
  5. Undecidability results
  6. State-reachability for classes with negative entries
  7. Coverability for non-negative classes with zero-rows/columns
  8. Reachability for non-negative classes with weighted/overlapping edges
  9. Decidability results and complexity upper bounds
  10. State-reachability for non-negative classes
  11. Coverability for non-negative classes with only self-loop matrices
  12. Reachability for non-negative classes with only permutation matrices
  13. Complexity lower bounds
  14. State-reachability for non-negative classes with zero-rows/columns
  15. Non-negative classes with only permutation matrices
  16. ...and 18 more sections

Key Result

theorem 1

The reachability problem for a class $\mathcal{C}$ is decidable (and in NEXP) if $\mathcal{C}$ contains only permutation matrices. Otherwise, the reachability problem is undecidable.

Theorems & Definitions (34)

  • theorem 1
  • theorem 2
  • theorem 3
  • theorem 4
  • theorem 5
  • theorem 6
  • theorem 7
  • theorem 8
  • theorem 9
  • theorem 10
  • ...and 24 more