On the Separability Problem of String Constraints

TL;DR

This paper investigates the problem of separating straight-line string constraints using different classes of languages, establishing undecidability results and providing decidability and complexity bounds for specific cases.

Contribution

It proves regular separability is undecidable, shows decidability with piece-wise testable languages, and offers an EXPSPACE algorithm for a positive fragment.

Findings

Regular separability is undecidable.

Decidability achieved with piece-wise testable languages.

EXPSPACE algorithm developed for a positive fragment.

Abstract

We address the separability problem for straight-line string constraints. The separability problem for languages of a class C by a class S asks: given two languages A and B in C, does there exist a language I in S separating A and B (i.e., I is a superset of A and disjoint from B)? The separability of string constraints is the same as the fundamental problem of interpolation for string constraints. We first show that regular separability of straight line string constraints is undecidable. Our second result is the decidability of the separability problem for straight-line string constraints by piece-wise testable languages, though the precise complexity is open. In our third result, we consider the positive fragment of piece-wise testable languages as a separator, and obtain an EXPSPACE algorithm for the separability of a useful class of straight-line string constraints, and a PSPACE-hardness result.