Membership and separation problems inside two-variable first order logic

This thesis studies the expressive power of restricted fragments of first order logic on words with the order predicate. In particular, we consider particular instances of the following two questions.

Given a regular language L, and a fragment of first order logic, can L be described by formulae in this fragment?

Given two regular languages L1 and L2, and a fragment of first order logic, can we find a language L which can be described by formulae in this fragment such that L1 is a subset of L and the intersection of L2 and L is empty.

The former is known as the membership problem, and the latter the separation problem. These problems are well studied in the theory of regular languages, and their solution has often relied on tools from algebra, such as finite monoids and pointlikes.

We consider formulae using only two variables, a fragment known as FO2[<]. Inside this fragment, we make further restrictions regarding the alternation depth of the formula, i.e. how many times we are allowed to switch between existential and universal quantifiers along a parse tree of a formula.

For languages of finite words, membership for these fragments has already been solved. We generalise these results in multiple directions.

First, we solve the membership problem for the aforementioned fragments for inf-regular languages, i.e. languages consisting of both infinitely and finitely long words. This in particular solves the membership problem for omega-regular languages, i.e. those containing only infinitely long words. Our main tool is to impose algebraic conditions on the syntactic monoid: a monoid which can be computed from any major presentation of regular languages. For the lower levels, we also need to consider topological properties of the languages.

The above shows that membership for inf- and omega-regular languages is decidable. However, given a language presented by an automata, calculating the syntactic monoid is generally not efficient. Our second main contribution is therefore an efficient way to decide membership for languages presented by deterministic finite automata (for regular languages) and Carton--Michel automata (for omega-regular languages). We give forbidden patterns for these fragments; that is, we specify structures which cannot be present in an automata for it to be expressible by formulae of a particular alternation depth. Finding these patterns can be done in non-deterministic logarithmic space. Together with a reduction from graph reachability, this shows that the membership problem for these fragments is NL-complete when the input is given as a deterministic finite automaton or Carton--Michel automaton.

Our final main contribution is a solution to the separation and covering problem for languages consisting of finite words. We introduce conelikes as a generalisation of pointlikes for ordered monoids, and use these to solve the covering problem (which generalises separation) for the aforementioned fragments.