![[.ics]](small_ics.png)
| Orateur | Alfredo Costa (University of Coimbra, ) |
| Date | Vendredi 25 mai 2012 |
| Salle | salle 178 |
| Titre | Some operators that preserve the locality of a pseudovariety of semigroups. |
| Résumé | Finite semigroups are a useful algebraic tool to decide computational problems from automata theory, formal languages and logic. In this framework, the decidability of a property is quite often reduced to the decidability of (the membership in) a pseudovariety of semigroups. For example, a language of finite words can be expressed by a sentence of the first order fragment FO^2[<] if and only of its syntactic semigroup belongs to the pseudovariety DA, as shown by Thérien and Wilke. Frequently a pseudovariety is expressed in terms of more simple decidable pseudovarieties, using operations between them, like the Mal'cev product and the semidirect product. However, these operations do not always preserve decidability. In this context, an algebraic property of pseudovarieties called "locality" is useful. For example, Thérien and Wilke showed that the pseudovariety corresponding to FO^2[<,suc] is DA*D, which is decidable since Almeida proved DA is local. We study a family of Mal'cev operators of the form Z(m)_, showing that some of them preserve the locality of pseudovarieties. In the process, we deal with the localization operator L( ) and the semidirect product operator ( )*D, establishing some interplay between them. Among these operators we find K(m)_ and D(m)_. As an application, we deduce that the pseudovarieties in the hierarchies R_1, R_2, R_3... and L_1, L_2, L_3... of subpseudovarieties of DA, obtained from J by alternate application of the operators K(m)_ and D(m)_, are local when m>1. These pseudovarieties are interesting, since recently Kufleitner and Weil proved the decidability of the variety of languages expressed by the fragment of sentences of FO^2[<] with at most m alternating blocks of quantifiers in its parsing tree, by showing that this variety corresponds to the intersection between R_m and L_m. This is joint work with Ana Escada. |
| Orateur | Antoine Durand-Gasselin (Liafa, Université Paris Diderot, ) |
| Date | Mardi 15 mai 2012 |
| Salle | salle 76 |
| Titre | Ehrenfeucht-Fraïssé goes elementarily automatic for structures of bounded degree |
| Résumé | Many relational structures are automatically presentable, i.e. elements of the domain can be seen as words over a finite alphabet and equality and other atomic relations are represented with finite automata.~The first-order theories over such structures are known to be primitive recursive, which is shown by the inductive construction of an automaton representing any relation definable in the first-order logic. We propose a general method based on Ehrenfeucht-Fraïssé games to give upper bounds on the size of these automata and on the time required to build them. We apply this method for two different automatic structures which have elementary decision procedures, Presburger Arithmetic and automatic structures of bounded degree. For the latter no upper bound on the size of the automata was known. We conclude that the very general and simple automata-based algorithm works well to decide the first-order theories over these structures. (joint work with Antoine Durand-Gasselin) |
| Orateur | Sergueï Lenglet (PPS, Université Paris-Diderot, ) |
| Date | Mardi 17 avril 2012 |
| Salle | salle 76 |
| Titre | Bisimulations pour les opérateurs de contrôle délimité |
| Résumé | Nous présentons les premiers résultats sur la définition d'une théorie comportementale pour un lambda-calcul étendu avec les opérateurs de contrôle délimité shift et reset. Dans un premier temps, nous définissons une notion d'équivalence comportementale, que nous cherchons ensuite à caractériser à l'aide de bisimulations (applicative et de forme normale). Nous étudions aussi la relation entre équivalence comportementale et une autre équivalence basée sur une transformation CPS. |
| Orateur | Yann Strozecki (LRI, Paris-Sud 11, ) |
| Date | Mardi 10 avril 2012 |
| Salle | salle 76 |
| Titre | Largeur de décomposition d'hypergraphe |
| Résumé | Dans cet exposé, je vais présenter une décomposition arborescente d'hypergraphe. Cette notion est très simple et généralise notamment des notions de décomposition sur les matroïdes. On va montrer certaines propriétés de cette décomposition par rapport à divers opérations sur les hypergraphes ainsi que des exemples d'hypergraphes qui ont une petite ou une grande largeur. Par ailleurs, cette décomposition admet plusieurs restrictions intéressantes, et sur les graphes elle est équivalente à la largeur de clique. Enfin, on s'intéressera au problème de trouver en temps polynomial de bonnes décomposition pour des hypergraphes. |
| Orateur | Olivier Serre (Liafa, ) |
| Date | Mardi 3 avril 2012 |
| Salle | salle 76 |
| Titre | Qualitative Tree Languages |
| Résumé | We study finite automata running over infinite binary trees and we relax the notion of accepting run by allowing a negligible set (in the sense of measure theory) of non-accepting branches. In this qualitative setting, a tree is accepted by the automaton if there exists a run over this tree in which almost every branch is accepting. This leads to a new class of tree languages, called the qualitative tree languages that enjoys many properties. Then, we replace the existential quantification — a tree is accepted if there exists some accepting run over the input tree — by a probabilistic quantification — a tree is accepted if almost every run over the input tree is accepting. Together with the qualitative acceptance and the Büchi condition, we obtain a class of probabilistic tree automata with a decidable emptiness problem. To our knowledge, this is the first positive result for a class of probabilistic automaton over infinite trees. |
| Orateur | Jorge Almeida (University of Porto, ) |
| Date | Mardi 27 mars 2012 |
| Salle | salle 76 |
| Titre | Schützenberger groups of primitive substitutions are decidable |
| Résumé | (joint work with Alfredo Costa) It is well known that the words that appear as factors in the iteration on the letters of a primitive endomorphism (substitution) f of the free semigroup on a finite alphabet A is the language of blocks of a minimal symbolic dynamical system (subshift) X_f, consisting of biinfinite words over the alphabet A whose blocks are those factors. I proved in 2005 that, associating to a minimal subshift X over the alphabet A the closure J(X) of its language of blocks in the profinite semigroup freely generated by A, one obtains a bijection between minimal subshifts and J-maximal regular J-classes. My co-author showed in his thesis that, viewed as an abstract group G(X), the maximal subgroups of J(X) constitute a conjugacy invariant. I also showed that, if f induces an automorphism of the free group on A, then G(X_f) is a free profinite group, while there are examples for which G(X_f), which is always finitely generated, is not a free profinite group. Rhodes and Steinberg proved that the closed subgroups of a free profinite semigroup are projective as profinite groups. Hence, as observed by Lubotzky, if finitely generated, such groups admit finite presentations, as profinite groups, in which the relations simply state that each generator is a fixed point of a retraction of the free profinite group. I conjectured in 2005 that, under special conditions on the primitive substitution f, the group G(X_f) admits such a presentation in which the retraction is obtained as a (profinite) idempotent iterate of a positive finite continuous endomorphism f' of the free profinite group, where f' can be effectively computed from f. The interest in such presentations stems from the fact that the relations can be effectively checked in a given finite group, so that the group with such a retract presentation has decidable finite quotients. It turns out that the conjecture holds for every primitive substitution f. It is therefore decidable whether a finite group is a quotient of G(X_f). The proof of the conjecture in such a wide setting depends on a synchronization result of Mossé for (biinfinite) fixed points of primitive substitutions. As an application, we show that the group associated with the classical Prouhet-Thue-Morse substitution (a -> ab, b -> ba) is not free. |
| Orateur | Amélie Stainer (INRIA, ) |
| Date | Mardi 20 mars 2012 |
| Salle | salle 76 |
| Titre | A game approach to determinize timed automata |
| Résumé | Timed automata are frequently used to model real-time systems. Their determinization is a key issue for several validation problems. However, not all timed automata can be determinized, and determinizability itself is undecidable. In this talk, we will present a game-based algorithm which, given a timed automaton, tries to produce a language-equivalent deterministic timed automaton, otherwise a deterministic over-approximation. Our method subsumes two recent contributions: it is at once more general than a recent determinization procedure and more precise than the existing over-approximation algorithm. Then, we will explain how this method can be adapted to be usefull for test generation. This talk is a joint work with Nathalie Bertrand, Thierry Jéron and Moez Krichen. Papers have been presented at FoSSaCs'11 and TACAS'11. |
| Orateur | Michał Skrzypczak (University of Warsaw, ) |
| Date | Mardi 13 mars 2012 |
| Salle | salle 76 |
| Titre | MSO+U defines languages at arbitrarily high levels of the projective hierarchy |
| Résumé | This work shows that for each i ∈ N there exists a ω-word language H_i definable in Monadic Second Order Logic extended with the unbounding quantifier (MSO + U) such that H_i is hard for i'th level of the projective hierarchy. Since it is not hard to see that each language expressible in MSO + U is projective, our finding solves the topological complexity of MSO + U. The result can immediately be transferred from ω-words to infinite labelled trees. As a consequence of the topological hardness we note that no alternating automaton with a Borel acceptance condition — or even with an acceptance condition of a bounded projective complexity — can capture all of MSO + U. |
| Orateur | Romain Brenguier (LSV, ) |
| Date | Mardi 6 mars 2012 |
| Salle | salle 76 |
| Titre | Nash equilibria in concurrent games |
| Résumé | We consider concurrent games played on graphs, and we want to decide the existence of a Nash equilibrium (possibly with a condition on the payoffs). We propose a general transformation from multiplayer games to zero-sum game and use it to characterise the exact complexity of the Nash equilibrium problem for classical objectives. We also extend the study to a more quantitative setting in which each player has several reachability or Büchi objectives, and a preorder on these objectives (for instance the counting order, where the aim is to maximise the number of objectives that are fulfilled). This is joint work with Patricia Bouyer, Nicolas Markey and Michael Ummels. |
| Orateur | Frédérique Carrere (LaBRI, ) |
| Date | Mardi 21 février 2012 |
| Salle | salle 76 |
| Titre | Balancing weighted binary trees in linear time. |
| Résumé | In this talk, we consider weighted binary trees, i.e., binary trees whose leaves hold positive constants called weights. We survey different balance definitions for weighted binary trees and different algorithms to build them from a sequence of weights. We consider the alphabetic version of the problem. In this case the leaves of the balanced alphabetic tree (read left-to-right) should be in the same order as in the original sequence. We present an incremental algorithm to build balanced alphabetic weighted trees in linear time. |
| Orateur | Pierre Halftermeyer (LaBRI, ) |
| Date | Mardi 14 février 2012 |
| Salle | salle 76 |
| Titre | Connexité dans les graphes de genre g avec obstacles: un schéma d'étiquetage. |
| Résumé | Nous présenterons une methode d'étiquetage compact d'un graphe G de genre g de façon à ce qu'on puisse répondre à une requête de connexité entre le sommet u et v dans G-X à partir des étiquettes de u, de v et de celles des sommets de X. |
| Orateur | Giulio Manzonetto (LIPN, Université Paris-Nord, ) |
| Date | Mardi 7 février 2012 |
| Salle | salle 76 |
| Titre | Lambda Calculus: The Differential Viewpoint |
| Résumé | We survey the central role of lambda calculus in theoretical computer science, with particular interest for its connections with programming languages, logic and category theory. Motivated by the discovery of denotational models of Linear Logic (LL) such as finiteness spaces, where all morphisms can be differentiated, we introduce the differential lambda-calculus which features two ways of applying a function to an argument: the standard one and a linear one, implementing differentiation. This approach allows to generalize Boudol’s resource calculus, in a framework where useful tools from analysis, like the Taylor expansion formula, can be applied. No prerequisites of lambda-calculus are supposed to follow the talk. |
| Orateur | David Janin (LaBRI, ) |
| Date | Mardi 31 janvier 2012 |
| Salle | salle 75 |
| Titre | Quasi-inverse monoids : towards an algebraic characterization of MSO-definable languages of overlapping one-dimensionnal tiles |
| Résumé | In this talk, we consider the notion of inverse monoid together with the notion of prehomomorphism (variant of McAlister definition) between ordered monoids. More precisely, we consider the class of images of (naturally ordered) inverse monoids by prehomomorphisms. Doing so, we define and study a subclass (?) of such monoids, called quasi-inverse monoids, that generalizes the class of inverse monoids. We show in particular that a natural order can be define on quasi-inverse monoids much in the same way the natural order is defined over inverse monoid. We also show that any (finite) monoid S can be embedded into a (finite) quasi-inverse monoid Q(S). This extension theorem leads to a partial algebraic characterization of MSO-definable languages of positive tiles (within McAlister inverse monoid). With some extra (but rather natural) closure hypothesis and definability conditions : these languages are just inverse images by prehomomorphism of finite subsets of quasi-inverse monoid. The two main definitions we are concerned about: 1) A monoid S is an inverse monoid when, for every x, there exists a unique y such that x y x = x and y x y = y 2) When both S and T are ordered monoid with product compatible with order a mapping f:S -> T is a prehomomorphism when : a) f(1) = 1 and (if ever) f(0) = 0, b) f(x) <= f(y) whenever x <= y c) f(xy) <= f(x) f(y) (instead of f(xy) = f(x) f(y) hence the name of such a mapping) d) f(x)f(y)=f(y)f(x) whenever xy=yx |
| Orateur | Thomas Colcombet (Liafa, ) |
| Date | Mardi 24 janvier 2012 |
| Salle | salle 76 |
| Titre | Topological Monadic Logic |
| Résumé | Topological monadic logic refers to weighted structures, i.e., structures whose elements are labelled with non-negative integers called weight. Topological monadic logic extends monadic logic with the ability to express that "there is a bound on the weights appearing on a set X" where X is a monadic variable. We consider this logic over weighted infinite words (of length omega), and we conjecture that the satisfaction of this logic is decidable (thus extending Büchi's seminal result). In this talk we introduce several equivalent formalisms for this logic, and we present results of normal forms for this logic. We describe the Borel complexity of this logic, and compare its expressiveness with the one of the logic MSO+U. Finally, we will reduce the open conjecture to some new forms of tiling problems. |
| Orateur | Pedro Silva (University of Porto, ) |
| Date | Mardi 17 janvier 2012 |
| Salle | salle 76 |
| Titre | WREATH PRODUCT: AN APOLOGY |
| Résumé | The algebraic definition of the wreath product seems at first sight obscure and hostile. However, by considering actions of monoids/groups on trees, this often unpopular operator becomes natural and clear. The use of the wreath product to obtain decompositions of algebraic structures has its most charismatic example in the Krohn-Rhodes Theorem: every finite monoid divides a wreath product of finite simple groups and very small aperiodic monoids. This approach admets extensions to the infinite case, and the wreath product is also essential in the exotic theory of self-similar groups. We shall speak of our recent contributions to these theories, in joint work with Rhodes or Steinberg and Kambites. |
| Orateur | Thomas Place (University of Warsaw, ) |
| Date | Mardi 13 décembre 2011 |
| Salle | salle 76 |
| Titre | Regular languages of infinite trees that are boolean combinations of open sets. |
| Résumé | This talk will be about boolean (not necessarily positive) combinations of open sets. I will present a decidable characterization of the regular languages of infinite trees that are boolean combination of open sets. In other words, I will present an algorithm, which inputs a regular language of infinite trees, and decides if the language is a boolean combination of open sets. This algorithm uses algebra and will be introduced as a set identities that are satisfied if and only if a language is a boolean combination of open sets and are easily decidable. |
| Orateur | Laurent Doyen (CNRS, LSV, ) |
| Date | Mardi 6 décembre 2011 |
| Salle | salle 76 |
| Titre | Partial-Observation Stochastic Games: How to Win when Belief Fails |
| Résumé | We consider two-player stochastic games played on finite graphs with reachability (and Buechi) objectives where the first player tries to ensure a target state to be visited (or visited infinitely often) almost-surely, i.e., with probability 1, or positively, i.e., with positive probability, no matter the strategy of the second player. We classify such games according to the information and to the power of randomization available to the players. On the basis of information, the game can be one-sided with either (a) player 1, or (b) player 2 having partial observation, or two-sided with (c) both players having partial observation. On the basis of randomization, (a) the players may not be allowed to use randomization (pure strategies), or (b) they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) they may use full randomization. Our main results for pure strategies are as follows: (1) For one-sided games with player 2 perfect observation we show that (in contrast to full randomized strategies) belief-based strategies are not sufficient, and we present an exponential upper bound on memory both for almost-sure and positive winning strategies; we show that the problem of deciding the existence of almost-sure and positive winning strategies for player 1 is EXPTIME-complete. (2) For one-sided games with player 1 perfect observation we show that non-elementary memory is both necessary and sufficient for both almost-sure and positive winning strategies. (3) We show that for the general (two-sided) case finite-memory strategies are sufficient for both positive and almost-sure winning, and at least non-elementary memory is required. We establish the equivalence of the almost-sure winning problems for pure strategies and for randomized strategies with actions invisible. Our equivalence result exhibits serious flaws in previous results in the literature: we show a non-elementary memory lower bound for almost-sure winning whereas an exponential upper bound was previously claimed. |
| Orateur | Laurent Braud (LaBRI, ) |
| Date | Mardi 29 novembre 2011 |
| Salle | salle 76 |
| Titre | Towards nominal computation |
| Résumé | Nominal sets are a different kind of set theory, with a more relaxed notion of finiteness. They offer an elegant formalism for describing lambda-terms modulo alpha-conversion, or automata on data words. This presentation is an attempt at defining computation in nominal sets. We present a rudimentary programming language, called Nλ. The key idea is that it includes a native type for finite sets in the nominal sense. |
| Orateur | Łukasz Kaiser (CNRS, Liafa, ) |
| Date | Mardi 22 novembre 2011 |
| Salle | salle 76 |
| Titre | The Field of Reals is not omega-Automatic |
| Résumé | We investigate structural properties of omega-automatic presentations of infinite structures in order to sharpen our methods to determine whether a given structure is omega-automatic. We apply these methods to show that no field of characteristic 0 admits an injective omega-automatic presentation, and that uncountable fields with a definable linear order cannot be omega-automatic. |
| Orateur | David Janin (LaBRI, ) |
| Date | Mardi 15 novembre 2011 |
| Salle | salle 76 |
| Titre | Sur les langages de triplets de mots |
| Résumé | On s'intéresse aux langages de triplets de mots finis de la forme (u1,u2,u3) qui ont pour vocation à représenté des mots «contextualisés». Plus précisément, le triplet de mot (u1,u2,u3) représente le mot u2 dont l’usage est restreint à un certain contexte d’utilisation définit par u1 et u3 de la façon suivante : un tel mot ne peut être concaténé, à gauche, que par un mot finissant par u1 et à droite, que par un mot commençant par u3. L'étude de ce modèle, apparemment ad hoc, et du produit (partiel) qu’il induit, nous conduit cependant à la définition d’une extension originale du monoïde libre qui semble répondre à une question de Jean-Camille Birget en 1992 : quelle structure algébrique correspond aux automates boustrophédons (ou two way automata). En développant cette théorie, on obtient en particulier, pour les langages de triplets : - d’une notion d'automate boustrophédons déterministe canonique (minimal ?), - d’une notion d'expression rationnel, - d’une notion algébrique de reconnaissabilité, toutes trois équivalentes. La théorie obtenue, qui poursuit les travaux de Rabin et Scott (1959), Shepherdson (1959), Pecuchet (1985), Birget (1989), et de nombreux autres (e.g. Vardi, 1989, Hines 1997), se révèle tout à la fois simple, conséquente et solide. Elle semble ouvrir de nombreuses perspectives aussi bien en algèbre : quelle structure algébrique générique sous-jacente à ce monoid des triplets ? en théorie des automates : quelles liens avec les pebbles two-way automata ? et, en plongeant les mots dans les mots temporisés : quelles expressions algébriques induites pour les langages temporisés ? |
| Orateur | Olivier Gauwin (LaBRI, ) |
| Date | Mardi 8 novembre 2011 |
| Salle | salle 76 |
| Titre | Analyse d'automates à pile pour XML |
| Résumé | Les documents XML sont habituellement représentés sous forme arborescente. Les langages de requête associés, comme XPath, sont des langages navigationnels dans ces arbres, et les automates usuels utilisent des parcours ascendants. Lire les balises d'un document XML l'une après l'autre revient à parcourir l'arbre correspondant dans l'ordre préfixe. Les automates à pile deviennent alors plus adaptés que les automates d'arbres classiques. Dans cet exposé, je poserai le problème consistant à répondre aux requêtes au plus tôt, selon ce type de parcours des arbres. Je montrerai qu'il se réduit à décider, pour un préfixe fixé, si tout suffixe "bien formé" est accepté. Je présenterai deux algorithmes pour ce problème, lorsque les requêtes sont données par des automates à pile. |
| Orateur | Achim Blumensath (Liafa, université Paris 7, ) |
| Date | Mardi 18 octobre 2011 |
| Salle | salle 76 |
| Titre | Recognisability for infinite trees |
| Résumé | We develop a framework for recognisability of languages of infinite trees. This framework has the same expressive power as tree automata. We present an algebraic proof of Rabin's Tree Theorem that does not make use of automata or games. |
| Orateur | Bruno Courcelle (LaBRI, ) |
| Date | Mardi 11 octobre 2011 |
| Salle | salle 178 |
| Titre | Orientations et ordres totaux définissables en logique du second-ordre monadique |
| Résumé | J'examine dans quelle mesure il est possible de définir en logique du second ordre monadique, pour un graphe non orienté: une orientation, toutes les orientations, un ordre total. Les réponses ne sont pas les mêmes avec ou sans quantifications sur les ensembles d'arêtes. Je mets en évidence des conditions combinatoires qui rendent ces définitions possibles. Certains résultats sont obtenus avec A. Blumensath. |
| Orateur | David Janin (LaBRI, ) |
| Date | Mardi 4 octobre 2011 |
| Salle | salle 76 |
| Titre | Langages de rythmes : une approche formelle |
| Résumé | Nous nous intéressons ici à la modélisation des motifs rythmiques. En passant en revue les approches existantes, nous sommes amené étendre le modèle classique des mots temporisés (avec représentation en durée relative) utilisables en musiques en un modèle de mots triplements pondérés. Ce modèle permet en effet de distinguer, pour tout motif rythmique (comme pour tout processus industriel) : une introduction, un développement et une conclusion. Cette approche, qui induit des opérateurs de composition et de transformation pertinents pour la modélisation musicale, posent plusieurs questions intéressantes de théorie des langages. Séquentialité, parallélisme, temporisation et hiérarchisation semblent par ailleurs et enfin pouvoir être abordé dans un même formalisme. De nombreux développements en perspective ? |
| Orateur | Hugo Gimbert (LaBRI, ) |
| Date | Mardi 27 septembre 2011 |
| Salle | salle 76 |
| Titre | A Class of Probabilistic Automata with a Decidable Value 1 Problem |
| Résumé | The value 1 problem is a decision problem for probabilistic automata over finite words: given a probabilistic automaton A, are there words accepted by A with probability arbitrarily close to 1? This problem was proved undecidable recently, even in restricted cases. We introduce a new class of probabilistic automata, called *leak-tight automata*, for which the value 1 problem is shown decidable (and PSPACE-complete). We construct an algorithm based on the computation of a monoid abstracting the behaviours of the automaton. The correctness proof on this algorithm relies on algebraic techniques developed by Simon. |