Groupe de Travail
Graphes et Logique

le lundi de 14h à 15h dans l'amphi du LaBRI

Sur le web :
http://www.labri.fr/Perso/~janin/groupe









   


* 18 Octobre Sur la théorie monadique des poêles finies
  David Janin
  Résumé : (joint work with Anuj Dawar, Cambridge).
Les poêles finies sont les codages graphiques des mots infinis ultimement périodiques. On se propose ici d'étudier la logique monadique du second ordre sur les poêles en s'intéressant tout particulièrement aux formules qui ne distingue pas deux poêles codant le même mot (i.e. formule dites invariante par développement finis de poêles). On obtient alors la caractérisation suivante de ces formules de poêles.
Thm 1 :
pour tout langage omega-rationnel L : la classe des poêles codant les mots ultimement périodiques de L est définissable dans le fragment existentielle de la logique monadique.
Thm 2 :
pour toute formule de logique monadique phi invariante par développement de poêle, il existe un langage omega-rationnel L dont les mots ultimement périodiques sont exactement les mots codés par les poêles de phi.
 
Autrement dit, on obtiend ici une reformulation du théorème de Büchi applicable aux représentations finis des mots là ou le théorème de Büchi s'applique sur la théorie monadique de l'ordinal omega. Techniquement, ces résultats s'appuient largement sur la théorie classique des langages omega-rationels sans pour autant (semble tiil) en être des conséquences immédiates.





Responsable du groupe de travail : Olivier Ly
Bureau : 306
Mél: ly@labri.fr
Tél: +33 5 40 00 38 73

Maintenance de la page: Alexis Bouquet
Bureau 325
Mél : bouquet@labri.fr


Archives

1   Année 2004-2005

   


* 11 Octobre Matroïdes et Graphes
  Bruno Courcelle
  Résumé : Présentation des matroïdes, liens avec les graphes, "branch decompositions" des graphes et des matroïdes, résultats de S. Oum et résultats aboutissant à une preuve de la conjecture (affaiblie) de Seese.

2   Année 2003-2004

   


* 29 Septembre Complexité minimale de la vérification des formules du premier ordre et du second ordre monadique, d'après Frick et Grohe.
  Bruno Courcelle
  Résumé : Les problèmes que l'on peut exprimer en logique du premier ordre sont décidables sur les graphes en temps polynomial par rapport à la taille du graphe, mais avec des constantes hyperexponentielles par rapport aux formules. Il en est de même pour la logique du second-ordre monadique sur les graphes de largeur arborescente bornée. Il est montré en considérant seulement les mots et les arbres que à moins que P = NP, ces constantes exponentielles sont inévitables.


* 13 Octobre Complete and Minimal Programming Language for Graph Transformation
  Prof. Annegret Habel Université d'Oldenburg - Allemagne(en visite à Bordeaux le mois d'octobre)
  Résumé : We identify a set of programming constructs ensuring that a programming language based on graph transformation is computationally complete. These constructs are (1) nondeterministic application of a set of graph transformation rules, (2) sequential composition and (3) iteration. This language is minimal in that omitting either sequential composition or iteration results in a computationally incomplete language. By computational completeness we refer to the ability to compute every computable partial function on labelled graphs. Our completeness proof is based on graph transformation programs which encode arbitrary graphs as strings, simulate Turing machines on these strings, and decode the resulting strings back into graphs.


* Mardi 28 Octobre An attempt at the conjecture of Seese
  Achim Blumensath (Aachen)
  Résumé : Seese proved that all graphs with decidable GSO-theory have finite tree width by employing the Excluded Grid Theorem of Robertson and Seymour. To solve the corresponding conjecture about clique width and MSO-theories, I tried to derive an analogous excluded grid theorem for clique width. In this talk I will present methods and technical tools for transferring proofs concerning tree width into proofs for clique width. In particular, concepts analogous to separators and connectedness will be studied. The main emphasis of the talk will be on ideas and concepts, so it will consist mostly of pictures and definitions, some results, but no proofs.


* 3 Novembre Jeux distribués et contrôle distribué pour systèmes asynchrones
  Marc Zeitoun (Paris)
  Résumé : à venir...


* 11 Novembre CHALLENCES OF FINITE SETS OF WORDS
  Juhani Karhumaki (Turku, Finland)
  Résumé : One of the basic results on words is the characterization when two words commute. As a starting point we consider the same problem for finite languages. It turns out that this and related prob- lems are very different and complicated. An example is a problem proposed by J. Conway more than 30 years ago. He asked whehter the maximal set commuting with a given rational set is rational as well. The solution is known only in the very special cases. Indeed, it is not even known whehter such a set is always recursive!

We discuss the above problem and several related ones. We show some undecidability results which explain - I hope - why these problems are so difficult. We also propose several open problems, not only connected to the commutation, but also in terms of equations over finite sets of words.


* 30 Janvier Tree walking automata
  Mikolaj Bojanzick (Poland)
  Résumé :


* 02 Février Distributed Synthesis
  Julien Bernet
  Résumé :


* 09 Février Positional Determinacy of Games with Infinitely Many Priorities
  Igor Walukiewicz
  Résumé :

[ Joint work with Erich Gaedel ]

