Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Flattability of Priority Vector Addition Systems

Roland Guttenberg

TL;DR

The paper addresses the reachability problem for Priority Vector Addition Systems (PVAS) by proving that semilinear reachability relations are flattenable and that PVAS admit semilinear inductive invariants. It introduces a RegEx characterization of PVAS reachability as RegEx over VAS reachability with the Kleene star restricted to monotone relations, and develops a novel well-quasi-order on PVAS runs to enable pumping arguments. By combining RegEx equivalence, wqo-based pumping, and geometric notions of cones and smooth periodic sets, the authors extend Leroux’s results from VAS to PVAS, establishing flattenability and invariants for the semilinear case. These results provide a foundational framework for analyzing PVAS behavior and raise open questions about semilinearity decision problems and computational complexity, with potential relevance to Pushdown/Grammar-VASS extensions.

Abstract

Vector addition systems (VAS), also known as Petri nets, are a popular model of concurrent systems. Many problems from many areas reduce to the reachability problem for VAS, which consists of deciding whether a target configuration of a VAS is reachable from a given initial configuration. One of the main approaches to solve the problem on practical instances is called flattening, intuitively removing nested loops. This technique is known to terminate for semilinear VAS. In this paper, we prove that also for VAS with nested zero tests, called Priority VAS, flattening does in fact terminate for all semilinear reachability relations. Furthermore, we prove that Priority VAS admit semilinear inductive invariants. Both of these results are obtained by defining a well-quasi-order on runs of Priority VAS which has good pumping properties.

Flattability of Priority Vector Addition Systems

TL;DR

The paper addresses the reachability problem for Priority Vector Addition Systems (PVAS) by proving that semilinear reachability relations are flattenable and that PVAS admit semilinear inductive invariants. It introduces a RegEx characterization of PVAS reachability as RegEx over VAS reachability with the Kleene star restricted to monotone relations, and develops a novel well-quasi-order on PVAS runs to enable pumping arguments. By combining RegEx equivalence, wqo-based pumping, and geometric notions of cones and smooth periodic sets, the authors extend Leroux’s results from VAS to PVAS, establishing flattenability and invariants for the semilinear case. These results provide a foundational framework for analyzing PVAS behavior and raise open questions about semilinearity decision problems and computational complexity, with potential relevance to Pushdown/Grammar-VASS extensions.

Abstract

Vector addition systems (VAS), also known as Petri nets, are a popular model of concurrent systems. Many problems from many areas reduce to the reachability problem for VAS, which consists of deciding whether a target configuration of a VAS is reachable from a given initial configuration. One of the main approaches to solve the problem on practical instances is called flattening, intuitively removing nested loops. This technique is known to terminate for semilinear VAS. In this paper, we prove that also for VAS with nested zero tests, called Priority VAS, flattening does in fact terminate for all semilinear reachability relations. Furthermore, we prove that Priority VAS admit semilinear inductive invariants. Both of these results are obtained by defining a well-quasi-order on runs of Priority VAS which has good pumping properties.
Paper Structure (23 sections, 31 theorems, 1 equation, 2 figures)

This paper contains 23 sections, 31 theorems, 1 equation, 2 figures.

Table of Contents

  1. Introduction
  2. Regular expressions for Priority VAS.
  3. A well-quasi-order (wqo) on the set of runs of Priority VAS.
  4. Structure of the paper.
  5. Preliminaries
  6. Vector Addition Systems and Priority Vector Addition Systems
  7. Equivalence of PVASS and Regular Expressions over VASS
  8. A Well-Quasi-Order on Runs of Priority VAS
  9. Well-Quasi-Order for VAS
  10. Well-Quasi-Order for Expressions
  11. Comparison with other Well-Quasi-Orders
  12. Geometric Preliminaries
  13. Cones and periodic sets.
  14. Smooth Periodic Sets.
  15. Almost semilinear relations.
  16. ...and 8 more sections

Key Result

Theorem 7

A relation $\mathbf{X} \subseteq \mathbb{N}^{d'} \times \mathbb{N}^{d"}$ is a PVASS section iff $\mathbf{X}=\mathop{\mathrm{Rel}}\nolimits(\mathbf{E})$ for some $\mathbf{E}$.

Figures (2)

  • Figure 1: Example of a PVASS and an equivalent (for $x_{in}=0$) flattened version.
  • Figure 2: Typical example of a non-semilinear VAS HopcroftP79. Edges $e$ are only labelled with their update $f(e)$, since this is a VASS, i.e. every edge fulfills $g(e)=0$.

Theorems & Definitions (51)

  • Definition 1
  • Remark 2
  • Remark 3
  • Remark 4
  • Definition 5
  • Example 6
  • Theorem 7
  • Example 8
  • Lemma 8
  • Corollary 9
  • ...and 41 more