Title: Regular Separability of Well Structured Transition Systems,
Abstract: We investigate the languages recognized by well-structured transition systems
(WSTS) with upward and downward compatibility. Our first result shows that,
under very mild assumptions, every two disjoint WSTS languages are regular
separable: There is a regular language containing one of them and being
disjoint from the other. As a consequence, if a language as well as its
complement are both recognized by WSTS, then they are necessarily regular. In
particular, no subclass of WSTS languages beyond the regular languages is
closed under complement. Our second result shows that for Petri nets, the
complexity of the backwards coverability algorithm yields a bound on the size
of the regular separator. We complement it by a lower bound construction.