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