JCJC - Jeunes chercheuses & jeunes chercheurs

# Jeux et Automates, Décidabilité et Extensions – JADE

Submission summary

Automata theory is born fifty years ago with the seminal works of Kleene. Though the primary motivation was the study of neural networks, the application field has widely spread and now covers diversified topics such as linguistic, theory of control, biology, data compression, system analysis, among many others. Many variations around this theory have been developed and connections with deep mathematical theories -- such as logic, algebra, or topology -- have been uncovered. In this project, we put ourselves in this perspective and consider variants of automata, with a particular interest for the theory of finite automata over infinite objects, such as words or trees. In this later case, the automata have a finite set of states, a standard transition function, together with special annotations allowing to define the notion of an accepting run, even when this run is infinite. The fundamental result of Rabin states that so-called Rabin automata over infinite trees form a boolean algebra. Game theory is also a wide subject: economy, mathematics, and computer science are its main application fields. In computer science, a game consists of two antagonistic players, that performs, in a turn based way, a possibly infinite number number of moves. Hence, determining the winner of the game is a major algorithmic question. Games happen to be a powerful proof tool as many decision problems can be translated into equivalent games. Then solving that game is the same as deciding the original problem. To solve the game, a special attention is generally devoted to the notion strategy. A typical reasoning consists in proving that if one player can win, he can actually do it using a strategy having a very special form: hence this drastically reduces the number of strategies to consider, and leads to consider only finitely many of them which permits to perform an exhaustive search to conclude. This general framework is in particular at the very heart of every modern presentation of Rabin's Theorem. Several problems are of special interest. - Tree automata with equality constraints between browsers. We allow in the transition function equality and disequality tests between sons of the current node. If in the case of finite trees, emptiness is decidable, the problem is more delicate for infinite trees. Understanding the origin of the difficulty and then solving it remains to be done. - Decidable extensions of the monadic second order (MSO) theory. Recent works show that, as opposed to the common opinion, it is possible to solve logics which are more expressive than MSO. Those works offers many perspectives in verification, and entail the definition of new families of automata, more general than the usual ones. Their study, as well as the one of the associated games form an important subject of study for the members of the project. - Positionally determined games. The simplest strategies are the one which do not use memory -- positional ones. The existence of such a strategy depends simultaneously on the winning condition and on the structure of the game graph. We aim at characterizing over a family of game graphs, which are the winning condition entailing positional winning strategies. This research has been pursued for finite game graphs, and for infinite game graphs. The game graphs involved in automata theory are more restricted, and have to be investigated. - Parity index of a language of infinite trees. The parity index measures the topological complexity of a language and the efficiency of several algorithm strongly rely on it. Using recent approaches we expect to give an algorithm that computes it. The good knowledge of the members of the project in both fields of automata theory and games, as well as in logic should allow them to attack in a relevant way some important questions in the field, as those previously mentioned. Furthermore, their ongoing collaborations will provide the dynamism and visibility needed by the project, as well as attract extra researchers around them.

## Project coordination

Thomas COLCOMBET (Organisme de recherche)

The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.

## Partner

Help of the ANR 89,630 euros
Beginning and duration of the scientific project: - 36 Months