Previous Next Contents

4   Année 2001-2002

   


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


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


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


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


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

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

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


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


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


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


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

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


* 8 avril Le projet VISIDIA
  M. Mosbah


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


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

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

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


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

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

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

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


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

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

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

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

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


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


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


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


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


Previous Next Contents