Sujet : Deciding properties of tree languages

Responsable : Igor Walukiewicz et Pascal Weil
Téléphone : 69 17
e-mail : voir la page web
Site Web : http://www.labri.fr/Perso/~igw/
Equipe : LAAA

Présentation du sujet :

Labeled trees arise in several contexts. They are models of
executions of programs: a tree represents all the possible executions
of a nondeterministic program. They are also models for organization
of data: Extended Markup Language (XML) is a standard for data exchange
on the web (see the surveys on Frank Neven's web-page).

In both contexts it is important to have logics to describe tree
properties. In the first case such logics are used to specify
programme properties; in the second they are used to formulate database
queries and for checking integrity of data.

Monadic second-order logic (MSOL) is the most standard formalism for
expressing properties of trees. It has many good properties but there
are also numerous reasons to look for stronger as well as for weaker
formalisms. On one hand one would like to express more properties, on
the other, one looks for languages for which verification is
computationally easier. There are at least two, quite broad, themes in
this subject:

1. Finding new decidable extensions of MSOL. These can be, for example,
in a form of adding possibility of counting or comparing the equality
of subtrees. Of course such types of extensions were studied already
in the literature but we are far from having the full picture.

2. Deciding if a given property can be written in a given logic. Some
logics weaker than MSOL are interesting because, for example, the
verification problem for them is easier. The question is then whether
a given property is expressible in a weaker logic. A related question is
that of the characterization of the expressive power of such sublogics
of MSOL as CTL or first-order logic (FOL). These are very
fundamental questions. The characterization for FOL properties of word
languages was given by Sch\"utzenberger in the sixties, but the for
trees such a characterization is still unknown. Recently results were
obtained from some small fragments of FOL.

Mot-clés : Word and tree languages, automata theory, XML

Références :
The references can be obtained from Igor Walukiewicz