The Geometry of Reachability in Continuous Vector Addition Systems with States

TL;DR

This paper explores the geometric structure of reachability sets in continuous vector addition systems with states, revealing their composition, and introduces efficient algorithms for reachability analysis, while also identifying complexity boundaries with zero tests.

Contribution

It characterizes the geometry of reachability sets as Minkowski sums of convex cones and zonotopes, and provides polynomial-time algorithms for reachability in fixed dimensions.

Findings

Reachability sets are almost Minkowski sums of convex cones and zonotopes.

Short linear path schemes suffice to witness reachability in fixed dimensions.

Adding zero tests makes the reachability problem intractable even for low dimensions.

Abstract

We study the geometry of reachability sets of continuous vector addition systems with states (VASS). In particular we establish that they are almost Minkowski sums of convex cones and zonotopes generated by the vectors labelling the transitions of the VASS. We use the latter to prove that short so-called linear path schemes suffice as witnesses of reachability in continuous VASS of fixed dimension. Then, we give new polynomial-time algorithms for the reachability problem for linear path schemes. Finally, we also establish that enriching the model with zero tests makes the reachability problem intractable already for linear path schemes of dimension two.