Generalized linear equations with unordered data

Consider a Petri net in which every token carries a k-element set of data, and whenever we fire a transition
then data from consumed and produced tokens are compared for equality and disequality. Such an extension
of Petri Nets allows more precise modeling than normal Petri Nets. Of course, comparing to Patri nets the analysis
of data nets is harder and natural problems become undecidable, but not all of them. In this work, we prove that so-called
integer reachability, useful as a witness of nonreachability in standard sens, is in NEexpTime.
The case when k=1 was considered in the paper published at LICS 2017.
During the talk, I will focus on the cases when k=1 and k=2, to illustrate developed techniques.