Quite a while ago Jonathan Swift reported on serious disagreements between the Big-Endians and the Little-Endians, two factions within the society of Lilliput, on a matter of fundamental importance: Big-Endians break their eggs at the larger end (``the primitive way"), while Little-Endians break it at the smaller end, and doing so support the view of the Emperor who had ``published an edict, commanding all his subjects, upon great penaltys, to break the smaller end of their eggs.'' The issue was very serious indeed because the Big-Endians ``so highly resented this law, that our historys tell us there have been six rebellions raised on that account; wherein one Emperor lost his life, and another his crown.'' [Part I, Chapter IV, Swift1726].

The fights between Big-Endians and Little-Endians continued and became even more vigorous when, with the advent of modern computing machines, new issues arose: should numbers be stored most or least significant byte first? Big-endians insist that the ``big end" is stored first because this is the way God intended integers to be represented, most important part first. Those in the big-endian camp include the Java VM virtual computer, the Java binary file format, the IBM 360 and and most mainframes. Little-Endians assert that putting the low-order part first is more natural because when you do arithmetic, you start at the least significant part and work toward the most significant part. In the little-endian camp are the Intel 8080, 8086, 80286, Pentium and follow ons and the MOS 6502.

A yet more serious battle between the two factions arose when the people of Lilliput abandonded their traditional games like chess, soccer, Russian roulette, etc. and started to play parity games. The little-endian rules for playing parity games assert, quite reasonably, that the smallest priority occurring infinitely often in a play determines the winner. The Big-Endians on the other side insist, strangely enough, that it is the largest priority seen infinitely often that decides who wins the game.

The goal of this work is to settle this issue once and for all and to prove that the Little-Endians are right. One method to do so would of course be to show the existence of an egg that can only be broken at the smaller end. However, it can be proved that the size of such an egg would necessarily have to be infinite; hence at least a constructive proof seems out of reach for present methodology. Instead we resolve this issue by way of parity games with infinitely many priorities. Whatever arguments there are between Little-Endians and Big-Endians, both factions agree that the right way to win parity games is via positional strategies or, if these are unavailable, finite-memory strategies, because the use of infinite memory ``is just not fair''. We prove here that any parity game with priorities in
w, defined in the little-endian style, can indeed be won be means of a positional winning strategy. The Big-Endians, however, miserably fail on their variant of parity games, as soon as they admit infinitely many priorities.


* 16 Février Vérification compositionnelle de programmes séquentiels
  Olivier Ly
  Résumé : We deal with the compositional verification of sequential programs.

This consists in deciding whether or not a given set of local structural properties of the functions of a program implies a given global behavioural property of the program.

Here we consider properties expressed in monadic second-order logic dealing with the control flow of the program and the function calls occuring during its execution. This problem has been investigated in relation with the security of open multi-application smart cards.

We prove that the compositionality is a decidable problem for sequential programs whose control-flow graphs are of tree-width less than a fixed integer value, which includes in particular structured programs.


* 23 Février "Axiomatising Tree-interpretable Structures"
  Achim Blumensath
  Résumé : Tree-interpretable structures -- also called prefix-recognisable or VR-equational -- are infinite structures that can be represented finitely in one of the following equivalent ways:

o an interpretation in the infinite binary tree

o a system of VR-equations

o a list of automata

In this talk I will show that every such structure can be finitely axiomatised in guarded second-order logic with cardinality quantifiers. The talk will be technical containing a detailed presentation of the proof.


* 1 Mars Sur la reconnaissabilité des ensembles de graphes
  Bruno Coucelle
  Résumé :

Once the set of finite graphs is equipped with an algebraic structure <?xml:namespace prefix = o ns ="urn:schemas-microsoft-com:office:office" /> (arising from the definition of operations that generalize the concatenation of words), one can define the notion of a recognizable set of graphs in terms of finite congruences.

Thus the class of recognizable sets depends on the signature of graph operations. We consider three signatures related respectively to Hyperedge Remplacement (HR) context-free graph grammars, to Vertex Replacement (VR) context-free graph grammars, and to modular decompositions of graphs. We compare the corresponding classes of recognizable sets.

In the lecture, we will sketch the proof that for graphs without large complete bipartite subgraphs, HR-recognizability and VR-recognizability coincide. The same combinatorial condition equates HR-context-free and VR-context-free sets of graphs.

If time permits we survey results showing that VR recognizability is a robust property in the sense that many variants of each signature yield the same notions of recognizability.

This lecture is based on an article by B. Courcelle and Pascal Weil That is accessible from :

http://www.labri.fr/Perso/ courcell/Textes/BC-PW.pdf


* 22 Mars Le problème de l'équivalence des DPDA t-turn
  Géraud Sénizergues
  Résumé : Nous introduisons une nouvelle propriété structurelle des langages préfixes: le "lemme des sous-mots". Il s' agit d'un nouvel outil permettant de construire des algorithmes décidant si des langages préfixes sont égaux ou non. En particulier, nous démontrons que le problème de l'équivalence des automates "finite-turn" est co-NP (en fonction du nombre de turns).


* 28 Mars Calculs locaux et algorithmique distribuée
  Yves Métivier
  Résumé : ?


* 19 Avril Keys, Nominals, and Concrete Domains
  Carlos Areces (INRIA Lorraine)
  Résumé : I will describe how description logics with concrete domains can be extended with "key constraints" that allow the expression of statements like "US citizens are uniquely identified by their social security number". Based on this idea, I'll introduce a number of natural description logics and discuss their decidability and computational complexity. It turns out that naive extensions with key constraints easily lead to undecidability, whereas more careful extensions yield NExpTime-complete DLs for a variety of useful concrete domains.

This was work in collaboration with Ian Horrocks, Carsten Lutz and Ulrike Sattler.


* 26 Avril Election, Nommage et Calculs Locaux.
  Jérémie Chalopin
  Résumé : Dans le cadre des calculs locaux, on s'intéresse au problème de l'élection qui consiste à distinguer un unique sommet du graphe en partant d'une configuration initiale quelconque, ainsi qu'au problème du nommage qui consiste à assigner une identité distincte à tous les sommets du graphe. Dans différents modèles de calculs locaux, on caractérise quels sont les graphes pour lesquels il existe un algorithme d'élection ou un algorithme de nommage. Ces résultats nous permettent en particulier de donner une hiérarchie stricte entre les différents modèles.

Pour donner ces caractérisations, on utilise différents types de morphismes de graphes. Pour donner des conditions nécessaires, on adapte le lemme de relèvement d'Angluin à chacun de ces morphismes. Les conditions suffisantes sont basées sur des adaptations de l'algorithme de Mazurkiewicz à chacun de ces modèles.


* 3 Mai Higher Order Pushdown Automata, the Caucal Hierarchy of Graphs and Parity Games
  Thierry Cachat
  Résumé : We consider two-player parity games played on transition graphs of higher order pushdown automata. They are ``game-equivalent'' to a kind of model-checking game played on graphs of the infinite hierarchy introduced recently by Caucal. Then in this hierarchy we show how to reduce a game to a graph of lower level. This leads to an effective solution and a construction of the winning strategies.


* 10 Mai ALGORITHMIC GAME SEMANTICS
  Andrzej Murawski
  Résumé : Game semantics has emerged as a powerful paradigm for giving semantics to a variety of programming languages ranging from purely functional languages to languages with non-functional features such as control and locally-scoped references. Recently it has been developing in a new algorithmic direction with a view to applications in computer-assisted verification.

After a brief review of results in game semantics, I will present an overview of the recent developments and - to give the flavour of the approach - I am going to demonstrate how the game semantics of second-order imperative programs can be captured by regular languages.


* 17 Mai A Pumping Lemma for Higher-Order Pushdown Automata
  Achim Blumensath
  Résumé : à venir


* 21 Juin Equivalence locale des graphes, "vertex-minors" et leur codage en logique du second-ordre monadique au moyen des "systèmes isotropes"
  Bruno Courcelle
  Résumé : La complémentation locale consiste à échanger arcs et non-arcs au voisinage d'un sommet. Deux graphes sont localement équivalents si on peut passer de l'un à l'autre par une suite de complémentations locales. La relation de "vertex-minor" combine complémentations locales et passage au sous-graphe induit. C'est un bel-ordre (résultat récent de S. Oum, élève de P.Seymour). On peut l'exprimer en logique MS, ce qui n'est pas évident d'après la définition, au moyen des systèmes isotropes ("isotropic systems") étudiés par A. Bouchet.

3   Année 2002-2003

   


* 7 octobre Réunion de rentrée
   
Résumé : Présentation des membres.


* 14 octobre On the FO-definability of tree languages
  Mikolaj Bojanczik (Warsaw)
Résumé :
First order definability (Joint work with Igor Walukiewicz)

The following problems are considered:
1."Is a given regular tree language first order definable?"
2."Is a given regular tree language chain logic definable?"

None of these problems are solved, although some conjectures and partial results are proposed.
Moreover a brief survey of results in this field, starting from the sixties, is presented.


* 21 octobre Decomposition de graphes
  Michel Bauderon
  Résumé : One of the biggest fight of Computer Science was against complexity,and the solution was in general found in simplicity, mainly that of the structures to be considered.
While discrete structures in general - let's say graphs - where difficult to grasp and manage, lots of efforts where done - with much success - on trees or tree-like structures.
It is well known indeed that many problems which in general are intractable, may become easy, let's say polynomial, provided that the underlying structure is tree-like (modular decomposition, bounded tree-width, ?) But there are other structures with strong regularity which seem to be reluctant to any pleasant treatment, among which grids.
This is why we started to study those kind of graphs, trying to find adequate decomposition in simpler item together with reconstruction mechanism suitable to facilitate the description of better algorithms. We have not gone that far yet, but have obtained new kinds of decomposition of such graphs based on structural properties of the graphs we consider.


* 28 octobre Jeux distribués
  Julien Bernet
  Résumé : (Travail réalisé en collaboration avec Swarup Mohalik)
Le problème de la synthèse d'un programme pour un processus interagissant avec un environnement, et devant respecter une spécification donnée, peut être réduit au problème consistant à trouver une stratégie gagnante dans un jeu infini à deux joueurs : un des joueurs joue le rôle du processus, et son adversaire joue le rôle de l'environnement.
On s'intéresse au problème de la synthèse dans un cadre distribué : plusieurs processus interagissent avec l'environnement, et leur comportement global doit respecter une spécification donnée. Je présenterai un modèle de jeux dans lesquels une équipe de processus joue contre un environnement : trouver une stratégie gagnante pour les processus dans un tel jeu revient à synthétiser un programme correct pour chaque processus.
Ce modèle permet d'exprimer le problème de la réalisation étudié dans l'article de A. Pnueli et R. Rosner : "Distributed reactive systems are hard to synthesize". Il est cependant trop expressif : nous verrons que le problème consistant à trouver une stratégie gagnante pour les processus est indécidable. Nous passerons en revue quelques classes de jeux dans lesquels ce problème devient décidable.

En conclusion, nous verrons que le problème de la décomposition, qui consiste à décider si une stratégie globale pour tous les processus peut être répartie en stratégie locales, une pour chaque processus, peut être résolu, avec une complexité en temps polynômiale dans la taille du jeu.


* 4 novembre Deciding program logics over push-down trees
  Igor Walukiewicz
  Résumé : A celebrated result of Rabin says that the monadic second order (MSO) theory of the full infinite binary tree is decidable. From there it follows that MSO theory of any regular tree is decidable. One can think of a regular tree as a tree that is an unraveling of a finite graph, or equivalently, as the unraveling of the state graph of a finite automaton.

A push-down tree is the unraveling of a graph of configurations of a pushdown automaton. Such a tree may have an infinite number of non-isomorphic subtrees, hence it may be not regular. Still MSO theory of any push-down tree is decidable. As the degree of such a tree is bounded we know that MSOL is equivalent to the mu-calculus over a pushdown tree.

In this talk we will show that the mu-calculus theory of a pushdown tree can be decided in EXPTIME. We will also provide a matching lower bound for a small fragment of the logic. We will then consider some fragments for which the problem becomes PSPACE-complete. Finally, we will mention extensions to automata with tree shaped stacks and stacks of stacks.


* 7 et 8 novembre AS automates, modèles distribués et temporisés
   
  Résumé : http://www.labri.fr/Perso/ weil/ASSTIC/78novembre.html


* 18 novembre Graphes de démonstration
  Christian Rétoré
  Résumé : Les démonstrations formelles de la logique linéaire peuvent être vues comme des graphes (aussi appelés réseaux de démonstration) qui admettent deux définitions: l'une, inductive, qui suit la construction de la démonstration dans les formalismes courants(déduction naturelle ou calcul des séquents), et l'autre, universelle, qui les caractérise comme l'ensemble des graphes sans certains cycles. Ces graphes sont un progrès pour la syntaxe logique parce qu'un seul et même graphe décrit plusieurs démonstrations qui ne diffèrent que par des permutations de règles; de plus on a affaire à des objets mathématiques raisonnablement structurés.

Nous montrerons qu'on peut aboutir, pour le fragment multiplicatif de la logique linéaire, à la définition suivante: une démonstration est un graphe muni d'un couplage parfait (décrivant les axiomes "a ou non a" ), et dont les autres arêtes forment un cographe (qui décrit la formule démontrée), tel que tout cycle élémentaire alternant les arêtes du couplage et celles du cographe contienne une corde. Cela permet d'interprêter la commutativité et l'associativité des connecteurs par l'égalité des graphes.

Ensuite on se posera la question d'étendre cette définition à la logique linéaire non-commutative.

Il est inutile de connaître la logique linéaire pour suivre cet exposé.


* 25 novembre Réaliseurs des graphes plans triconnexes et Demi-flips diagonaux.
  Nicolas Bonichon
  Résumé : Ce travail a été réalisé en collaboration avec Mohamed Mosbah.
Les réaliseurs ont été introduits par Walter Schnyder pour caractériser les graphes planaires. Plus tard une généralisation de ces objets a été introduite pour les graphes plans triconnexes.
Dans un premier temps, nous présenterons les réaliseurs des graphes plans maximaux ainsi que les opérations de flips diagonaux sur ces objets. Dans un deuxième temps, nous présenterons les réaliseurs des graphes plans triconnexes. Enfin, nous introduirons une généralisation des flips diagonaux aux réaliseurs des graphes plans triconnexes.


* 2 décembre Reconnaissabilité pour les langages de graphes et de posets
  Pascal Weil
  Résumé : L'articulation entre les notions de reconnaissabilité (algébrique) et de définissabilité (logique) est l'un des piliers de l'informatique théorique depuis ses origines, et c'est aussi l'un des outils privilégiés de ses applications. Cette articulation, acquise à l'origine pour les langages de mots et de mots infinis, a été explorée depuis dans un certain nombre d'autres domaines liés aux extensions de la théorie des langages pour la représentation de comportements distribués ou temporisés.

Le domaine sur lequel je me concentrerai est celui des langages de graphes, et parmi eux, les langages d'ensembles partiellement ordonnés -- vus comme des graphes acycliques transitifs. La notion de reconnaissabilité est intrinsèquement liée au choix d'une structure algébrique (celle du monoïde libre dans le cas des langages de mots) : je considèrerai en particulier l'ensemble des graphes finis étiquetés par un alphabet A comme une algèbre pour la signature modulaire ; il s'agit d'un ensemble d'opérations sur les graphes donné par la théorie de la décomposition modulaire des graphes.


* 9 décembre Level of knowledge of formulas in distributed systems
  Swarup Mohalik
  Résumé : The talk is an exposition of a paper by Parikh et al. where a concept called "level of knowledge" of formulas in a distributed system is explored.

These levels are correlated with certain regular, down-closed sets of strings over the knowledge modalities in the distributed system. It is shown that in certain systems, one can design protocols to attain all such levels but in systems without synchrony there are restrictions on the attainable knowledge levels.

Rohit Parikh and Paul Krasucki Levels of knowledge in distributed systems Sadhana, Vol. 17, Part 1, 1992, pp 167-191


* 16 décembre Extraction de connaissance
  Noël Novelli
  Résumé : La fouille de données (Data Mining) peut être définie comme un processus extraction d'information non triviale et intéressante à partir de gros volume de données. Après un peu de philosophie sur l'information non triviale et surtout intéressante, nous distinguerons les grandes familles de méthodes faisant partie des techniques de fouilles de données comme les règles d'associations, la classification supervisée et non supervisée (regroupement ou clustering) ou encore les arbres de décisions... ainsi que les cadres d'applications de ces travaux. Nous réduirons ensuite le cadre aux différents travaux de recherche sur l'extraction de Dépendances Fonctionnelles (implication sémantique entre attributs d'une base de données) à l'aide de techniques issues du Data Mining puis au pré-calcul de requêtes multidimensionnelles.


