18:30- Cocktail at LaBRI
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.
slides
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.
slides
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".
slides
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.
slides
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.
slides
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.
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.)
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.)
slides
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.
slides