References & Citations
Computer Science > Formal Languages and Automata Theory
Title: Flattability of Priority Vector Addition Systems
(Submitted on 14 Feb 2024 (v1), last revised 30 Apr 2024 (this version, v2))
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.
Submission history
From: Roland Guttenberg [view email][v1] Wed, 14 Feb 2024 13:57:25 GMT (255kb,D)
[v2] Tue, 30 Apr 2024 13:30:47 GMT (250kb,D)
Link back to: arXiv, form interface, contact.