Reachability in Priority Vector Addition Systems

Vector addition systems (VAS), also known as Petri nets, are a popular model of concurrent systems. Configurations are tuples in $\mathbb{N}^d$, and a step consists of adding a given vector in $\mathbb{Z}^d$. 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. Many interesting techniques have been developed for normal VAS, for example Leroux has shown that VAS admit semilinear inductive invariants, which leads to an algorithm for reachability based on two semi-algorithms: If the target is reachable, guess the path, otherwise guess the separating semilinear inductive invariant and verify it. Recently interest has emerged in trying to extend these properties to VAS with additional mechanisms, like VAS with a pushdown stack, (unordered) data or, as considered in this talk, with nested zero tests, called Priority VAS. We give a new characterization of reachability relations of Priority VAS as regular expressions over reachability relations of standard VAS and use it to reprove that also VAS with nested zero tests admit semilinear inductive invariants. Furthermore, we prove that every semilinear Priority VAS is flattable, i. e. intuitively that nested loops can be removed if the Priority VAS is semilinear. This result was unknown even for a single zero test. The corresponding paper was published in ICALP 2024 and is available at https: //doi. org/10. 4230/LIPIcs. ICALP. 2024. 141

Authors

• Roland Guttenberg

Keywords

No keywords are indexed for this paper.