A new characterisation for FO2 over finite words

First-Order Logic with two variables, over finite words, is known for having many semantic characterisations: turtle languages, unambiguous monomials, deterministic partially ordered 2-way automata...

In this talk, we will focus on the second one: a monomial over an alphabet A is a language of the shape A_0 a_0 A_1 ... A_{n-1} a_{n-1} A_n, where each A_i is a subalphabet, and each a_i an individual letter; it is said unambiguous if every word in the language admits a unique decomposition. It is known that a language is definable in FO2 iff it is a union of such unambiguous monomials.

We exploit this characterisation to show that a language definable in FO2 can be described as a union of what we call split trees: those are finite trees in which the children of each internal node describe a split (a particular sort of unambiguous monomials). With this new characterisation, some problems about FO2 may be solved via a straightforward reduction to the monadic theory of the omega-branching tree, which is known to be decidable. More precisely: consider such a problem P, and an instance inst of it, one can construct an MSO formula phi_{P,i} over the omega-branching tree such that it is satisfiable if and only if inst is indeed in P.

Originally, this word was motivated by the problem of uniformisation in FO2 (does a given regular relation admit a uniformisation that is definable in FO2?). We begin the talk by introducing this problem, before developing our tools. We then focus on the better-known separation problem (given two disjoint regular languages, is there a language definable in FO2 that contains one and does not intersect the other?), and show how this problem (first solved by Place and Zeitoun) can be also be solved via our new method.

This is a joint work with Dr Nathan Lhote and Dr hab. Michał Skrzypczak.