First-order Separation over Countable Scattered Linear Orders

We consider regular languages of words whose domain is a countable scattered linear ordering (examples of countable scattered linear orders include the set of integers or any countable ordinal). Given two regular languages, we want to decide whether there exists a formula of first-order logic that is satisfied by every word of the first language but by no word of the other. We prove that this problem is decidable using an algebraic construction: given a morphism from the set of all words to a finite scattered monoid, we show that one can effectively build a function that approximates the original morphism while being definable in first-order logic. Essentially, this approximant is obtained from the original morphism by forgetting about group-like phenomena and gap-detection using an algorithm resembling Henckell's saturation algorithm for computing aperiodic pointlike sets of finite semigroups. We also study the case of words indexed by countable ordinals (on which first-order logic admits a simpler characterisation), which was published at FoSSaCS '22, and separation by first-order logic extended with monadic quantification over Dedekind cuts. This is joint work with Thomas Colcombet and Sam van Gool.

Authors

• Rémi Morvan

Keywords

No keywords are indexed for this paper.