![[.ics]](small_ics.png)
| Orateur | Benjamin Monmege (ENS Cachan, ) |
| Date | Mardi 2 juillet 2013 |
| Salle | salle 76 |
| Titre | Specification of Quantitative Properties: Logics, Automata, Expressions |
| Résumé | Automatic verification has nowadays become a central domain of investigation in computer science. Over 25 years, a rich theory has been developed leading to numerous tools, both in academics and industry, allowing the verification of Boolean properties - those that can be either true or false. Current needs evolve to a finer analysis, a more quantitative one. Extension of verification techniques to quantitative domains has begun 15 years ago with probabilistic systems. However, many other quantitative properties are of interest, such as the lifespan of an equipment, energy consumption of an application, the reliability of a program, or the number of results matching a database query. Expressing these properties requires new specification languages, as well as algorithms checking these properties over a given structure. We study several formalisms, equipped with weights, able to specify such properties: denotational ones – like regular expressions, first-order logic, or temporal logics – or more operational ones, like navigating automata, possibly extended with pebbles. We study the compared expressiveness of these formalisms. In particular, we give efficient translations from denotational formalisms to the operational one. These objects, and the associated results, are presented in a unified framework of graph structures permitting to handle finite words, ranked trees, nested words, pictures or messsage sequence charts, as special cases. Therefore, possible applications are the verification of quantitative properties of traces of programs (possibly recursive, or concurrent), querying of XML documents (modelling databases for example), or natural language processing. We also present results about algorithmic questions that naturally arise in this context, like evaluation and satisfiability. |
| Orateur | Makoto Kanazawa (NII, ) |
| Date | Mardi 11 juin 2013 |
| Salle | salle 76 |
| Titre | Multi-dimensional trees and a Chomsky-Schützenberger-Weir representation theorem for simple context-free tree grammars |
| Résumé | Weir (1987) showed that every tree-adjoining language can be expressed as a homomorphic image of the intersection of three sets: a regular set R, the Dyck language D_{2n} over the alphabet consisting of 2n pairs of brackets [_1, ]_1,..., [_{2n}, ]_{2n}, and g^{-1}(D_{2n}), where g is the bijection that maps [_{2i+1} to itself and cyclically permutes ]_{2i+1}, [_{2i+2}, ]_{2i+2}, for each i = 0, ..., n-1. I generalize this theorem to simple context-free tree grammars: If L is the yield image of the language of a simple context-free tree grammar of rank m-1, then L can be expressed as a homomorphic image of the intersection of a regular set R, the Dyck language D_{mn} over the alphabet of mn pairs of brackets, and g^{-1}(D_{mn}), where g is the bijection that maps [_{mi+1} to itself and cyclically permutes ]_{mi+1}, [_{mi+2}, ]_{mi+2}, ..., [_{mi+m}, ]_{mi+m}, for i = 0, ..., n-1. I obtain this result via a natural generalization of the Chomsky-Schützenberger theorem to the tree languages of simple context-free tree grammars. This intermediate result is stated in terms of "Dyck tree languages". In order to emphasize the analogy between the string case and the tree case, I use the notion of "multi-dimensional tree" introduced by Rogers (2003). An element of a Dyck tree language is regarded as a two-dimensional encoding of a three-dimensional tree, just like an element of an ordinary Dyck language encodes an ordinary, two-dimensional tree. A simple context-free tree language is defined to be the yield image of a local set of three-dimensional trees, where the "yield" is obtained from two-dimensional encoding by erasing the "brackets". I show that many necessary lemmas can be stated as general facts about m-dimensional trees. |
| Orateur | Pierre Clairambault (University of Cambridge, ) |
| Date | Mardi 4 juin 2013 |
| Salle | salle 76 |
| Titre | Böhm trees as higher-order recursion schemes |
| Résumé | Higher-order recursive schemes (HORS) are schematic representations of functional programs. They generate possibly infinite ranked labelled trees and, viewed as tree generators, are equivalent to λY-terms of ground type in which free variables can only have types of the form o → ... → o (with o as a special case). In this talk, I will show that any λY-term (with no restrictions on term type or the types of free variables) has an equivalent presentation as a HORS. That is, for any λY-term, there exists a HORS generating a tree that faithfully represents the Böhm tree of the λY-term. In particular, the HORS encodes higher-order binding information contained in the Böhm tree. The result reduces the problem of Böhm tree equivalence for the λY-calculus to the equivalence problem for HORS and enables MSO model-checking of Böhm trees. We also show how to adapt the methodology to finitary PCF (over finite datatypes). This is joint work with Andrzej Murawski. |
| Orateur | Johann Brault-Baron (GREYC, ) |
| Date | Mardi 28 mai 2013 |
| Salle | salle 76 |
| Titre | Towards a characterisation of linear-time first-order existential queries |
| Résumé | (or three complexity dichotomy theorems for existential first-order) It is known that the data complexity of a Conjunctive Query (CQ) is determined only by the way its variables are shared between atoms, reflected by its hypergraph. In particular, Yannakakis [Yan81, BFMY83] proved that a CQ is decidable in linear time when it is alpha- acyclic, i.e. its hypergraph is alpha-acyclic; Bagan et al. [BDG07] even state: "Any CQ is decidable in linear time iff it is alpha-acyclic (under certain hypotheses)". They also prove a similar result for the enumeration problem. Since the complexity of a Negative Conjunctive Query (NCQ), a conjunctive query where all atoms are negated, also only depends on its hypergraph, there must be a similar dichotomy in this case. We show that: "Any NCQ is decidable in linear time iff it is beta-acyclic (under certain hypotheses)" and also give a similar result for the enumeration problem. If we consider Signed Conjunctive Query (SCQ), a conjunctive query where *some* atoms are negated, we need to introduce a notion of acyclicity of bicolored hypergraphs, that generalizes both alpha and beta acyclicities. With this notion, we finally generalize both previous dichotomy theorems in a single one, that deals with both the decision and the enumeration problems. This dichotomy theorem implies that beta-acyclic existential first-order queries are decidable in linear time, and that this hypergraph criterion is optimal. |
| Orateur | Damien Pous (CNRS, LIP, ) |
| Date | Mardi 14 mai 2013 |
| Salle | salle 76 |
| Titre | Checking NFA equivalence with bisimulations up to congruence |
| Résumé | We introduce "bisimulation up to congruence" as a technique for proving language equivalence of non-deterministic finite automata. Exploiting this technique, we devise an optimisation of the classical algorithm by Hopcroft and Karp which, as we show, is exploiting a weaker "bisimulation up to equivalence" technique. The resulting algorithm can be exponentially faster than the recently introduced "antichain algorithms". (joint work with Filippo Bonchi) |
| Orateur | Géraud Sénizergues (LaBRI, ) |
| Date | Mardi 30 avril 2013 |
| Salle | salle 76 |
| Titre | LALBLC: a program testing the equivalence of dpda's. |
| Résumé | We present a preliminar version of the program "LALBLC" (i.e. LA=LB? Let us Compute). The equivalence problem for dpda consists in deciding, for two given deterministic pushdown automata A,B, whether they recognize the same language. It was proved in [TCS 2001, G.S.] that this problem is decidable by means of some complete proof systems. The program LALBLC gives, in some sense, life to the above completeness proof: on an input A,B, the program computes either a proof of their equivalence (w.r.t. to the system D5 of the above reference) or computes a witness of their non-equivalence (i.e. a word that belongs to the symmetric difference of the two languages). We shall outline the main mathematical objects that are manipulated as well as the main functions performed over these objects. We shall also describe some experimental results obtained so far. The talk is based on an ongoing, joint, work with P. Henry. |
| Orateur | Benedikt Bollig (CNRS, LSV, ) |
| Date | Mardi 23 avril 2013 |
| Salle | salle 76 |
| Titre | An optimal construction of Hanf sentences over structures of bounded degree |
| Résumé | Hanf's locality theorem states that first-order sentences cannot distinguish between locally finite structures realizing the same multi-set of neighborhoods (1965). This result was sharpened by Fagin, Stockmeyer, and Vardi (1995). They prove that, given a first-order sentence of quantifier rank at most k, satisfaction in structures of bounded degree only depends on how often each isomorphism type of a neighborhood of radius 3^k occurs, counted up to some threshold. As a corollary, one obtains that every first-order formula over structures of bounded degree can be written in Hanf normal form, i.e., as a boolean combination of formulas of the form "there exist at least n realizations of neighborhood N". So far, however, there has been no elementary construction of Hanf normal forms. In this talk, we show that Hanf normal forms can be computed in triply exponential time. It is also shown that this is the best upper bound one can achieve. Finally, we survey applications of Hanf normal forms in finite model theory (in particular, parametrized complexity theory) and automata theory over graphs and partial orders. This is joint work with Dietrich Kuske, which appeared in Journal of Applied Logic 10:179-186, 2012. |
| Orateur | Pierre Bourhis (Oxford University, ) |
| Date | Mardi 16 avril 2013 |
| Salle | salle 178 |
| Titre | Recursive queries on trees and data trees |
| Résumé | The analysis of datalog programs over relational structures has been studied in depth, most notably the problem of containment. The analysis problems that have been considered were shown to be undecidable with the exception of (i) containment of arbitrary programs in nonrecursive ones, (ii) containment of monadic programs, and (iii) emptiness. In this paper, we are concerned with a much less studied problem, the analysis of datalog programs over data trees. We show that the analysis of datalog programs is more complex for data trees than for arbitrary structures. In particular, we prove that the three aforementioned problems are undecidable for data trees. But in practice, data trees (e.g., XML trees) are often of bounded depth. We prove that all three problems are decidable over bounded depth data trees. Another contribution of the paper is the study of a new form of automata called pattern automata, that are essentially equivalent to linear datalog programs. We use pattern automata to show that the emptiness problem for linear monadic datalog programs with data value inequalities is decidable over arbitrary data trees. |
| Orateur | Howard Straubing (Boston College, ) |
| Date | Mardi 9 avril 2013 |
| Salle | salle 76 |
| Titre | Quantifier Alternation in Two-variable Logic |
| Résumé | It has long been known that every first-order formula over the base < is equivalent to one in which there are only three bound variables. The class of regular languages definable by formulas using only two variables turned out to be unexpectedly interesting, with a succinct nontrivial algebraic description and many striking equivalent characterizations. Here we briefly review these results (due largely to Thérien and Wilke) and present recent work giving an effective algebraic description of the levels of the quantifier alternation hierarchy in two-variable logic. This is joint work with Andreas Krebs of the University of Tübingen. (Based on Straubing, CSL 2011 and Krebs and Straubing, FSTTCS 2012. Another approach, yielding a quite different algebraic description of the same hierarchy, is in Kufleitner and Weil, CSL 2012). |
| Orateur | David Janin (LaBRI, ) |
| Date | Mardi 26 mars 2013 |
| Salle | salle 76 |
| Titre | Algebras, automata and logic for languages of labeled birooted trees |
| Résumé | We study languages of labeled finite birooted trees: Munn’s birooted trees extended with vertex labeling. We define a notion of finite state birooted tree automata that is shown to capture the class of languages that are upward closed w.r.t. the natural order and definable in Monadic Second Order Logic. Then, relying on the inverse monoid structure of labeled birooted trees, we derive a notion of recognizable languages by means of (adequate) premorphisms into finite (adequately) ordered monoids. This notion is shown to capture finite boolean combinations of languages as above. As a particular case, a simple encoding of finite (mono-rooted) labeled trees in an antichain of labeled birooted trees shows that classical regular languages of finite (mono-rooted) trees are also recognized by such premorphisms and finite ordered monoids. |
| Orateur | Allyx Fontaine (LaBRI, ) |
| Date | Mardi 19 mars 2013 |
| Salle | salle 178 |
| Titre | A Formal Analysis in Coq of a Handshake Randomised Distributed Algorithm |
| Résumé | Under some hypothesis on the distributed system, there is no deterministic solution of certain classical problems, as the handshake problem. Randomised solutions are then needed to solve those problems. We present a formalisation in Coq of a distributed randomised algorithm that solves this problem. This allows us to formally prove properties of this algorithm such as termination and probabilistic results. |
| Orateur | Benoît Groz (Tel Aviv University, ) |
| Date | Mardi 5 mars 2013 |
| Salle | salle 76 |
| Titre | Deterministic regular expressions |
| Résumé | Deterministic regular expressions appear in many schema languages for XML (DTDs, XML Schemas) to define the possible content of an element. We prove that one can determine in linear time whether a given expression is deterministic. We also present algorithms to decide in linear time if a given word is accepted by an expression, for large families of deterministic regular expressions. Our algorithms build datastructures on the expression's parse tree, whereas classical algorithms for those problems rely on the Glushkov automaton which may have quadratic size when the size of the alphabet is not bounded. |
| Orateur | Etienne Lozes (LSV, ) |
| Date | Mardi 26 février 2013 |
| Salle | salle 76 |
| Titre | The expressivity of Separation Logic : a survey |
| Résumé | Separation logic is a program logic à la Hoare that was introduced by Reynolds and O'Hearn at the end of the 90s. Proving a program goes through writing valid Hoare triples {Pre} p {Post}, where Pre, Post are logical assertions and p is a program. The main novelty of separation logic with respect to Hoare logic is that the assertion language introduces two new logical connectives, the separating conjunction and the magic wand, and exploits them in some inference rules for Hoare triples. In the context of heap-manipulating programs, the assertion language can be seen as a special case of the spatial logic for graphs, where a graph property "A and separately B" means that the set of edges of the graph can be partitioned in two subsets such that the two resulting subgraphs satisfy A and B respectively. In this talk, after briefly reviewing the context of separation logic, I will compare separation logic and its fragments with weak second order and weak monadic second order logic. Separation logic will be shown to be equivalent to second order logic. It will also be shown that the magic wand subsumes the separating conjunction, in the sense that there is a logspace elimination procedure for separating conjunction (joint work with Remi Brochenin and Stephane Demri). I will also report about a result due to Dawar and Antonopoulos that states that Separation logic without magic wand is strictly less expressive than monadic second order logic. |
| Orateur | Frédéric Servais (University of Hasselt, ) |
| Date | Mardi 19 février 2013 |
| Salle | salle 76 |
| Titre | From Two-Way to One-Way Finite State Transducers |
| Résumé | Any two-way finite state automaton is equivalent to some one-way finite state automaton. This well-known result, shown by Rabin and Scott and independently by Shepherdson, states that two-way finite state automata (even non-deterministic) characterize the class of regular languages. It is also known that this result does not extend to finite string transductions: (deterministic) two-way finite state transducers strictly extend the expressive power of (functional) one-way transducers. In particular deterministic two-way transducers capture exactly the class of MSO-transductions of finite strings. In this talk, I will address the following definability problem: given a function defined by a two-way finite state transducer, is it definable by a one-way finite state transducer? By extending Rabin and Scott's proof to transductions, we show that this problem is decidable. Our procedure builds a one-way transducer, which is equivalent to the two-way transducer, whenever one exists. This is a joint work with Emmanuel Filiot, Olivier Gauwin and Pierre-Alain Reynier. |
| Orateur | Rémy Chrétien (LSV, ) |
| Date | Mardi 15 janvier 2013 |
| Salle | salle 76 |
| Titre | Trace equivalence of protocols for an unbounded number of sessions |
| Résumé | Secure design of communication protocols in order to ensure the authentication of electronic agents or the safety of secret data is known to be difficult and fairly error-prone. Symbolic frameworks such as the Dolev-Yao model and later various process algebra have proven themselves valuable for finding attacks and assessing the security of these protocols. Several tools have thus been developed to answer the need of automated verification: ProVerif, AVISPA and Scyther rely on various formal methods to prove that a range of security properties holds in protocols. The problem of deciding reachability for cryptographic protocols has been thoroughly studied for an unbounded number of sessions and proven to be undecidable in general. Nevertheless some fragments were shown to be decidable, either by tagging or by restricting the number of blind-copies. On the other hand, trace equivalence has only been proven to be decidable for a bounded number of sessions. The objective of this talk is to provide the first results of decidability of trace equivalence for an unbounded number of sessions. Trace equivalence for a first class of protocols was shown undecidable under scarce restrictions one variable and symmetric encryption are indeed enough. Consequently, we restrained our class of protocols a step further by making the protocols deterministic in some sense and preventing it from disclosing secret keys. This tighter class of protocols was then shown to be decidable after reduction to an equivalence between deterministic pushdown automata. |
| Orateur | Sylvain Salvati (INRIA, ) |
| Date | Mardi 18 décembre 2012 |
| Salle | salle 76 |
| Titre | The IO and OI hierarchies revisited (2) |
| Résumé | I will pursue the presentation of about the IO and OI hierarchies by presenting the decidability results for the emptiness and the membership problems. The techniques I will use are mostly based on denotational semantics of lambda-calculus. If time permits, I will detail the proof of the generalized version of Statman's finite completeness Theorem that is at the core of the decidability of membership. This is joint work with Gregory M. Kobele. |
| Orateur | Sylvain Salvati (INRIA, ) |
| Date | Mardi 4 décembre 2012 |
| Salle | salle 76 |
| Titre | The IO and OI hierarchies revisited (1) |
| Résumé | The IO and OI hierarchies of languages have been introduced by Damm in his article of 1982. The idea was to use higher-order computation as a means of defining languages. Damm latter showed that the OI hierarchy, as he defined it, coincides with higher-order pushdown automata. At the turn of the century, Knapick et al. showed that higher-order pushdown automata were making a restriction, called "safety", on higher-order computation. Parys has showed that the use of safety restricts what counts as a deterministic language and it is in general believed that it restricts the class of definable languages. In this talk, we shall redefine IO and OI hierarchy in terms of non-deterministic lambda-calculus with fixpoint. In doing so, we will allow the definition of languages of strings, of trees and of lambda-terms. Using a classical technique from the lambda-calculus, we will see that OI subsumes IO. Afterwards, using finite denotational models of the lambda-calculus, we will see various decidability results for these hierarchy such as emptiness and membership. For the membership problem in OI, the decidability result is based on a generalization of Statman finite completeness Theorem. This is joint work with Gregory M. Kobele. |
| Orateur | Pedro Silva (University of Porto, ) |
| Date | Mardi 20 novembre 2012 |
| Salle | salle 76 |
| Titre | NOUVELLES NOTIONS DE RANG ET INDÉPENDANCE POUR GRAPHES FINIS |
| Résumé | L'année dernière, Izakhian et Rhodes ont développé une théorie de représentation de matroïdes par des matrices booléennes où tous les matroïdes deviennent représentables, au contraire de ce qui se passe avec les représentations classiques sur des corps. Dans un travail de collaboration avec John Rhodes, on développe une théorie analogue pour les graphes finis, menant à de nouvelles notions de rang et d'indépendance de sommets. Ces notions admettent une caractérisation alternative purement combinatoire et sont la base de quelques résultats inespérés. |
| Orateur | Sylvain Lombardy (LaBRI, ) |
| Date | Mardi 13 novembre 2012 |
| Salle | salle 76 |
| Titre | Automates avec multiplicité et epsilon-transitions |
| Résumé | Les epsilon-transitions apparaissent naturellement dans les automates lors de certains algorithmes de conversion d'expressions rationnelles, ou lorsque l'on manipule des transducteurs. La présence d'epsilon-transitions peut conduire un même mot à être accepté par un nombre infini de calculs, ce qui posent des problèmes dans le cadre des automates avec multiplicité. Nous verrons comment les définitions habituelles du comportement de tels automates peuvent être mises en défaut et comment définir la validité d'un tel automate de façon à avoir une définition stable, décidable et qui permette la suppression des epsilon-transitions quel que soit le type de multiplicité avec lequel on travaille. |
| Orateur | Denis Kuperberg (LIAFA, ) |
| Date | Mardi 23 octobre 2012 |
| Salle | salle 76 |
| Titre | La théorie des fonctions de coût régulières |
| Résumé | La théorie des fonctions de coûts régulières permet d'étendre quantitativement celle des langages réguliers, et présente plusieurs avantages. Premièrement, les caractérisations en termes d'automates, de monoides ou de logique (MSO,FO,LTL), s'étendent bien dans le cadre des fonctions de coût, et on peut obtenir des généralisations des théorèmes de caractérisation à la Schutzenberger, ainsi que de nouveaux théorèmes propres aux fonctions de coût. Deuxièmement, cette nouvelle théorie permet d'obtenir des résultats difficiles de décidabilité dans la théorie classique des langages réguliers, comme celui du problème de la hauteur d'étoile (qui est à l'origine du développement de cette théorie). On présentera le modèle des fonctions de coût, et on montrera comment les notions classiques sur les langages réguliers (comme celle de monoide syntactique) se généralisent à ce cadre quantitatif. |
| Orateur | Colin Riba (LIP, ENS Lyon, ) |
| Date | Mardi 16 octobre 2012 |
| Salle | salle 76 |
| Titre | A Model Theoretic Proof of Completeness of an Axiomatization of Monadic Second-Order Logic on Infinite Words |
| Résumé | We discuss the completeness of an axiomatization of Monadic Second-Order Logic (MSO) on infinite words (or streams). By using model-theoretic tools, we give an alternative proof of D. Siefkes' result that a fragment with full comprehension and induction of second-order Peano's arithmetic is complete w.r.t. the validity of MSO-formulas on streams. We rely on Feferman-Vaught Theorems and the Ehrenfeucht-Fraïssé method for Henkin models of second-order arithmetic. Our main technical contribution is an infinitary Feferman-Vaught Fusion of such models. We show it using Ramseyan factorizations similar to those for standard infinite words. We also discuss a Ramsey's theorem for MSO-definable colorings, and show that in linearly ordered Henkin models, Ramsey's theorem for additive MSO-definable colorings implies Ramsey's theorem for all MSO-definable colorings. |
| Orateur | David Janin (LaBRI, ) |
| Date | Mardi 9 octobre 2012 |
| Salle | salle 76 |
| Titre | Walking in the free inverse monoid (continued) |
| Résumé | Talk of the previous week, continued. |
| Orateur | David Janin (LaBRI, ) |
| Date | Mardi 2 octobre 2012 |
| Salle | salle 76 |
| Titre | Walking in the free inverse monoid |
| Résumé | We consider subsets of the free inverse monoid or, following Munn's representation theorem, languages of finite birooted trees. We propose three notions of definability for these languages: definability by means of finite state walking automata with nested (invisible) pebbles, definability by means of (extension of) Kleene regular expressions, and definability by means of (adequate) premorphisms (or relational morphisms) in (adequate) finite ordered monoids. Various correspondences, linking these three notions together, are shown to hold. Finite walking automata with a finite number of pebbles are shown to be captured by regular expressions; the number of allowed pebbles corresponds to the nesting depth of a projection operator onto languages of idempotent birooted trees. Finite walking automata with a finite or an infinite number of pebbles are also shown to be captured by finitely generated premorphisms from the (naturally ordered) free inverse monoid in their associated (finite) transition monoids (ordered by inclusion). These results strengthen the idea that the category of (quasi-inverse) ordered monoids and (appropriate) premorphisms is an adequate framework for the study of walking automata on trees much in the same way the category of monoids and morphisms is an adequate framework for the study of classic (one way) automata. Moreover, since our algebraic characterization of walking automata holds even for automata using infinitely many pebbles, it also provides a presumably new algebraic framework for the study of regular languages of finite trees. This work extend a similar work on languages of one-dimensional tiles (linear unidirectional birooted trees) recently done with Anne Dicky. |
| Orateur | Sean Cleary (City College of New York, ) |
| Date | Mardi 18 septembre 2012 |
| Salle | salle 178 |
| Titre | Complexity of languages of geodesics |
| Résumé | We address questions about recognizing geodesics in groups with simple automata, and consider both full languages of all geodesics from the identity and languages of unique normal form geodesics from the identity. We describe languages of geodesics which can be recognized by simple automata- finite state automata, pushdown automata and counter automata, and give some criteria which rule out the ability of some automata to recognize certain geodesic languages. The examples include wreath products examples and Thompson's group F, and we show that the linguistic complexity of languages of geodesics can depend upon choice of generating set. This is joint work with Jennifer Taback and Murray Elder. |