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