* 6 janvier Vers un algorithme plus performant pour 3SAT
  Mike Robson
  Résumé : Un nouvel algorithme de résolution de 3SAT est présenté utilisant de nouvelles idées et ayant un temps de calcul borné par O(1.526237n). Si ce temps reste supérieur à celui des meilleurs algorithmes connus (O(1.481n)), il n'est qu'une première étape dans l'exploitation de ces nouvelles méthodes et, sans doute, ce temps peut être réduit davantage.


* 13 janvier Simulation Relations for Parity Games
  Carsten Fritz (Université de kiel, Allemagne)
  Résumé : We will suggest definitions of delayed simulation relations [ESW01] for parity games.
The definitions will be game-based; they can be seen as extensions of the definitions of [FW02].
Our approach can easily be extended to, e.g., alternating parity automata.
We will then discuss the possibilities of using these relations for the simplification of parity games.
This is very much a work in progress -- the input and criticism of the audience is very welcome!

References: [ESW01] Etessami, Schuller, Wilke. Fair simulation relations, parity games, and state space reduction for Büchi automata. LNCS 2076. 2001. [FW02] Fritz, Wilke. State space reductions for alternating Büchi automata: Quotienting by simulation equivalences. LNCS 2556. 2002.


* 3 février Indexation de documents XML
  Sofian Maabout
  Résumé : XML est un modèle de représentation et d'échange de données. Un document XML peut être vu comme un arbre et son interrogation consiste essentiellement en l'extraction de sous arbres. Les langages de requêtes pour XML utilisent tous des expressions de chemin. Je parlerai de quelques méthodes d'indexation qui permettent d'évaluer efficacement ces expressions de chemin, donc les requêtes.


* 10 février Sur les classes ambiguës de la hiérarchie du mu-calcul.
  André Arnold
  Résumé :
On sait que dans le mu-calcul sur les arbres et dans le mu-calcul modal les index de Mostowski définissent une hiérarchie infinie dont les classes sont désignées par ½_n et ?_n.
On peut raffiner cette hiérarchie en considérant aussi les classes ambigües (½_n inter ?-n) et les classes compositionnelles (Comp (½_n,?_n)). La caractérisation de Rabin des ensembles qui sont à la fois Büchi et co-Büchi s'écrit alors : ½_2 inter ?_2 = Comp(½_1,?_1). Il est donc naturel de se demander si ce résultat se généralise aux autres niveaux de la hiérarchie.
Dans cet exposé, nous montrerons dans un premier temps que ce résultat ne se généralise pas, puis nous montrerons qu'il se généralise quand même.


* 17 février The mu calculus with explicit interpolants
  Giacomo Lenzi
  Résumé : We will present a variant of modal mu calculus, where operators for uniform interpolation are explicitly added to the syntax.
We will present an axiomatization for this logic.
This is a joint work with Giovanna D'Agostino of the University of Udine.


* 3 Mars Quelques aspects de la jeu-simulation
  Thierry Cachat
  Résumé : On donnera une définition de la "jeu-simulation", qui permet de déterminer le gagnant et la stratégie d'un jeu donné en le réduisant à un autre jeu que l'on sait déjà résoudre.
Cette technique, sans porter encore de nom, a été utilisée de différentes façons dans plusieurs travaux que nous présenterons.
On s'intéressera particulièrement aux jeux de parité sur les graphes des automates à pile et les graphes préfixes reconnaissables.

http://www-i7.informatik.rwth-aachen.de/ cachat/indexFR.html


* 17 Mars A game model for distributed synthesis
  Swarup Mohalik
  Résumé : In this talk, we present a game model which has the aspect of "distribution" in the model itself.
We give the motivation for such a model to overcome the problem of undecidability that arises in most situations of distributed sythesis.
This is corroborated by showing how some existing frameworks of distributed synthesis can be encoded in this game model.


* 24 Mars Expressiveness and Complexity of a Graph Logic
  Anuj Dawar (University of Cambridge)
  Résumé : Cardelli, Gardner and Ghelli defined a logic for specifying properties of graph-stuctured data.
This logic is based on a representation of graphs as terms, inspired by process algebra.
In this talk I will consider some preliminary questions about the expressive power and complexity
of their graph logic, in particular by comparing it with monadic second-order logic.

joint work with Philippa Gardner and Giorgio Ghelli


