PTL-separability and closures for WQOs on words.

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