Monday, June 18th

18:30- Cocktail at LaBRI

Tuesday, June 19th

Wednesday, June 20th


Achim Blumensath: The power of monadic second-order transductions

Abstract: Transductions - a notion playing a central role in the work of Bruno Courcelle - provide an indispensable tool when studying the monadic second-order theory of graphs. After presenting the basic properties of transductions, and describing several applications of them, the talk will focus on the question of the expressive power of transductions. That is, the question of which transformations of graphs can be realised by a transduction. In particular, we will be interested in methods to prove that there is no transduction from one graph to another one.

Thomas Colcombet: The forest factorisation theorem

Abstract: The factorisation forest theorem of Simon is a Ramsey-like statement for semigroups. It has gained a renewal of interest in the last year for its use in the context of automata theory and logic. This talk will be the occasion to describe some connections between some works of Courcelle and the theorem of factorisation forest.

Bruno Courcelle: Canonical graph decompositions

Abstract: Several graph decompositions are important for algorithmic purposes, for understanding the structure of objects (I am actually more interested on that latter aspect) and for proving wqo results. I will review the algorithmic and structural properties of several known canonical decompositions: Tutte decomposition in 3-connected components, modular decomposition, split decomposition, and define a new one for strongly connected graphs, closely linked to Tutte decomposition, that I call the "atomic decomposition" (1) The initial motivation is the study of Gauss words (representing self-intersecting curves in the plane). Knuth has defined in 1974 a similar but actually different (non-canonical) decomposition of strongly connected graphs.
(1) Why not? Some computer scientists work on "deforestation".

Irène Guessarian: Classes of interpretations revisited

Abstract: We will briefly survey early works by B. Courcelle on algebraic semantics and his seminal work on fundamental properties of infinite trees : we will try to show a few among the many extensions and developments initiated by the work of B. Courcelle. We will then introduce the notion of class of interpretations studied by B. Courcelle and I. Guessarian, present some papers based on this notion, some extensions and related works, and conclude with some further extensions which could be of interest.

Stephan Kreutzer: Lower Bounds for the Complexity of Monadic Second-Order Logic

Abstract: Courcelle's famous theorem states that any property of graphs definable in monadic second-order logic (MSO) can be decided in linear time on any class of graphs of bounded tree-width, or in other words, MSO is fixed-parameter tractable in linear time on any such class of graphs, where the parameter is the tree-width and the size of the formula. From a logical perspective, Courcelle's theorem establishes a sufficient condition, or an upper bound, for tractability of MSO-model checking. Whereas such upper bounds on the complexity of logics have received significant attention in the literature, much less is known about corresponding lower bounds. The topic of this talk is to present recent results obtained on lower bounds for MSO in relation to the tree-width of graphs. More specifically, under a suitable complexity assumption, we show that if C is any class of graphs which is closed under taking subgraphs, and additionally, the treewidth of C is not bounded polylogarithmically (in fact, log^c n for some small c suffices), then MSO-model checking is not fixed-parameter tractable on C in the sense above. To obtain this result we will also present recent progress on the complexity of computing brambles, a natural obstruction to small tree-width.

Janos Makowsky: Hankel Matrices, Connection Matrices and Definability in Monadic Second Order Logic (MSOL)

Abstract: To prove non-definability one usually uses game theoretic arguments which can get quite involved. We use matrix theoretic methods instead to prove non-definability in MSOL and its variations. This simplifies proofs of non-definability both conceptually and technically. In the talk we will illustrate the method in the case of graph properties, graph parameters and graph polynomials. The method has its origin in a paper by Carlyle and Paz from 1971, where they used Hankel matrices in formal language theory to characterize recognizability by stochastic automata. The method was used by Matz (1998) to prove non-definability of picture languages. Freedman, Lovasz and Schrijver (2007) introduced connection matrices to characterize graph parameters as partition functions. This was further generalized by Godlin, Kotek and the speaker (2008) and further developed since.

Maurice Nivat: Bruno Courcelle et 40 ans d'informatique plus ou moins théorique

Jacques Sakarovitch: Weighted automata: from behaviour equivalence to computation correspondence

Abstract: Decidability of equivalence of weighted automata is classically based upon linear algebra techniques. The same result is revisited with the notions of conjugacy and automata covering, leading to a combinatorial description of the equivalence, up to a 1-1 correspondence between computations of equivalent automata when the weights are taken in N. (joint work with Marie-Pierre Béal and Sylvain Lombardy.)

Wolfgang Thomas: Composition for orders with an extra binary relation

Abstract: The composition method is a powerful tool for the analysis of the MSO-theory of a structure (M,<,P) where (M,<) is a linear ordering and P a monadic predicate over M. In this talk we explain how (and in which cases) the method can be adapted to handle the first-order theory of a structure (M,<,R) where R is binary. We focus on relations R of finite valency (where for each m there are only finitely many m' with R(m,m') or R(m',m)). As a consequence of a composition theory for such structures, we can bound the recursion theoretic complexity of the first-order theory of (N,<,R) where (N,<) is the natural number ordering and R is of finite valency, and conclude that addition and multiplication are not definable if R is arithmetical. (The results are from the author's unpublished habilitation thesis of 1980 and presented here for the first time.)

Igor Walukiewicz: Transductions and beyond

Abstract: MSOL-transductions allow us to construct complicated models with decidable monadic-second order logic (MSOL) theory. A good example is the unfolding theorem: the MSOL theory of an unfolding of a graph can be algorithmically reduced to the MSOL theory of the graph. To see the power of this operation observe that the unfolding of a one vertex graph is an infinite sequence. Thus we obtain Buechi's result on the decidability of the MSOL theory of an infinite sequence. Iterating the unfolding operation followed by an MSOL interpretation, we get Caucal's hierarchy of graphs having a decidable MSOL theory. More recently Ong has shown that the MSOL theory of every tree of execution of a recursive scheme is decidable. This year it has been finally proved that the class of such trees is strictly bigger than the class of trees from Caucal's hierarchy. We will show that the theorem of Ong is an instance of a more general transduction operation resulting from the evaluation of lambda-terms.