* 12 Mai Automates mixtes
  Gérard Huet
  Résumé : Les arbres lexicaux (tries) sont isomorphes aux automates finis déterministes acycliques, qui reconnaissent les langages finis. Leur partage en dag en produit la forme minimale. Des automates ou transducteurs d'états finis plus généraux peuvent être décrits par des arbres lexicaux annotés de décorations qui codent des transitions non déterministes, des cycles décrits par des adresses virtuelles, des écritures sur une bande de sortie, etc. En restant dans la problématique des types inductifs, ces structures de données pures peuvent être uniformément minimisées par un foncteur de partage, et donc donner lieu à des transducteurs minimaux. On aboutit ainsi à une représentation uniforme d'automates par des forêts d'arbres de recouvrement de graphes de transition comme squelettes déterministes préférentiels minimaux. Cette représentation a été appliquée systématiquement dans la boîte à outils Zen, utilisée par l'auteur pour la programmation d'opérations phonologiques et morphologiques en Pidgin ML.


* 19 Mai Temporal logic and regular languages
  Zoltan Esik
  Résumé : We associate a modal operator with each language belonging to a given class of regular languages and use the semidirect product of monoids with distinguished generators to characterize the expressive power of the resulting logic. We also discuss some generalizations of the method.


* 26 Mai An infinite hierarchy of graph families
  Didier Caucal
  Résumé : Starting from the finite graphs and using the unfolding followed by the inverse rational mapping, we present an infinite hierarchy of families of graphs having a decidable monadic theory. The first level of this hierarchy is the family of prefix-recognizable graphs, which are the graphs obtained by transitive closure of the pushdown transition graphs, and are also the graphs obtained by monadic second order interpretations from the binary tree. For each family of this hierarchy, we give closure properties and a tree generator. We show also that this hierarchy contains the transition graphs of the multi level stack automata, and the solutions


* 2 Juin Complétion aux modèles des théories logiques
  Luigi Santocanale
  Résumé : Let T be an algebraic theory corresponding to a propositional logic (e.g. the theory of Heyting algebras coming from intuitionistic logic, the theory of modal algebras S5, the theory of modal mu-algebras coming from the modal mu-calculus).

We shall see how notions like uniform interpolation and the deduction theorem translate into properties of the dual category of finitely presented algebras. These properties imply the existence of a modal completion of T.

We shall discuss how existence of model completions leads to design decision procedures for the join T1vT2 of two theories, given that we have available two procedures to decide T1 and T2.

Refs: Games sheaves and model completions by M. Zawadowski et S. Ghilardi.


* 16 Juin Jeux sur des graphes d'automates à pile : des conditions décidables de complexités Boréliennes finies arbitraires.
  Olivier Serre
  Résumé : Les graphes d'automates à pile (pushdown graphs) fournissent un modèle intéressant de systèmes infinis. L'étude des jeux à deux joueurs sur de tels graphes est alors naturelle pour des problèmes de vérification et pour ses liens avec le model checking du mu-calcul. En 1996, Igor Walukiewicz a donné une solution pour résoudre ces jeux dans le cas des conditions de parité. Par la suite, plusieurs voies ont été explorées : recherche de nouvelles constructions, approche uniforme du problème, nouvelles conditions de gain...

Dans cet exposé, on s'intéressera à la condition suivante, dite d'explosion stricte : Eve gagne ssi la taille de la pile converge vers +infty. Résoudre un jeu pushdown muni de cette condition est un problème Dexptime- complet.

Ensuite, à partir de cette condition, on montrera comment engendrer de nouvelles conditions de gain de complexités boréliennes finies arbitraires qui restent décidables.

Les techniques utilisées seront des réductions vers des jeux munis de conditions de gain plus simples. Par ailleurs, pour prouver les complexités Boréliennes de ces jeux, nous utiliserons des jeux de Wadge.

4   Année 2001-2002

   


* 1 octobre Model Checking Problem for Message Sequence Graphs and its extensions against MSO specifications
  Meenakshi B. (Chennai, Inde)
  Résumé : We study the model-checking problem for classes of message sequence charts (MSCs) defined by message sequence graphs (MSGs) and its extensions. The extensions studied subsume the class of regular MSC languages. We show that the model checking problem for MSGs and the extended class of MSGs against monadic second-order specifications is decidable. Moreover, we present two ways to model-check the extended classes --- one extends the proof for MSGs while the other extends the proof for regular MSC languages.


* 8 octobre Controller synthesis for timed specifications
  Deepak D'Souza (Chennai, Inde)
  Résumé : We study the problem of control synthesis for a timed plant and an *external* timed specification. We show that the problem is decidable when we are given a priori a maximum "granularity" for the controller, and when specifications comprise *undesired* w-regular timed behaviours. We also show that for deterministic specifications, the common granularity of the plant and specification suffices.


* 15 octobre An approach to the embedding problem for codes defined by binary relations
  Do Long Van (Hanoï, Vietnam)
  Résumé : We consider the possibility to embed a finite (regular) code in a given class C of codes in a code maximal in C (not necessarily maximal as a code) which remains finite (regular, resp.). This is called the embedding problem for the class C of codes. A general embedding scheme is proposed for the classes of codes defined by length-increasing transitive binary relations. As applications, possitive solutions for the embedding problem are obtained in a unified way for many classes of codes, well-known as well as new.


* 22 octobre Realizers : influence de la face externe et flips diagonaux
  Nicolas Bonichon
  Résumé : Les arbres de Schnyder ont été introduits par Walter Schnyder en 1989. Ces triplets arbres, ou realizers, sont à la base de nombreux algorithmes de dessins de graphe. Dans sa thèse, Enno Brehm a montré que l'ensemble des realizers d'un graphe muni d'opérations basées sur les recolorations de cycles avait une structure de treillis distributif. Nous présenterons deux résultats : -La taille du treillis des realizers d'un graphe ne dépend pas du choix de la face externe. -On peut transformer un realizer de taille n en tout autre realizer de taille n simplement à l'aide de flips diagonaux.


* 29 octobre Distributed Automata in an Assumption-Commitment framework
  Swarup Mohalik (Bangalore, Inde - Postdoc LaBRI)
  Résumé : Finite state distributed systems can be modelled as sets of finite state automata operating on local alphabets. But in order to exhibit non-trivial global behaviour they must have strong synchronizing capability.

We try to build this capability into the system of automata using assumptions and commitments. Each local automaton makes assumptions about the state of other automata in the system and offers some commitments itself. The allowed global moves are those where the resulting global state has matching assumptions and commitments.

We try to motivate the formulation through some examples and prove that all regular behaviour can be captured through systems of automata with assumption and commitments over given local alphabets. This provides a kind of decomposition result for finite state automata.


* 12 novembre Représentations partiellement complémentées de graphes orientés et extension aux graphes représentés à l'aide de formules de logique du premier ordre sans quantificateur
  Rémi Vanicat
  Résumé : Une opération de complément d'un noeud d'un graphe orienté change tous arcs sortants en non-arc et inversement. On définit ainsi une relation d'équivalence entre deux graphes si l'un peux être obtenue à partir de l'autre avec une séquence de tels opérations. Dahlaus Gustedt et McConnell ont montré que si G et G' sont deux graphes équivalents, on peux résoudre certain algorithme classique sur G' en utilisant la représentation par liste d'adjacence sur G avec une complexité O(n+m(G)). On utilisera leur résultat pour exécuter des algorithmes sur des graphes représenté a l'aide de la logique du première ordre sans quantificateur.


* 26 novembre Omega-semigroupes et langages de mots infinis
  Jean-Eric Pin (LIAFA)


* 11 mars Finite codes over free binoids
  K. Hashiguchi (Okayama, Japon)
  Résumé : A free binoid B generated by a finite alphabet A is a free algebra which is the closure of A under two independent bunary associative operations C and D. The free binoid B also has the same identity I to both operations C and D. Any element of B is uniquely denoted by a sequence of symbols from the extended alphabet which is the union of A and the set whose elements are C,D,( and ). In this talk, we introduce the notion of finie codes over B, and show that the following problem is decidable ; given a finite subset X of B and an operator O (one of C and D), decide whether (X,O) constitutes a finite code.


* 18 mars Une caractérisation des familles de réseaux admettant un algorithme d'élection
  E. Godard
  Résumé : L'élection consiste à parvenir à distinguer, par calculs distribués, un noeud de tous les autres. Pour un réseau donné, l'existence d'un algorithme d'élection est conditionnée classiquement par l'absence de symétries internes dans le réseau. Cependant, pour élire dans un réseau sans symétrie, on doit utiliser certaines informations relatives à celui-ci (sa taille par exemple) : il n'existe pas d'algorithme universel d'élection pour la famille des graphes sans symétrie.

Cet exposé présentera une condition nécessaire et suffisante pour qu'une sous-famille des graphes sans symétrie admette un algorithme universel d'élection. Cette condition s'exprime en termes de quasi-revêtements ( morphisme partiel de graphes qui conserve les propriétés locales ). On utilisera également des extensions d'un algorithme d'énumération d'A. Mazurkievicz et d'un algorithme de détection des propriétés stables de Shy, Szymanski et Prywes.


