UNderstanding Regular Expressions, Automata and Logics – UNREAL

This project is in the field of the theory of regular languages of words and trees. Its objective is to understand classes of such languages.

The standard way of "understanding" a class of regular languages is the "membership problem", which consists in designing an algorithm to decide whether an input language is in the class or not. Despite continuous progress on this problem since the 1960s, fundamental questions remain open, such as the decidability of the levels of quantifier alternation hierarchies in 1st-order logic.

In recent years, advances have been made by the participants in this project concerning these hierarchies. Our scientific objectives are:

- to understand the levels of quantifier alternation hierarchies for finite words that are beyond our grasp. To achieve this task, we propose to study a new problem, defined in the project. We believe that understanding it will enable us to obtain results that seem out of reach with current techniques:

- to lift to infinite words what has already been obtained on finite words. Ideally, we want to obtain reductions from infinite words to finite words. Historically, results on infinite words have always been inspired by those obtained on finite words. This makes the objective realistic.

- to develop the approach for finite tree languages. Characterizing descriptive formalisms on trees is notoriously very difficult (in particular, the membership problem for 1st-order logic seems to be out of reach). However, the results obtained on words concern classes considered as manageable for finite trees. This gives us hope that the theory, which does not currently exist, can be developed in this context.