Thomas Colcombet: projet GALE


The project GALE (Games, Automata and Logic’s Extensions)

This project is now closed since December 31, 2015.

What is it?

The project GALE is a scientific project in computer science of the European Research Council funded from the European Union’s Seventh Framework Programme (FP7/2007-2013) under grant agreement n 259454.

Scientific objectives

The project GALE aims at generalizing the central decidability results of Büchi and Rabin to more general settings, and understanding the consequences of these extensions both at theoretical and applicative levels.

The original results of Büchi and Rabin state the decidability of monadic second-order logic (monadic logic for short) over infinite words and trees respectively. Those results are of such importance that Rabin’s theorem is also called the ‘Mother of all decidability results’.

The primary goal of this project is to demonstrate that it is possible to go significantly beyond the expressiveness of monadic logic, while retaining similar decidability results. We are considering extensions in two distinct directions. The first consists of enriching the logic with the ability to speak in a weak form about set cardinality, this is the ”cost-function” setting. The second direction is an extension of monadic logic by topological capabilities, yielding to ”Asymptotic Monadic Logic”.

The second aspect of this proposal is the study of the ”applicability” of this theory. It implies determining the extra-cost induced by the use of the more complex techniques that we are developing compared to the classical theory. It involves the study of variant weaker formalisms corresponding typically to temporal logics. And finally, it means developing the model-checking approach toward these quantitative notions.


Current members involved in the project are:

Other people closely related to the project