* 8 avril Le projet VISIDIA
  M. Mosbah


* 15 avril Sur le probleme des variables dans le mu calcul.
  G. Lenzi


* 6 mai Graphes de Cayley planaires : un problème d'étiquetage
  D. Renault
  Résumé : Etant donné un groupe G finiment présenté et A un ensemble de générateurs, le graphe de Cayley de G associé à A est défini de la manière suivante : les sommets du graphe sont les éléments de G, les étiquettes des arêtes sont les éléments de A, et il existe une arête étiquetée par x reliant un sommet g1 à un sommet g2 si et seulement si g1 * x = g2 dans G.

Dans le cas général, il n'est pas évident de pouvoir décider si un graphe donné est un graphe de Cayley de groupe ou non. T. Chaboud a apporté une réponse élégante dans le cas de certains graphes planaires sommet-transitif. Cet exposé présentera la méthode qu'il a utilisée, ainsi que certaines extensions que l'on peut apporter pour une classe de graphes plus générale.

Mots-clé : graphes de Cayley, graphes sommet-transitif, graphes planaires, pavages, plan hyperbolique, étiquetage


* 21 mai Regular Languages Definable by Lindstrom Quantifiers
  Zoltan Esik (Université de Szeged, Hongrie)
  Résumé : By the classic result of Buchi, Elgot and Trakhtenbrot, the regular languages are exactly those definable by the sentences of a certain monadic second-order logic over words. Moreover, Mc Naughton and Papert proved that the first-order sentences of this logic define an important subclass of the regular languages, the star-free languages. By Schutzenberger's theorem, the star-free languages are exactly those that can be recognized by the aperiodics, i.e., by those finite monoids containing no nontrivial groups.

Because of the limited expressive power of first-order logic on words, and in the search for characterizations of other important subclasses of regular languages in terms of formal logic, Straubing, Therien and Thomas introduced modular quantifiers and showed that a language is definable in the logic involving, in addition to first-order quantifiers, the modular quantifiers iff its syntactic monoid is finite and solvable, i.e., it contains only solvable groups. And if no first-order quantifiers are allowed, then a language is definable iff its syntactic monoid is a finite solvable group.

The modular quantifiers, and the quantifiers associated by Barrington, Immerman and Straubing with finite monoids and groups, are all special cases of (simple) Lindstrom quantifiers corresponding to regular languages. In our main result, we give an algebraic characterization of the expressive power of Lindstrom quantifiers associated with any given subclass of the regular languages subject to natural condition. This allows us to characterize those classes of Lindsrom quantifiers that have the same expressive power as monadic second-order logic.

The results were obtained in collaboration with Kim G. Larsen during a visit at BRICS and the Department of Computer Science of Aalborg University.


* 10 juin Two-way alternating automata and finite models
  Mikolaj Bojanczyk (Warsaw University)
  Résumé : Two-way alternating tree automata on infinite trees were studied by Vardi in [2], who used them to decide the satisfiability problem for the modal mu-calculus with backward modalities. Another application came in [1], where the satisfiability problem for fixed point Guarded Logic was reduced to the the same problem for two-way automata. In this talk I shall consider the following problem for a graph version of the automata: "Given a two-way alternating automaton, decide wheter it accepts some finite graph."

An exponential algorithm is presented, which reduces the finite satisfiability of an automaton to the nonemptiness of a certain tree language. An upper bound comes from the fact that the EXPTIME complete satisfiability problem for one-way automata is a special case of the finite graph problem. Thus the finite graph problem is proved EXPTIME complete.

Finally I will discuss how the finite model problems for the mu-calculus with backward modalities and the fixpoint Guarded Logic can be solved using this result.

[1] E. Graedel, I. Walukiewicz, "Guarded fixed point logic", LICS 1999

[2] M. Vardi, "Reasoning about the past with two-way automata", 1998, LNCS vol 1443


* 21 juin - 14h The Powerdomain of Indexed Valuations
  Daniele Varacca (BRICS, Aarhus University and Cambridge University)
  Résumé : This talk is about combining nondeterminism and probability in denotational semantics. We argue that the usual powerdomain of valuations does not combine well with the nondeterministic powerdomain. We define the notion of indexed valuations which can be combined nicely with nondeterministic powerdomain. We give a computational intuition for this construction. The work will appear in the proceeding of LICS 2002.


* 21 juin - 15h Dynamic Planar Convex Hull (joint work with Gerth Brodal)
  Riko Jacob (BRICS, University of Aarhus)
  Résumé : We determine the computational complexity of the dynamic convex hull problem in the planar case. We present a data structure that maintains a finite set of points in the plane under insertion and deletion of points in amortized O(log n) time. Here n denotes the number of points in the set. The data structure supports the reporting of the extreme point of the set in some direction in worst-case and amortized O(log n) time. The space usage of the data structure is O(n). We give a lower bound on the amortized asymptotic time complexity that matches the performance of this data structure.


* 1 juillet Spécifications partielles de dessin de graphe : Etude logique et combinatoire
  Soutenance de thèse : Valère Dussaux
  Résumé : Les travaux présentés dans cette thèse concernent les spécifications de dessin de graphe. On introduit la notion de carte partielle dont deux cas extrêmes sont le graphe (sans indication de dessin) et la carte (combinatoire) qui spécifie complètement le dessin (à déformation près) d'un graphe connexe. Des problèmes de réalisabilité de dessin sans croisement d'arêtes, sur le plan, sur des surfaces plus complexes, sont étudiés des points de vue logique et combinatoire au moyen de la structure de carte partielle. Dans la formulation de ceux-ci intervient le problème de l'ordonnancement cyclique. On obtient des caractérisations par configurations exclues de relations cycliquement consistantes, de certaines classes de cartes partielles et des cartes dessinables sur une surface donnée. Ces caractérisations sont exprimables dans la logique du second ordre


* 8 juillet Mu-calcul algébrique: équations et congruences
  Luigi SantoCanale

5   Année 2000-2001

   


* 11 septembre An automaton model for user-controlled navigation of the web
  K. Lodaya (The Institute of Mathematical Sciences, Chennai)
  Résumé : We present a simple theoretical model of web navigation, in which each WWW user creates style specifications which constrain web browsing, search and navigation using the user's own judgement of the quality of visited sites. A finite state automaton is associated with each specification, which is presented in a two-level modal logic making up the acceptance condition for the automaton. We show that many interesting queries regarding the user's web search can be answered using standard automata theory.

