PTL-separability and closures for WQOs on words

TL;DR

This paper introduces a broad class of well-quasi-orderings on words that unify various language classes, enabling decision procedures for separability and effective computation of downward closures, with applications to logical fragments.

Contribution

It generalizes PTL-separability and closure results for WQOs on words, providing a unified framework and decision algorithms for separability and downward closures.

Findings

Decidability of separability by PTLs for many language classes

Reduction of problems to the simultaneous unboundedness problem (SUP)

Decidability of separability for a fragment of first-order logic with modular predicates

Abstract

We introduce a flexible class of well-quasi-orderings (WQOs) on words that generalizes the ordering of (not necessarily contiguous) subwords. Each such WQO induces a class of piecewise testable languages (PTLs) as Boolean combinations of upward closed sets. In this way, a range of regular language classes arises as PTLs. Moreover, each of the WQOs guarantees regularity of all downward closed sets. We consider two problems. First, we study which (perhaps non-regular) language classes permit a decision procedure to decide whether two given languages are separable by a PTL with respect to a given WQO. Second, we want to effectively compute downward closures with respect to these WQOs. Our first main result that for each of the WQOs, under mild assumptions, both problems reduce to the simultaneous unboundedness problem (SUP) and are thus solvable for many powerful system classes. In the second main result, we apply the framework to show decidability of separability of regular languages by $\mathcal{B}\Sigma_1[<, \mathsf{mod}]$, a fragment of first-order logic with modular predicates.