Following a recently considered generalisation of linear equations to unordered-data vectors and to ordered-data vectors, we perform a further generalisation to data vectors that are functions from k-element subsets of the unordered-data set to vectors of integer numbers. These generalised equations naturally appear in the analysis of vector addition systems (or Petri nets) extended so that each token carries a set of unordered data. We show that nonnegative-integer solvability of linear equations is in nondeterministic exponential time while integer solvability is in polynomial time.

Abstract We show that the existential fragment of Büchi arithmetic is strictly less expressive than full Büchi arithmetic of any base, and moreover establish that its $$\varSigma _2$$ Σ 2 -fragment is already expressively complete. Furthermore, we show that regular languages of polynomial growth are definable in the existential fragment of Büchi arithmetic.