![[.ics]](small_ics.png)
| Orateur | Volker Diekert (Universität Stuttgart, ) |
| Date | Mardi 23 juin 2015 |
| Salle | 178 |
| Titre | Word equations and EDT0L languages |
| Résumé | In my talk I speak about a joint work with Laura Ciobanu and Murray Elder which will appear at ICALP 2015. The result is an easy to understand algorithm for the following problem. Input. A word equation with rational constraints in free groups (resp. free monoids with involution). Ouput. An NFA which accepts a rational language of Endomorphisms over an extended alphabet defining an EDT0L which represents all solutions in reduced words. Such a simple description was previously known only for quadratic word equations by Ferté, Marin, Sénizergues (Theory of Computing systems 2014). |
| Orateur | Makoto Kanazawa (National Institutes of Informatics (Tokyo), ) |
| Date | Mardi 10 mars 2015 |
| Salle | salle 76 |
| Titre | Enumerating One-Variable Tree Patterns That Match a Given Tree |
| Résumé | Motivated by "distributional learning" of non-linear tree grammars, I consider the problem of enumerating one-variable tree patterns that match a given tree. This problem arises when a distributional learner tries to find all ways of decomposing a given derived tree into a "substructure" and a "context". A one-variable tree pattern is a tree with holes, which should be filled by a single tree. Such a tree pattern P[x] is said to "match" a tree T (with no holes) if there is a subtree T' of T such that P[T'] (the result of filling the holes of P[x] with T') equals T. It is easy to see that there are in general exponentially many one-variable tree patterns that match a given tree. Restricting the search space to "k-copying" one-variable tree patterns (with at most k holes) trivially makes it possible to enumerate all matching tree patterns in polynomial time, but this class of tree patterns is not closed under composition, and for this reason is not so useful for the intended application to distributional learning. I show that the restriction to the class of all (iterated) compositions of k-copying one-variable tree patterns reduces the number of matching tree patterns to less than n^{k+1}, and makes it possible to enumerate them all in polynomial time. This is part of joint work with Alex Clark, Greg Kobele, and Ryo Yoshinaka. |
| Orateur | Gabriele Puppis (LaBRI, ) |
| Date | Mardi 3 mars 2015 |
| Salle | salle 76 |
| Titre | Non-determinism vs two-way |
| Résumé | Non-determinism and walking mechanisms were considered already at the very beginning of automata theory. A classical result by Rabin and Scott shows that deterministic finite state automata (DFA) are as expressive as their non-deterministic and two-way counterparts (NFA and 2DFA). The translation from 2DFA to NFA is easily seen to imply an exponential blowup in the worst case. The converse translation, which is based on the subset construction and maps NFA to DFA, also implies an exponential blowup. This latter translation, however, is not known to be optimal when one aims at removing non-determinism by possibly introducing two-wanness. In particular, the question of whether the exponential blowup is unavoidable when transforming NFA to 2DFA is open. In a short paper, Sipser has attempted to answer the above question by identifying a family of languages that are optimal candidates for separating small NFA from small 2DFA. The paper shows that there are languages that can be recognised by NFA of size n, but cannot be recognised by sweeping deterministic automata (i.e. special forms of 2DFA) of size less than 2^n. I will present a simplified version of Sipser's proof and discuss some generalisations of it. |
| Orateur | David Janin (LaBRI, ) |
| Date | Mardi 27 janvier 2015 |
| Salle | salle 178 |
| Titre | The inverse monoid of higher dimensional strings |
| Résumé | Is there a notion of higher dimensional strings, equipped with a simple string product, such that one can generate essentially all finite graphs ? By extending Stephen’s representation theorem’s of inverse semigroups, we can give a positive answer to this question. More precisely, we define the category of unambiguous graphs and connecting morphisms and we prove it admits pushouts. Then, we derive from such a category an inverse monoid of k-birooted graphs, aka higher dimensional strings, and we show it generalizes Courcelle’s approach for generating and studying (languages of) graphs of bounded tree width. |
| Orateur | Nicolas de Rugy (Université Denis Diderot - Paris 7, ) |
| Date | Mardi 20 janvier 2015 |
| Salle | salle 76 |
| Titre | Model checking en logique de dépendance |
| Résumé | La logique de dépendance et ses variantes (indépendance et inclusion) ont été introduites par Vänäänen il y a quelques années pour parler de façon "propre" de dépendance en logique. Je présenterai cette logique et ses résultats principaux en complexité. |
| Orateur | Laure Daviaud (LIF, ) |
| Date | Mardi 16 décembre 2014 |
| Salle | salle 76 |
| Titre | Asymptotic behaviour of max-plus automata and size-change abstraction |
| Résumé | Max-plus automata are weighted automata over the semiring (NU{-infinite}, max, +) that compute some functions from words to NU{-infinite}. More precisely, a (max,+)-automaton is a non deterministic finite automaton with a weight on each transition. The weight of a given run is the sum of the weights of the transitions along the run and the weight of a word w is the maximum of the weights of the runs labelled by w and going from an initial state to a final state. In this talk, we will study the asymptotic behaviour of a max-plus automaton and more precisely the maximum length of a word of weight at most n. In particular, I will show that this function is of the form Theta(n^alpha) for a computable rational alpha. I will also explain how this analysis can, in combination with the size-change abstraction, be used for inferring the termination time of an algorithm as a function of the size of its input. This is a joint work with Thomas Colcombet (LIAFA, Université Paris 7, CNRS) and Florian Zuleger (Vienna University). |
| Orateur | Luc Segoufin (INRIA, ) |
| Date | Mardi 9 décembre 2014 |
| Salle | salle 76 |
| Titre | Constant delay enumeration for database queries |
| Résumé | In this talk we will survey some of the recent results about enumerating the answers to queries over a database. We focus on the case where the enumeration is performed with a constant delay between any two consecutive solutions, after a linear time preprocessing. We will consider conjunctive, FO, and MSO queries. Constant Delay enumeration cannot be always achieved. It requires restricting either the class of queries or the class of databases. We will describe several scenarios when this is possible. |
| Orateur | Bruno Karelovic (Liafa, ) |
| Date | Mardi 2 décembre 2014 |
| Salle | salle 76 |
| Titre | Concurrent parity games with pure memoryless winning strategies |
| Résumé | In this talk we reexamine concurrent stochastic parity games. As it is known for such games the set of states X1 where player 1 can win almost surely can be strictly included in the set W1 of states having value 1 where player 1 has a strategy allowing him to win with a probability as close to 1 as he wishes. This strict inclusion holds even for the simplest classes of parity games like reachability games and Buchi games. In this talk we exhibit a natural class of stochastic concurrent parity games such that the sets X1 and W1 defined above are equal. Moreover player 1 has a pure memoryless strategy such that for games starting in X1 = W1 he wins almost surely. By symmetry a similar property holds for player 0 and for states having value 0. On the other hand, we show that in the same class of games players do not have optimal strategies for games starting in states with values strictly between 0 and 1. |
| Orateur | Noémie Meunier (Université de Mons, FNRS, ) |
| Date | Mardi 25 novembre 2014 |
| Salle | salle 178 |
| Titre | Secure Equilibria in Weighted Games |
| Résumé | We consider two-player non zero-sum infinite duration games played on weighted graphs. We extend the notion of secure equilibrium introduced by Chatterjee et al., from the Boolean setting to this quantitative setting. As for the Boolean setting, our notion of secure equilibrium refines the classical notion of Nash equilibrium. We prove that secure equilibria always exist in a large class of weighted games which includes common measures like sup, inf, lim sup, lim inf, mean-payoff, and discounted sum. Moreover we show that one can synthesize finite-memory strategy profiles with few memory. We also prove that the constrained existence problem for secure equilibria is decidable for sup, inf, lim sup, lim inf and mean-payoff measures. Our solutions rely on new results for zero-sum quantitative games with lexicographic objectives that are interesting on their own right. |
| Orateur | Lorijn van Rooijen (LaBRI, ) |
| Date | Mardi 18 novembre 2014 |
| Salle | salle 76 |
| Titre | A combinatorial approach to the separation problem |
| Résumé | The separation problem, for a class S of languages, is the following: given two input languages, does there exist a language from S that contains the first language and that is disjoint from the second language? For regular input languages, the separation problem for a class S subsumes the classical membership problem for this class, and provides more detailed information about the class. The separation problem emerged in different contexts, and has been studied, for specific classes of languages, using involved profinite methods. We will discuss an approach to this problem that only uses elementary combinatorial arguments. This approach furthermore gives a description of a separating language, in case it exists. In this talk, we focus on the separation problem for the classes of piecewise testable languages and of FO2-definable languages. This is joint work with Thomas Place and Marc Zeitoun. |
| Orateur | Charles Grellois (PPS/Liafa, ) |
| Date | Mardi 4 novembre 2014 |
| Salle | salle 76 |
| Titre | Type systems and logical models for higher-order verification |
| Résumé | Verifying functional programs is a complex issue, due to their higher-order nature: in such programs, a function may take another function as argument. Ong proved however in 2006 that one can decide if such a program, modelled as a recursion scheme, satisfies a given MSO formula. Other proofs were given since, and all of them make use of semantic notions: game semantics, logical models, type systems... After introducing the main elements of this model-checking problem, we will see how all these concepts relate and allow the logical analysis of recursion schemes. |
| Orateur | Diego Figueira (LaBRI, ) |
| Date | Mardi 21 octobre 2014 |
| Salle | salle 76 |
| Titre | Basic model theory of XPath on data trees |
| Résumé | We investigate model theoretic properties of XPath with data (in)equality tests over the class of data trees, i.e., the class of trees where each node contains a label from a finite alphabet and a data value from an infinite domain. We provide notions of (bi)simulations for XPath logics containing the child, descendant, parent and ancestor axes to navigate the tree. We show that these notions precisely characterize the equivalence relation associated with each logic. We study formula complexity measures consisting of the number of nested axes and nested subformulas in a formula; these notions are akin to the notion of quantifier rank in first-order logic. We show characterization results for fine grained notions of equivalence and (bi)simulation that take into account these complexity measures. We also prove that positive fragments of these logics correspond to the formulas preserved under (non-symmetric) simulations. We show that the logic including the child axis is equivalent to the fragment of first-order logic invariant under the corresponding notion of bisimulation. This talk is based in a joint work with Santiago Figueira (UBA, Argentina) and Carlos Areces (UNC, Argentina) presented in ICDT'14. |
| Orateur | Bruno Courcelle (LaBRI, ) |
| Date | Mardi 14 octobre 2014 |
| Salle | salle 76 |
| Titre | Vérification de propriétés de graphes au moyen d'automates programmés (fly-automata). |
| Résumé | La transformation des formules de la logique du second-ordre monadique en automates fournit des automates trop grands pour être construits. Mais ces automates peuvent être définis par des "petits" programmes qui calculeront "à la demande" les états et les transitions nécessaires pour traiter un terme donné. Cette méthode, basée sur les "automates programmés", a été testée et s'applique à des propriétés non exprimables en logique du second-ordre monadique. Exposé en français, transparents et questions en anglais. Slides will be in English Abstract: The automata produced from MSO formulas are usually too large to be constructed. But they can be described by "small" programs. Fly automata compute on the fly the necessary states and transitions. They can check graph properties that are not MSO expressible. |