This is joint work with my colleague R. Ramanujam, and was presented at the Conference on Implementation and Application of Automata (CIAA '00), London, Canada, in July this year.


* 2 Octobre Introduction aux Messages séquences Charts (titre provisoire)
  Pascal Weil


* 5 Octobre (Jeudi 16h -17h30) Méthodes logiques en algorithmique
  Janos Makowski (Haifa)
  Résumé : Définissabilité logique et calculabilité sur les objets finis:
Structures finies, langages logiques du premier et du second ordre; Jeux de Ehrenfeucht et Fraïssé: résultats de non-définissabilité; Définissabilité des langages rationnels; Classe NP et théorème de Fagin.


* 9 Octobre (Lundi 14h - 15h30) Méthodes logiques en algorithmique
  Janos Makowski (Haifa)
  Résumé : Polynômes sur les graphes et leur complexité:
Complexité du calcul du permanent d'une matrice et classe #P; Largeur arborescente, Evaluation efficace du permanent; Applications aux noeuds; Polynômes de Tutte et de Kauffman.


* 12 Octobre (Jeudi 16h-17h30) Méthodes logiques en algorithmique
  Janos Makowski (Haifa)
  Résumé : Décomposition des graphes et des structures, et inductivité de la vérification:
Théorèmes de Fefermann, Vaught et Shelah pour les logiques du premier ordre et du second-ordre monadique; Applications aux structures relationnelles de largeur arborescente bornée; Généralisations et problèmes.


* 23 Octobre Décomposition arborescentes locales - d'aprés M. Grohe
  Bruno Courcelle


* 13 Novembre "Tilling system et hierarchie monadique" d'aprés Matz et Thomas
  David Janin


* 20 Novembre Evaluation exhaustive des requetes en logique monadique du second ordre monadique, d'après Grohe et Flum
  Bruno Courcelle


* 27 Novembre Jeux d'Ehrenfeucht-Fraissé et hierarchie d'alternance de quantificateurs de la logique monadique faible du second-ordre
  Olivier Ly


* 4 Decembre Arbres de Schnyder d'un graphe planaire maximal. Opérations, propriétés et dessins
  Nicolas Bonichon


* 18 Decembre "Tilling system et hierarchie monadique" (suite et fin)
  David Janin


* 8 janvier Décompositions arborescentes de formules du premier ordre d'après M. Grohe
  Bruno Courcelle


* 22 janvier Résolution des jeux de parité par améliorations successives de stratégies
  Aymeric Vincent
  Résumé : Dans un article présenté à CAV'2000, Vöge et Jurdzinski proposent un algorithme permettant de trouver l'ensemble des positions gagnantes pour un joueur dans un jeu de parité en améliorant par étapes une stratégie choisie au départ arbitrairement.

La méthode utilisée fait intervenir des étiquetages de positions sur lesquels existe une relation d'ordre qui permet d'assurer la terminaison de l'algorithme.

Le but de cet exposé est de présenter intuitivement les idées sous-jacentes au papier, afin de pouvoir le lire plus facilement.

L'intérêt pour cet article est motivé par le fait que le problème est dans UP inter co-UP, et que la complexité d'une étape de l'algorithme est polynomiale. La question (ouverte) est donc de savoir si le nombre d'étapes nécessaires pour aboutir à la solution est polynomial ou non.


* 29 janvier Une approche algébrique pour le calcul efficace des positions gagnantes dans les jeux de parité.
  David Janin
  Résumé : Les jeux de parité se trouvent au coeur de la théorie des automates d'arbres infinis et du mu-calcul propositionnel. Cet exposé se propose d'étudier le problème fondamentale encore ouvert sur les jeux de parité : la complexité du calcul des positions gagnantes.

En définissant une relation d'ordre appropriée sur les positions dans les jeux de parité, je montrerais qu'il existe un jeu de parité canonique, dont toutes les positions sont gagnantes, dans lequel se plonge (via l'ordre ci-dessus) toutes les positions gagnantes de tous les jeux de parités.

La relation d'ordre préservant les positions gagnantes et le graphe canonique étant de taille n^d (pour tous jeux à n positions et 2d indices de parité), ce résultat induit un algorithme de calcul des positions gagnantes au moins aussi bon, en termes de complexité, que tous les algorithmes (dont la complexité a été analysé) connus à ce jour.

L'algorithme présenté est-il polynomial de degré borné ? cette question est (actuellement) ouverte.

Par ailleurs, cette approche nouvelle pourrait aussi offrir des critères de décision pour des problèmes classiques du mu-calcul ou de la logique monadique du second ordre sur les arbres (et les graphes modulo dépliage).


* 5 février Logique et Compression
  Michel de Rougemont


* 12 février Dépliages partiels, arbres hyperalgébriques et logique du second-ordre monadique, Travail en cours avec T. Knapik (La Réunion).
  Bruno Courcelle


* 5 mars Dépliages partiels, arbres hyperalgébriques et logique du second-ordre monadique, Travail en cours avec T. Knapik (La Réunion) - La suite.
  Bruno Courcelle


* 12 mars Prédicats morphiques et extensions - Travail en collaboration avec W. Thomas
  Olivier Carton
  Résumé : Nous considérons la structure (N,<,P) des entiers naturels munis de l'ordre, étendue par un prédicat unaire P. Nous montrons que pour un prédicat morphique P, la théorie monadique du second ordre associée MTh(N,<,P) est décidable. Ce résultat étend les résultats précédents de Elgot et Rabin (1966) et Maes (1999). La solution est obtenue par des méthodes de théorie des semigroupes, qui sont reliées à l'approche par automates de Elgot et Rabin. Finalement, nous montrons comment ces méthodes permettent d'obtenir une large classe de prédicats P pour lesquels la théorie MTh(N,<,P) est décidable.


* 19 mars Reconnaissance de graphes par calculs locaux
  Emmanuel Godard
  Résumé : Les calculs locaux sont utilisés pour décrire les algorithmes distribués et consistent en des systèmes de réécriture de graphes. Dans le cadre de l'étude de la puissance et des limitations de ces calculs locaux, on s'intéresse au problème de la reconnaissance qui consiste, pour un réseau, à calculer certaines propriétés topologiques du graphe sous-jacent (être un arbre, planarité, ...). On présentera une caractérisation complète des propriétés reconnaissables par calculs locaux en fonction du degré de connaissance que peut avoir a priori le réseau sur lui-même (nombre de sommets, ...). Cette caractérisation est basée sur l'utilisation de revêtements (morphismes de graphes préservant les propriétés locales) et d'un algorithme d'énumération de sommets proposé par A. Mazurkievicz.


* 26 mars Modularité de l'appel par nécessité pour les systèmes de réécriture de termes orthogonaux.
  Irène Durand
  Résumé : On se place dans le cadre des systèmes de réécritures de termes orthogonaux. Précedemment a été définie une hiérarchie de classes de systèmes de réécriture de termes orthogonaux telle que pour chaque classe:

1- on a une stratégie de réécriture séquentielle optimale et calculable (valable pour tous les systèmes de la classe)
2- on peut décider si un système appartient à la classe

La complexité de décider si un système appartient à une de ces classes étant élevée (exponentielle en bas de la hiérarchie, doublement exponentielle en haut), il est intéressant d´étudier la modularité de l'appartenance à ces classes: "si deux systèmes R1 et R2 appartiennent à la classe C, leur union appartient-t'elle aussi à C?". On montre que ce n'est pas toujours le cas et on donne des conditions suffisantes pour que ce soit le cas.


* 23 avril Graphes infinis et Logique monadique du second ordre
  Téodore Knapik (La Réunion)

6   Année 1999-2000

Groupe de travail géré par par D. Janin

   


* 4 octobre D. Janin
  Sur la complexité monadique du mu-calcul


* 18 octobre P. Weil
  Automates et rationalité pour les langages série-paralléle et d'autres structures
  Résumé : [résultats obtenus conjointement avec Kamal Lodaya (I. M. Sc., Chennai)]

Dans un travail antérieur, nous avions abordé l'étude des langages de pomsets série-parallèle à l'aide de la notion classique de reconnaissabilité, et en introduisant un modèle d'automates adapté à la manipulation de ces pomsets. Il s'était avéré que la classe des langages acceptés par des automates et celle des langages reconnaissables coïncident sous l'hypothèse de largeur bornée, mais que cela n'est pas le cas en général.

Les résultats qui seront présentés au groupe de travail se situent dans la continuité de ceux qui viennent d'être rappelés. Pour élucider le lien entre reconnaissabilité et automates, nous passons des pomsets série-parallèle aux ``
sS-langages'', c'est-à-dire que nous nous plaçons dans une structure algébrique où coexistent un produit binaire associatif, dit produit séquentiel, et d'autres opérations, dans une signature S fixée, qui ne sont soumises à aucun axiome.

Les automates introduits pour les langages série-parallèle sont étendus à ce cadre plus général et plus libre, et on y démontre l'équivalence entre reconnaissabilité et acceptation par un automate. Une caractérisation par expressions rationnelles peut également être donnée.

L'application de ces résultats aux langages série-parallèle montre d'une part que tout langage série-parallèle reconnaissable est accepté par un automate, et d'autre part que les langages série-parallèle acceptés par des automates sont caractérisés par certaines expressions rationnelles. La question de la clôture par complément des langages série-parallèle acceptés par automate reste ouverte.


* 25 octobre O. Ly
  Problème des bouts pour les graphes automatiques et générations de graphes par substitution
  Résumé : On montre que le nombre de bouts d'un graphe automatique n'est pas calculable. La preuve utilise les notions de machine auto-stabilisante et de graphes des configuration d'une machine de Turing. On établit par ailleurs un lien entre les graphes automatiques et les systèmes de substitution de graphes finis. De façon plus précise, la suite des sphères d'un graphe automatique est générée en itérant une substitution de graphe. On en déduit que le probléme de la connexité des graphes produits en itérant une substitution est indécidable. Nous verrons aussi que le type de substitution considéré ici permet l'émulation des systémes de remplacement d'hyperarcs pour lesquels le problème de la connexité est décidable.


* 8 novembre M. Ykhlef
  Soutenance de thèse


* 29 novembre G. Lenzi
  Une characterization au second ordre des automates de Buchi
  Résumé : Nous considérons la logique monadique du second ordre avec deux fonctions de successeurs, interprétée sur l'arbre binaire. Nous montrons que une propriété est définissable dans le fragment S2 de cette logique si et seulement si elle est définissable par un automate de Büchi. En plus nous montrons que toute propriété définissable dans S2 avec égalité est définissable dans S2 sans égalité aussi.


* 13 decembre B. Courcelle et R. Vanicat
  Representations efficaces de graphes pour l'adjacence et la distance


* 10 janvier V. Dussaux
  Autour des spécifications partielles de dessins plannaires


* 17 janvier B. Courcelle et J. Makowsi
  Operations sur les hypergraphes compatibles avec la logique monadique du 2nd ordre: complementations et fusions de sommets


* 21 février M. Jurdzinski - Varsovie/Aarhus(BRICS)
  On the model-checking problem


* 28 février N. Bonichon
  Algorithme de dessin de graphe planaire en couches


* 6 mars D. janin
  Vers une théorie algébrique des langages d'arbres infinis


* 14 mars Décomposition orthogonale de graphes
  F. Carrere


* 27 mars Logique temporelle avec compteurs et automates
  Hubert COMON (LSV, Cachan)


* 17 avril E. Gioan
  Correspondance entre les orientations et les arbres maximaux d'un graphe : generalisation aux regions et simplexes d'un arrangement d'hyperplans, et aux matroides orientes.
  Résumé : Il s'agit en general d'une correspondance canonique entre les reorientations et les bases d'un matroide oriente, compatible avec les activites. Dans le cas d'un arrangement d'hyperplans (ensemble d'hyperplans d'un espace vectoriel reel), elle se traduit geometriquement par une correspondance entre les regions et les simplexes (par exemple pour un ensemble de droites du plan affine, c'est une correspondance entre les regions et les triangles de la configuration). Plus particulierement dans le cas d'un graphe, on obtient une correspondance entre les orientations et les arbres maximaux. Les activites sont un modele d'etat du polynome de Tutte (ce polynome fondamental a deux variables generalise le polynome chromatique et le polynome des flots de la theorie des graphes, et est lie aussi a l'enumeration des cellules d'un arrangement d'hyperplans).


* 29 mai About graphical control structures for graph grammars
  S. Gruner (Berlin)


* 30 mai (Mardi) Independence: logics and concurrency
  J. Bradfield (Edimburg)
  Résumé : The idea of Henkin's branching quantifiers, in which quantified variables depend on only some of the previous variables, has in recent years been taken up again in logic by Hintikka and Sandu. I will introduce this logic, and then suggest that there is a natural associated modal logic that gives some account of independence in concurrency, but without invoking true concurrent models. I will give examples, define some associated fixpoint logics, and consider some problems of more general fixpoint extensions.


* 5 juin From Atjai-Fagin game to Erenfeucht-Fraissé games and back
  J. Marcinkowski (Wroclav)


* 19 juin Largeur de clique des graphes dénombrables: un résultat de compacité
  B. Courcelle

7   Année 1998-99

Groupe de travail géré par par D. Janin

   


* 21 Septembre A. Arnold
  La hiérarchie du mu-calcul sur les arbres binaires est infine


* 28 Septembre A. Middeldorp (Tsukuba, Japon)
  A deterministic Lazy Naroowing Calculus
  Résumé : In this talk we summarize recent joint work with Satoshi Okui on the completeness of the lazy narrowing calculus LNC. LNC consists of five simple inference rules that simulate the complicated narrowing operation. Contrary to what has been stated in the literature, we show that LNC lacks strong completeness, so selection functions to cut down the search space are not applicable. We establish an interesting connection between strong completeness of LNC and completeness of basic narrowing. We also address the eager variable elimination problem. It is known that many redundant derivations can be avoided if the variable elimination rule, one of the inference rules of LNC, is given precedence over the other inference rules. We prove the completeness of a restricted variant of eager variable elimination in the case of left-linear confluent rewrite systems. We show that for left-linear confluent constructor systems all non-determinism between the inference rules of LNC can be removed without losing completeness, provided we interpret equality as strict equality. For the subclass of orthogonal constructor systems the resulting calculus LNC_d is shown to have the nice property that solutions computed by different derivations starting from the same goal are incomparable.

If time permits we conclude with an overview of very recent completeness results for LCNC, the extension of LNC for conditional rewrite systems, which were obtained jointly with Mohamed Hamada and Taro Suzuki.

In this talk no specific knowledge of rewriting or narrowing is assumed.


* 5 Octobre Présentation des activités du groupe de travail
   


* 12 Octobre P. Weil
  Langages d'ensembles partiellement ordonnes serie-parallele


* 19 Octobre Ph. Narbel
  Les substitutions itérées et les automorphismes de surface
  Résumé : Il s'agira de montrer comment les substitutions itérées -- étudiées entre autres sous le nom de D0L-systèmes -- peuvent se représenter géométriquement, puis comment il est alors possible d'obtenir des résultats constructifs et algorithmiques liés à la classification classique (dite de Nielsen-Thurston) des automorphismes des surfaces, i.e. des transformations bi-continues bijectives des surfaces sur elles-mêmes.


* 26 Octobre B. Lesaec
  Représentation de graphes planaires en couches


* 2 Novembre C. Paul
  Algorithmes de décomposition modulaire


* 9 Novembre J.M. Le Bars (Caen, meilleur papier étudiant LICS'98)
  Lois 0-1 en logique


* 30 Novembre B. Courcelle
  Graphes uniformement creux et élimination des quantifications sur les ensembles d'arcs


* 7 Décembre B. Courcelle
  Graphes bipartis convexes


* 14 Décembre I. Walukiewicz
  On the guarded fragment of first order logic and its extension with fixpoints
  Résumé : Guarded fragment (GF), introduced by Andreka, van Benthem and Nemeti, is a fragment of first order logic that "behaves like modal logic". The fragment is defined by syntactically restricting the use of quantifiers. Nevertheless GF contains more than just formulas resulting from the translation of modal formulas. For example, in GF there is no restriction on the arity of relations in GF.

Andreka, van Benthem and Nemeti has shown that satisfiability problem for GF is decidable and that GF has some desirable properties like small model theorem, interpolation theorem and characterisation of the expressive power in terms of modified Ehrenfeucht-Fraisse games. Graedel has shown that satisfiability of formulas in GF (and its extension LGF) is complete for 2EXPTIME and it is complete for EXPTIME if the signature is fixed.

We consider the extension of LGF with fixpoint operators (of arbitrary arity). It turns that the satisfiability problem for this logic is still in 2EXPTIME and it is in EXPTIME if the signature is fixed. This way we have an extension of the mu-calculus with bigger expressive power but with the same complexity of the decision procedure.


* 11 Janvier H. Jacquet
  Une approche catégorique de la réécriture de sommets dans les graphes


* 18 Janvier G. Sénizergues
  T(A)=T(B) : le probleme de l'equivalence des transducteurs a pile deterministes de X* dans un groupe lineaire


* 25 Janvier E. Sopena
  Homomorphismes et Colorations de Graphes Orientés
  Résumé : Un homomorphisme d'un graphe G vers un graphe G' est une application f:V(G)¾® V(G') qui préserve les arêtes : xyÎ E(G) f(x)f(y)Î E(G'). On observe alors facilement qu'un graphe G est k-coloriable si et seulement s'il admet un homomorphisme vers le graphe complet à k sommets. Si l'on considère maintenant les graphes orientés antisymétriques, la notion d'homomorphisme induit de la même façon la notion de coloration de graphe orienté : une k-coloration d'un graphe orienté H est une application c:V(H)¾®{1,2,...,k} telle que
(i) xyÎ E(H) c(x)¹ c(y) et
(ii) xy,ztÎ E(H), c(x)=c(t) c(y)¹ c(z).
Nous allons présenter les principaux résultats obtenus jusqu'ici sur les homomorphismes et colorations de graphes orientés. Nous présenterons également quelques questions ouvertes.


* 8 Février I. Klimann (LIAFA, Paris VII)
  De nouvelles structures pour resoudre des problemes d'(A,B)-invariance
  Résumé : On cherche a trouver le sup de l'ensemble {X| AX £ X+B et X£ K} dans divers cadres (langages, series), ou A, B et K sont des parametres fixes ayant une certaine regularite. Pour cela, on introduit de nouveaux outils melant automates (pour les langages) ou representations lineaires (pour les series) a des formules booleennes.


* 15 Février M. Robson
  Un Majorant du seuil de 3-coloriabilité


* 8 mars V. Dussaux
  Problemes lies aux cartes partielles et caracterisation des cartes toriques


* 15 mars A. Raspaud
  Coloration des graphes mixtes


* 22 mars E. Godard
  Classes de graphes reconnaissable par calculs locaux


* 29 mars N. Bidoit
  Hierarchie de langages de requetes temporelles lineaires


* 31 mai G. Lenzi
  Sur la structure de la logique monadique du second ordre sur l'arbre binaire


* 7 juin B. Lesaec
  Reconnaissance forte pour les langages rationnels

8   Année 1997-98

Groupe de travail géré par par D. Janin

   


* 13 Octobre Bertrand Lesaec
  Géneration de Tests


* 20 Octobre David Janin
  Problèmes ouverts I


* 27 Octobre André Raspaud (1/2h) -- Bruno Courcelle (1/2h)
  Problèmes ouverts II


* 3 Novembre Nicole Bidoit
  Extension des langages temporels aux bases de données non structurées


* 10 Novembre Yves Métivier
  Coverings and the power of local computations in graphs knowing the size or the topology


* 17 Novembre Géraud Senizergues
  G(A) ~ G(B) ?


* 24 Novembre Mourad Ykhlef
  Langages de requètes pour bases de données semi-structurées


* 5 janvier Mike Robson
  Une conjecture sur les arbres binaires de recherche


* 19 janvier Olivier Ly
  Le problème de l'homéomorphisme de surfaces équationnelles sans bord est décidable


* 26 janvier Denis Lugiez (LIM - Marseille)
  Quelques sortes d'automates d'arbres a contraintes et leur utilisation en Preuve automatique
  Résumé : Les outils automatiques de preuves permettent de realiser des preuves par induction en utilisant des techniques a base de reecriture. Dans ce cadre les fonctions sont definies par des regles de reecriture. Pour assurer de bonnes proprietes a la procedure de preuve, il faut pouvoir decider que ces definitions sont completes et savoir construire des ensembles-tests. On montre dans cet expose comment l'utilisation de nouvelles classes d'automates d'arbres a contraintes permet de resoudre ces questions dans de nombreux cas utiles, notamment lorsque des constructeurs associatifs-commutatifs sont utilises. Nous montrerons que la classe d'automate utilisee possede de bonnes proprietes en combinant des techniques arithmetiques et des techniques de pompage. Nous terminerons en discutant les possibilites d'extension de la classe d'automates consideree.


* 26 janvier Nicolas Magnier
  Validation des transactions dans les bases de données : Classes décidables et vérification automatique


* 2 février Pierre-André Wacrenier
   


* 9 février Khanh Hoang (Paris I)
  Une approche basée sur le non-déterminisme au problème de la recherche d'un langage pour PTIME
  Résumé : Un problème central dans la théorie des modèles finis, la théorie des bases de données et la théorie de la complexité descriptive est la quête d'une logique pour PTIME. Nous présentons une approche basée sur le non-déterminisme pour aborder ce problème : elle permet d'obtenir un langage de requêtes dont le pouvoir d'expression est strictement plus grande que celui des langages connus .
 


* 23 février Mohamed Mosbah
  Les graphes de cliques


* 23 mars Bruno Courcelle
  Representation logique des dessins de graphes avec croisements d'arcs (11h-12h)


* 23 mars Luc Ségoufin (INRIA Rocquencourt)
  Interrogation des bases de donnees topographiques (14h-15)


* 30 mars Sofian Maabout (Anvers)
  Une sémantique trivaluée pour rêgles de mise à jour
  Résumé : Bien que l'introduction de rêgles du type ECA (Evénement, Condition, Action) -en anglais, trigger- dans les bases de données ait des applications potentielles trés diverses, il a été demontré que certaines proprietés fondamentales comme la terminaison et la confluence sont indecidables. Ainsi, l'utilisation de cet outil est rendu difficile.

Nous proposons d'utiliser la sémantique bien fondée [van Gelder et. al. 89] comme support pour la sémantique de rêgles dont l'évenement et l'action sont des mises a jour. Nous montrons l'applicabilité de l'approche en considerant le cas du maintien des contraintes d'intégrité. L'avantage de cette approche sont la complexite polynomiale de la sémantique, la terminaison et la confluence sont garanties. le problème est qu'on utilise une sémantique trivaluée. Nous montrons comment garantir des bases bivaluées pour une certaine classe de contraintes.


* 27 avril David Simplot (Lille)
  Itération de transductions préservant les longueurs
  Résumé : Un grand nombre d'outils et de modèles de calculs (systèmes de réécriture finis, automates cellulaires, machine de Turing, etc...) peuvent être simulés par l'itération d'une transduction rationnelle (fonction sur les mots réalisée par un automate fini avec fonction de sortie). Nous limitons notre étude aux transductions préservant les longueurs et plus particulièrement aux transductions construites à partir de transductions rationnelles (ou de fonctions rationnelles) préservant les longueurs avec les opérations d'union, composition et itération. Nous montrons que l'utilisation de transductions ou de fonctions rationnelles amène à la même classe et nous donnons plusieurs théorèmes de représentation à l'aide de différents outils (bimorphisme, langages de figures, automates cellulaires).


* 4 mai Bruno Courcelle
  D'aprés Robertson et Seymour (Mineurs de graphes n°23)


* 11 mai Teodore Knapik (la Réunion)
  Un aller-retour entre les semi-systèmes de Thue et les graphes infinis
  Résumé : L'exposé donne une approche de spécifications et vérifications de systèmes infinis. Cette approche, appelée spécifications de Thue, est basée sur les systèmes de Thue (i.e. équations entre mots). On s'intéresse à la version "orientée" des systèmes de Thue, i.e. systèmes de réécriture de mots.

Une spécification de Thue est un triplet (S,L,u) où S est un semi-système de Thue, L est un langage ne comportant que des mots irreductibles par rapport à S et u est un mot de S. Le modèle d'une spécification de Thue est un graphe orienté simple ayant une racine et vérifiant certaines conditions. (Il s'agit d'une sorte de "graphe de Cayley".)

Au cours de l'exposé on s'attachera principalement à dégager une classe de spécifications dont les modèles ont une théorie monadique du second ordre décidable. Les modèles de cette classe forment une famille de graphes observationnellement equivalents aux graphes des machines à pile.


* 25 mai Igor Walukiewicz (Varsovie)
  A fixpoint logic for languages traces


* 15 juin Giacomo Lenzi (Pise)
  Un prototype de systèmes d'axiomes pour la logique temporelle CTL*


* juin Philippe Narbel
   

9   Année 1996-97

Groupe de travail géré par P.A. Wacrenier

   


* 14 Octobre 96 Denis Lapoire
  Découpe de cartes


* 21 Octobre 96 David Janin
  Du théorème de Kleene au théorème de Stupp via les calculs de points fixes


* 28 Octobre 96 Denis Lapoire
  Titre à préciser


* 18 Novembre 96 Dirk Janssens (Univ. Anvers)
  Systèmes ESM


* 25 Novembre 96 Anne Bottreau
  Problèmes d'énumération et réécriture de graphes


* 2 Décembre 96 Nicolas Magnier
  Sur la décidabilité des problèmes de préservation de contraintes d'intégrité


* 16 Décembre 96 Mohamed Mosbah
  Marches aléatoires dans un graphe


* 6 Janvier 97 Renate Klempien-Hinrichs
  Remplacements de sommets dans des hypergraphes


* 13 Janvier 97 Sébastien Limet (Orléans)
  Unification dans les systèmes de réécriture et langages d'arbres


* 20 Janvier 97 Jérôme Olivier DURAND-LOSE
  Résultats de décidabilité sur les Automates Cellulaires



* 10 Mars 97 Laurent Pelecq
  Groupe d'automorphisme des graphes équationnels


* 24 Mars 97 Jérôme Olivier DURAND-LOSE
  Résultats de décidabilité sur les Automates Cellulaires


* 21 Avril 97 Géraud Sénizergues
  L(A) = L(B) ?


* 28 Avril 97 Pierre Tisseur - Marseille
  Vitesse de propagation de l'information, entropie et automates cellulaires

10   Année 1995-96

Groupe de travail géré par par P.A. Wacrenier

   


* 25 Septembre 95 André Arnold
  µ-calcul booléen, automates, graphes et jeux sur les graphes


* 9 Octobre 95 Christophe Reutenauer
  Variétés et fonctions rationnelles


* 16 Octobre 95 David Janin
  µ-calcul modal vs logique monadique du second ordre


* 23 Octobre 95 Anca Muscholl
  On trace codings


* 30 Octobre 95 Klaus Barthelmann
  Proving properties of distributed computations


* 13 Novembre 95 Laurent Pélecq
  Groupe d'automorphismes d'un graphe context-free


* 20 Novembre 95 Géraud Sénizergues
  Groupes agissant sur des graphes context-free


* 27 Novembre 95 Bruno Patrou
  Enveloppes z-libres, Opération zigzag binaire


* 11 Décembre 95 Bruno Courcelle
  Structures de graphes définissables en logique monadique du second-ordre


* 18 Décembre 95 Bruno Patrou
  Sur deux extensions de l'étoile de Kleene


* 22 Janvier 96 Géraud Sénizergues
  Sur la terminaison des systemes semi-Thuéiens à une règle


* 5 Février 96 Bruno Courcelle
  Décomposition de Tutte des graphes 2-connexes en Logique Monadique du 2nd ordre


* 19 Février 96 Mohamed Mosbah
  Calcul des fonctions Max-Min sur des graphes structurés


* 26 Février 96 Klaus Barthelmann
  VR sets of hypergraphs are HR if their tree-width is bounded


* 18 Mars 96 Yves Métivier
  Détection locale de la terminaison globale d'un algorithme distribué


* 1 Avril 96 Michel Billaud
  Erreurs fatales dans les expressions conditionnelles


* 20 Mai 96 Denis Lapoire
  Algèbre de Cartes


This document was translated from LATEX by HEVEA.