Linear equations for unordered data vectors in $[D]^k\to{}Z^d$

TL;DR

This paper generalizes linear equations to data vectors that are functions from subsets of unordered data, analyzing their solvability complexity, which varies between polynomial and nondeterministic exponential time.

Contribution

It introduces a new class of linear equations for data vectors from subsets of unordered data and characterizes their solvability complexity.

Findings

Nonnegative-integer solvability is in nondeterministic exponential time.

Integer solvability is in polynomial time.

Applications in analyzing extended vector addition systems and Petri nets.

Abstract

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.