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