Given two families of sets F and G, the F-separability problem for G asks whether for two given sets U, V in G there exists a set S in F, such that U is included in S and V is disjoint with S. We consider two families of sets F: modular sets S which are subsets of N^d, defined as unions of equivalence classes modulo some natural number n in N, and unary sets, which extend modular sets by requiring equality below a threshold n, and equivalence modulo n above n. Our main result is decidability of modular- and unary-separability for the class G of reachability sets of Vector Addition Systems, Petri Nets, Vector Addition Systems with States, and for sections thereof.
展开▼
