Integer Reachability in Data VASS

Overview & Synopsis

Data Petri nets are an extension of plain Petri nets where, intuitively speaking, tokens carry data values, and transitions may perform equality tests on data values involved. Likewise, data vector addition systems with states (data VASS) are an extension of plain VASS, and equivalent to data Petri nets. The decidability status of the reachability problem in this model is an established and long-standing open question. In this paper we perform a major step towards resolving this question: we show decidability of the integer reachability problem, where the counters can drop below zero. Contrarily to plain VASS, where integer reachability reduces to integer linear programming, the setting of data VASS is significantly more complex, mostly due to the fact that the state spaces are not finite but orbit-finite (like in register automata). Our decision procedure combines an iterative refinement, resembling the KLM decomposition in plain VASS, with a termination argument via a novel way of bounding the number of data values appearing in the refinement. As corollaries, we deduce decidability of a number of decision problems concerning register automata and data Petri nets.