1: \begin{abstract}

2: %     \input{abstract}

3: Data vectors generalise finite multisets: they

4: are finitely supported functions into a commutative monoid.

5: We study the question if a given data vector can be expressed

6: as a finite sum 

7: of others,

8: only assuming that 1) the domain is countable

9: and 2) the given set of base vectors is finite up to permutations of the domain.

10: 

11: Based on a succinct representation of the involved permutations

12: as integer linear constraints, we derive that

13: positive instances can be witnessed

14: in a bounded subset of the domain.

15: 

16: For data vectors over a group 

17: we moreover

18: study when a data vector is reversible, that is, if its inverse is

19: expressible using only nonnegative coefficients.

20: We show that

21: if all base vectors are reversible

22: then the expressibility problem reduces to checking membership

23: in finitely generated subgroups. 

24: Moreover, checking reversibility also reduces to such membership tests.

25: 

26: 

27: 

28: These questions naturally appear in the analysis of counter machines extended with unordered data:

29: namely, for data vectors over $(\Z^d,+)$ expressibility directly corresponds to

30: checking state equations for

31: Coloured Petri nets where tokens can only be tested for equality.

32: We derive that in this case, expressibility is in \NP, and in $\P$ for reversible instances.

33: These upper bounds are tight: they match the lower bounds for standard integer vectors (over singleton domains).

34: 

35: 

36: \end{abstract}

37: