|
|
* 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. |