Abstract

We investigate the languages recognized by well-structured transition systems (WSTS). Our first result shows that, under very mild assumptions, every two disjoint WSTS languages are regularly separable: There is a regular language containing one of them and being disjoint from the other. The result has theoretical as well as practical consequences. On the theoretical side, 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. On the practical side, regular approximations turn out to be complete for compositional safety verification of WSTS. 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.


Legal Disclosure | Privacy Statement