Regular Separability of Well Structured Transition Systems

TL;DR

This paper proves that disjoint languages recognized by well-structured transition systems are regularly separable under mild conditions, and explores the complexity of separators for Petri nets, revealing limitations of WSTS subclasses.

Contribution

It establishes regular separability for disjoint WSTS languages and analyzes the complexity bounds for separators in Petri nets.

Findings

Disjoint WSTS languages are regularly separable.

Languages and their complements recognized by WSTS are regular.

Complexity bounds for regular separators in Petri nets.

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.