Links' Seminars and Public Events |
2024 | |
---|---|
Wed 20th Nov 11:00 am 12:00 pm | Seminar by Bastien Degardins Speaker: Bastien Degardins Room: Amphi Atrium (RdC Bâtiment ESPRIT) Title: Visualization and queries for biology in de Bruijn Graphs using relational databases. Abstract: Since the emergence of modern sequencers, sequence bioinformatics has become crucial for processing sequencing data, essential in medicine, biology, archaeology, and beyond. However, the growing data volumes require software adaptations to meet these new challenges, despite significant hardware advancements. Vizitig is a genomic and transcriptomic data visualization software based on De Bruijn graphs, offering an intuitive query system without needing to load indexes into RAM, allowing direct work on disk. By leveraging relational databases, which are highly optimized and backed by decades of research, Vizitig opens new avenues for research.It relies on NetworkDisk, a Python package that manages graphs in a relational database, simplifying software engineering. With a domain-specific language (DSL), Vizitig enables intuitive queries and easy manipulation of graph metadata, even for non-technical users. For experts, its compatibility with NetworkX provides additional possibilities in terms of graph manipulation. |
Fri 15th Nov 11:00 am 12:15 pm | Seminar by Gabriel Bathie Speaker: Gabriel Bathie (perso.ens-lyon.fr/gabriel.bathie/) Room: B21 Title: The complexity of Testing Regular Languages - Gabriel Bathie, Corto Mascle and Nathanaël Fijalkow (LaBRI, Université de Bordeaux) Abstract: Property testing is concerned with the design of algorithms making sublinear number of queries to distinguish whether the input satisfies a given property or is far from having this property. A seminal paper of Alon, Krivelevich, Newman, and Szegedy in 2001 introduced property testing of formal languages: the goal is to determine whether an input word belongs to a given language, or is far from any word in that language (in terms of Hamming distance). They constructed the first property testing algorithm for the class of all regular languages. Somewhat surprisingly, their algorithm uses a number of queries that does not depend on the length of the input word. This opened up a line of work with improved complexity results and applications to streaming algorithms. In this work, we show a trichotomy result: the class of regular languages can be divided into three classes, each of which is associated with an optimal testing complexity. Our analysis yields effective characterizations for all three classes using so-called minimal blocking sequences, reasoning directly and combinatorially on automata. This talk will give an overview of the methods used since the work of Alon et al. and highlight the main tools used for our combinatorial characterization. Based on joint work with Corto Mascle and Nathanaël Fijalkow. "Lille-Salle B21" |
Tue 12th Nov 2:00 pm 3:30 pm | Seminar from Aliaume Lopez Speaker: Aliaume Lopez (www.lsv.fr/~lopez/) Title: Which polynomials are computed by N-weighted automata? Room: B21 Abstract: Given a semiring K, the notion of K-weighted automata generalizes regular languages to functions from Σ* to K. This model allows us to compute (multivariate) polynomial functions with coefficients in K. We provide a decidable characterization of polynomials with coefficients in Q that can be computed by K-weighted automata for K = (N,+,×) and for K = (Z+,×). As a consequence, we can decide which functions computed by Z-weighted automata are computed by N-weighted automata, under the assumption of commutativity (the order of the letters in the input does not matter) and polynomial growth (the output of the function is bounded by a polynomial in the size of the input). This surprisingly allows us to decide whether such functions are star-free, a notion borrowed from the theory of regular languages. "Lille-Salle B21" |
Fri 11th Oct 10:30 am 12:00 pm | Seminar from Alexis de Colnet Speaker: Alexis de Colnet (www.ac.tuwien.ac.at/people/decolnet/) Title: An FPRAS for #NFA and #nFBDD Abstract: #NFA is the problem of counting the words of a given length accepted by a non-deterministic finite automaton (NFA). The problem is #P-hard but the approximate variant admits polynomial-time randomized algorithms (FPRAS, or fully-polynomial time randomized approximation schemes). Arenas, Croquevielle, Jayaram and Riveros were the first to show that #NFA admits an FPRAS and that this result extends to several other counting problems, in fact all problems in the class SpanL. In this talk we present another FPRAS for #NFA which applies to problems not covered by Arenas et al.'s result. In particular, the FPRAS described in this talk can be used for the problem of counting the satisfying assignments of non-deterministic read-once branching programs (nFBDD). Atrium bâtiment Esprit |
Fri 7th Jun 10:00 am 11:00 am | Séminaire Sam Van Gool dualité de Stone |
Thu 30th May to Fri 31st May all day | Pysemigroup Hackaton |
Fri 24th May 11:00 am 11:30 am | Séminaire Sophie Tison Speaker: Sophie Tison Title: Containment of Regular Path Queries Under Constraints |
Thu 16th May 2:00 pm 4:00 pm | Seminar Arkaprava Title: Efficient Optimization of Network Metrics in Large Uncertain Graphs Abstract: Graphs constitute an omnipresent data structure that can model objects and their relationships in a wide variety of real-world scenarios. The optimization of network metrics finds use in a plethora of real-world applications. Most of the exact techniques for such tasks turn out to be prohibitively time-consuming and memory-intensive for the huge graphs that are usually encountered. Thus, there is a need for efficient approximation algorithms. This talk focuses on the efficient optimization of network metrics in large uncertain graphs, and specifically the following three research problems. The first problem aims to find, between a given pair of nodes in an uncertain graph, the path having the highest probability of being a shortest path. The second problem aims to find, in an uncertain graph, the subgraph having the highest probability of being densest. The third problem is a novel variant of the well-known opinion maximization problem where, given a social network of users with real-valued opinions (about different candidates), the goal is to choose the top-k seed users maximizing a specific voting-based score at a given finite time horizon. Best Regards, Arkaprava "Lieu : Lille, Salle : B11" |
Fri 19th Apr 11:00 am 12:00 pm | Seminar Pierre Lermusiaux Speaker: Pierre Lermusiaux (plermusi.github.io/) Title: Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation Abstract: Exception handling is a key feature in modern programming languages. Exceptions can be used to deal with errors, or as a means to control the flow of execution of a program. Since they might unexpectedly terminate a program, unhandled exceptions are a serious safety concern. We propose a static analysis to detect uncaught exceptions in functional programs, that is defined as an abstract interpreter. It computes a description of the values potentially returned by a program using a novel abstract domain, that can express inductively defined sets of values. Simultaneously, the analysis infers the possibly raised exceptions, by computing in the abstract exception monad. This abstract interpreter has been implemented as an effective static analyser for a large subset of OCaml programs, that supports mutable data types, the OCaml module system, and dynamically extensible data types such as the exception type. The analyser has been evaluated on several hundreds of OCaml programs. |
Fri 5th Apr 10:30 am 11:30 am | Séminaire Guillaume Lagarde Titre: Scaling Neural Program Synthesis with Distribution-based Search Abstract: In this talk, we will discuss the problem of automatically constructing computer programs from input-output examples, especially when the target language is domain-specific and defined using a context-free grammar. I will introduce a theoretical framework called distribution-based search, discuss its challenges, and present several search strategies based on learning the weights of a probabilistic context-free grammar (PCFG) and then using this PCFG to enumerate the most promising candidate programs efficiently. The presentation will be based on the following paper published at AAAI'2022: arxiv.org/abs/2110.12485 Joint work with Nathanaël Fijalkow, Théo Matricon, Kevin Ellis, Pierre Ohlmann, Akarsh Potta |
Fri 2nd Feb 10:30 am 11:30 am | Mikaël Monet: Probabiliste Shapley value |
Fri 26th Jan 10:00 am 11:00 am | Séminaire: Klara Nosan Sujet: TBA |
2023 | |
Thu 14th Dec 2:00 pm 5:00 pm | Claire Soyez-Martin PhD defense Amphi IRCICA |
Fri 1st Dec 10:00 am 11:00 am | Séminaire Oliver Titre: Direct Access for Conjunctive Queries with Negation Abstract: Direct Access is the operation of returning, given an index j, the jth answer of a conjunctive query on a given database for a given order. While this problem is #P-hard in general (wrt combined complexity), many conjunctive queries are structured enough so that for some lexicographical ordering of their answers, one can have a direct access to the answer set of a query Q that takes polylogarithmic time in the size of the database after a polynomial time precomputation. Previous work has precisely characterised the tractable classes and given fined-grained lower bounds on the time needed for precomputation depending on the structure of the query. We give a generalisation of these tractability results to the case of signed conjunctive queries, that is, conjunctive queries that may contain negative atoms. Our technique is based on solving the direct access task for a class of circuits that can represent relational data. Our result then follows from the fact that the tractable (signed) conjunctive queries can be transformed into polynomial size circuits. We recover the known tractable classes from the literature in the case of positive conjunctive queries using this technique and also discover new islands of tractability for signed conjunctive queries. In particular, our result generalises to the Direct Access Problem the known tractabilities of counting the number of answers to beta-acyclic negative queries and of deciding whether a negative query with bounded nested-width has an answer. This is joint work with Florent Capelli. |
Fri 24th Nov 10:00 am 11:00 am | Séminaire Pierre Vandenhove |
Fri 17th Nov 10:00 am 11:00 am | Séminaire Charles (RsonPath) TBA |
Fri 10th Nov 10:00 am 11:00 am | Séminaire Nils Vortmeier title: TBA |
Fri 20th Oct 10:30 am 12:30 pm | Aurelien part II |
Fri 22nd Sep 11:00 am 12:00 pm | Séminaire Théo Losekoot Title: Automata-based verification of relational properties of functions over algebraic data structures |
Fri 15th Sep 11:00 am 12:30 pm | Charles: Présentation de rsonpath |
Fri 23rd Jun 11:00 am 12:00 pm | Seminar by Florent Capelli Speaker: Florent Capelli — florent.capelli.me/ Title: A simpler FPRAS for nOBDD Abstract: A simpler FPRAS for nOBDD Abstract: In this talk, we revisit the algorithm by Arenas, Croquevielle, Jayaram and Riveros that allows to approximate the number of words of length n of a non deterministic finite automaton. We explain the algorithm and techniques in a modular and general way, without relating to the particular case of counting words in automaton. We illustrate the soundness of the approach by applying it to the problem of approximatively counting the number of satisfying assignments of a non-deterministic OBDD. B21 |
Fri 2nd Jun 11:00 am 12:30 pm | Séminaire Martin Berger Title: Search-Based Regular Expression Inference on a GPU Abstract: Regular expression inference (REI) is a supervised machine learning and program synthesis problem that takes a cost metric for regular expressions, and positive and negative examples of strings as input. It outputs a regular expression that is precise (i.e., accepts all positive and rejects all negative examples), and minimal w.r.t. to the cost metric. We present a novel algorithm for REI over arbitrary alphabets that is enumerative and trades off time for space. Our main algorithmic idea is to implement the search space of regular expressions succinctly as a contiguous matrix of bitvectors. Collectively, the bitvectors represent, as characteristic sequences, all sub-languages of the infix-closure of the union of positive and negative examples. Mathematically, this is a semiring of (a variant of) formal power series. Infix-closure enables bottom-up compositional construction of larger from smaller regular expressions using the operations of our semiring. This minimises data movement and data-dependent branching, hence maximises data-parallelism. In addition, the infix-closure remains unchanged during the search, hence search can be staged: first pre-compute various expensive operations, and then run the compute intensive search process. We provide two C++ implementations, one for general purpose CPUs and one for Nvidia GPUs (using CUDA). We benchmark both on Google Colab Pro: the GPU implementation is on average over 1000x faster than the CPU implementation on the hardest benchmarks. Joint work with Mojtaba Valizadeh Download: martinfriedrichberger.net/pldi2023.html |
Thu 13th Apr 11:00 am 12:00 pm | Séminaire Yann Strozecki Esprit salle Agora 2 (rez-de-chaussée) |
Tue 11th Apr 2:00 pm 3:00 pm | Séminaire Mamadou Esprit Agora 1 (rez-de-chaussée) |
Fri 24th Mar 10:00 am 11:00 am | Séminaire Mamadou KANTE |
Fri 20th Jan 11:00 am 12:00 pm | Seminar by Tito Speaker: Lê Thành Dũng Nguyễn, aka “Tito” — nguyentito.eu/ Title: Polyregular functions: some recent developments Abstract: The class of polyregular functions is composed of the string-to-string functions computed by pebble transducers. While this machine model (which extends two-way finite transducers) is two decades old, several alternative characterizations of polyregular functions have been discovered recently [Bojańczyk 2018; Bojańczyk, Kiefer & Lhote 2019], demonstrating their canonicity. The name comes from the polynomial bound on the growth rate of these functions: |f(w)| = |w|^O(1) where |w| is the length of the string w. In this talk, after recalling this context, I will present some subsequent developments in which I have been involved: * the subclass of comparison-free polyregular (or “polyblind”) functions, definable through a natural restriction of pebble transducers, which Pierre Pradic and I actually discovered while studying a linear λ-calculus; * some results that either relate the growth rate of a polyregular function (comparison-free or not) to the “resources” needed to compute it, or show that there is no such relationship. |
Fri 13th Jan 11:00 am 12:00 pm | Seminar by Sarah Winter Speaker: Sarah Winter — sarahwinter.net/ Title: A Regular and Complete Notion of Delay for Streaming String Transducers Abstract: The notion of delay between finite transducers is a core element of numerous fundamental results of transducer theory. The goal of this work is to provide a similar notion for more complex abstract machines: we introduce a new notion of delay tailored to measure the similarity between streaming string transducers (SST). We show that our notion is regular: we design a finite automaton that can check whether the delay between any two SSTs executions is smaller than some given bound. As a consequence, our notion enjoys good decidability properties: in particular, while equivalence between non-deterministic SSTs is undecidable, we show that equivalence up to fixed delay is decidable. Moreover, we show that our notion has good completeness properties: we prove that two SSTs are equivalent if and only if they are equivalent up to some (computable) bounded delay. Together with the regularity of our delay notion, it provides an alternative proof that SSTs equivalence is decidable. Finally, the definition of our delay notion is machine-independent, as it only depends on the origin semantics of SSTs. As a corollary, the completeness result also holds for equivalent machine models such as deterministic two-way transducers, or MSO transducers. This is joint work with Emmanuel Filiot, Ismaël Jecker, and Christof Löding. |
2022 | |
Fri 16th Dec 11:00 am 12:00 pm | Seminar by Sandra Kiefer CANCELLED: we will attempt to reschedule this seminar to early 2023. Speaker: Sandra Kiefer — www.lics.rwth-aachen.d.....dx/1/ Title: TBA Abstract: TBA |
Fri 9th Dec 11:00 am 12:00 pm | Seminar by Rémi Morvan Speaker: Rémi Morvan — www.morvan.xyz/ Titre: Approximation and Semantic Tree-width of Conjunctive Regular Path Queries Abstract: We show that the problem of whether a query is equivalent to a query of tree-width k is decidable, for the class of Unions of Conjunctive Regular Path Queries with two-way navigation (UC2RPQs). A previous result by Barceló, Romero, and Vardi has shown decidability for the case k=1, and here we show that decidability in fact holds for any arbitrary k>1. The algorithm is in 2ExpSpace, but we show that the complexity drops to the second level of the polynomial hierarchy for a restricted but practically relevant case of queries obtained by only allowing simple regular expressions. We also investigate the related problem of approximating a UC2RPQ by queries of small tree-width. We exhibit an algorithm which, for any fixed number k, builds the maximal under-approximation of tree-width k of a UC2RPQ. The maximal under-approximation of tree-width k of a query q is a query q' of tree-width k which is contained in q in a maximal and unique way, that is, such that for every query q'' of tree-width k, if q'' is contained in q then q'' is also contained in q'. Joint work with Diego Figueira. |
Fri 18th Nov 11:00 am 11:30 am | Seminar by Sarah Winter CANCELLED for COVID: we will attempt to reschedule this seminar to early 2023 Speaker: Sarah Winter — sarahwinter.net/ Title: A Regular and Complete Notion of Delay for Streaming String Transducers Abstract: The notion of delay between finite transducers is a core element of numerous fundamental results of transducer theory. The goal of this work is to provide a similar notion for more complex abstract machines: we introduce a new notion of delay tailored to measure the similarity between streaming string transducers (SST). We show that our notion is regular: we design a finite automaton that can check whether the delay between any two SSTs executions is smaller than some given bound. As a consequence, our notion enjoys good decidability properties: in particular, while equivalence between non-deterministic SSTs is undecidable, we show that equivalence up to fixed delay is decidable. Moreover, we show that our notion has good completeness properties: we prove that two SSTs are equivalent if and only if they are equivalent up to some (computable) bounded delay. Together with the regularity of our delay notion, it provides an alternative proof that SSTs equivalence is decidable. Finally, the definition of our delay notion is machine-independent, as it only depends on the origin semantics of SSTs. As a corollary, the completeness result also holds for equivalent machine models such as deterministic two-way transducers, or MSO transducers. This is joint work with Emmanuel Filiot, Ismaël Jecker, and Christof Löding. |
Fri 21st Oct 11:00 am 12:00 pm | Online seminar by Pierre Pradic Speaker: Pierre Pradic — perso.ens-lyon.fr/pierre.pradic/ Title: Synthesizing Nested Relational Queries from Implicit Specifications Abstract: Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset O in terms of datasets I⃗ ) is a logical specification involving the source data I⃗ and the interface data O. It is a valid definition of O in terms of I⃗ , if any two models of the specification agreeing on I⃗ agree on O. In contrast, an explicit definition is a query that produces O from I⃗ . Variants of Beth's theorem state that one can convert implicit definitions to explicit ones. Further, this conversion can be done effectively given a proof witnessing implicit definability in a suitable proof system. In this talk, I will discuss an analogous effective implicit-to-explicit result for nested relations: implicit definitions, given in the natural logic for nested relations, can be effectively converted to explicit definitions in the nested relational calculus NRC. I will first spend some time explaining what NRC is and what logic we use to describe implicit definitions of nested queries. Then I will present the results obtained in our papers, attempt to give some intuitions on the proof of the main theorem and say a few words on in particular the proof-theoretic techniques and concerns that come up (namely, cut-elimination and focussing) and how this can impact the complexity of extracting explicit definitions from proofs of implicit definability. Then if time allows I will discuss a more general model-theoretic result that we first used to give a non-constructive proof of our theorem, and some ideas that we have towards making it constructive and bounding the complexity of extracting explicit definitions. This is Joint work with Michael Benedikt and Christoph Wenhard. The main results I will be discussing were written up in arxiv.org/abs/2005.06503 and arxiv.org/abs/2209.08299. Online |
Fri 30th Sep 10:00 am 11:30 am | Seminar by Liat Peterfreund Speaker: Liat Peterfreund — sites.google.com/view/liatpeterfreund/ Title: Querying Incomplete Numerical Data: Between Certain and Possible Answers Abstract: Queries with aggregation and arithmetic operations, as well as incomplete data, are common in real-world databases, but we lack a good understanding of how they should interact. On the one hand, systems based on SQL provide ad-hoc rules for numerical nulls, on the other, theoretical research largely concentrates on the standard notions of certain and possible answers which in the presence of numerical attributes and aggregates are often meaningless. In this work, we define a principled compositional framework for databases with numerical nulls and answering queries with arithmetic and aggregations over them. We assume that missing values are given by probability distributions associated with marked nulls, which yields a model of probabilistic bag databases. We concentrate on queries that resemble standard SQL with arithmetic and aggregation and show that they are measurable, and that their outputs have a finite representation. Moreover, since the classical forms of answers provide little information in the numerical setting, we look at the probability that numerical values in output tuples belong to specific intervals. Even though their exact computation is intractable, we show efficient approximation algorithms to compute such probabilities. The talk is based on joint work with Marco Console and Leonid Libkin, and will be presented in PODS 2023. |
Fri 16th Sep 11:00 am 12:00 pm | Seminar Luis Galárraga Speaker : Luis Galárraga — luisgalarraga.de/about/ Title: Computing How-Provenance for SPARQL Queries via Query Rewriting Abstract: Over the past few years, we have witnessed the emergence of large knowledge graphs built by extracting and combining information from multiple sources. This has propelled many advances in query processing over knowledge graphs, however the aspect of providing provenance explanations for query results has so far been mostly neglected. In this talk I will present SPARQLprov, a method based on query rewriting, to compute how-provenance polynomials for SPARQL queries over knowledge graphs. Contrary to existing works, SPARQLprov is system-agnostic and can be applied to standard and already deployed SPARQL engines without the need of customized extensions. To do so, we rely on spm-semirings to compute polynomial annotations that respect the property of commutation with homomorphisms on monotonic and non-monotonic SPARQL queries without aggregate functions. An evaluation on real and synthetic data shows that SPARQLprov over standard engines competes with state-of-the-art solutions for how-provenance computation, while covering a larger fragment of the query language. |
Fri 1st Jul 11:00 am 12:00 pm | Séminaire Arnaud Durand |
Fri 10th Jun 10:00 am 11:00 am | Séminaire Corentin Barloy Title:The Regular Languages of First-Order Logic with One Alternation Abstract: The regular languages with a neutral letter expressible in first-order logic with one alternation are characterized. Specifically, it is shown that if an arbitrary Σ2 formula defines a regular language with a neutral letter, then there is an equivalent Σ2 formula that only uses the order predicate. This shows that the so-called Central Conjecture of Straubing holds for Σ2 over languages with a neutral letter, the first progress on the Conjecture in more than 20 years. To show the characterization, lower bounds against polynomial-size depth-3 Boolean circuits with constant top fan-in are developed. The heart of the combinatorial argument resides in studying how positions within a language are determined from one another, a technique of independent interest. |
Fri 25th Feb 11:00 am 12:00 pm | Séminaire Nico |
Fri 28th Jan 11:00 am 12:00 pm | Alexandre Vigny (visio) Title: Separator logic, expressive power and algorithmic applications Abstract: First-order logic (FO) can express many algorithmic problems on graphs, but fails to express whether two vertices are connected. We define a new logic (separator logic) by enriching FO with connectivity predicates connk(x, y, z1, . . . , zk) that hold true in a graph if there exists a path between x and y after deletion of z1, . . . , zk. In this talk I will first present a study of the expressive power of this new logic. I will then present algorithmic results for this logic on graph classes that exclude a topological minor. These results were obtained in collaboration with Michał Pilipczuk, Nicole Schirrmacher, Sebastian Siebertz, and Szymon Toruńczyk. |
Fri 21st Jan 11:00 am 12:00 pm | Aurélien Lemay in Seminar |
2021 | |
Fri 10th Dec 11:00 am 12:00 pm | Séminaire Sebastien Tavenas Title: Bornes inférieures superpolynomiales pour les circuits de profondeur constante Abstract: Tout polynôme multivarié P(X_1,...,X_n) peut être écrit comme une somme de monômes, i.e., une somme de produits de variables et de constantes du corps. La taille naturelle d'une telle expression est le nombre de monômes. Mais, que se passe-t-il si on rajoute un nouveau niveau de complexité en considérant les expressions de la forme : somme de produits de sommes (de variables et de constantes) ? Maintenant, il devient moins clair comment montrer qu'un polynôme donné n'a pas de petite expression. Dans cet exposé nous résoudrons exactement ce problème. Plus précisément, nous prouvons que certains polynômes explicites n'ont pas de représentations "somme de produits de sommes'' (SPS) de taille polynomiale. Nous pouvons aussi obtenir des résultats similaires pour les SPSP, SPSPS, etc... pour toutes les expressions de profondeur constante. " |
Thu 25th Nov 2:00 pm 3:00 pm | Nofar Carmeli in Links' Seminar |
Fri 29th Oct 11:00 am 12:00 pm | Séminaire Antoine Amarilli |
Fri 22nd Oct 11:00 am 12:00 pm | Mikaël Monet in Links' Seminar |
Fri 15th Oct 11:00 am 12:00 pm | Claire Soyez-Martin in Links' seminar |
Fri 17th Sep 11:00 am 12:00 pm | Séminaire Corentin Barloy Title: Stackless Processing of Streamed Trees Abstract: Processing tree-structured data in the streaming model is a chal-lenge: capturing regular properties of streamed trees by means of astack is costly in memory, but falling back to finite-state automata drastically limits the computational power. We propose an intermediate stackless model based on register automata equipped with a single counter, used to maintain the current depth in the tree. We explore the power of this model to validate and query streamed trees. Our main result is an effective characterization of regular path queries (RPQs) that can be evaluated stacklessly—with and without registers. In particular, we confirm the conjectured characterization of tree languages defined by DTDs that are recognizable without registers, by Segoufin and Vianu (2002), in the special case of tree languages defined by means of an RPQ. Link: paperman.name/data/pub.....0.pdf lille-Salle |
Fri 10th Sep 10:00 am 11:00 am | Séminaire de Patrick Baillot titre: Type-based complexity analysis in a parallel process calculus Abstract: Some type systems have been designed to analyse statically the time coplexity of functional languages. A natural question is whether this approach can be extended to parallel languages. We address this problem for the Pi-calculus, a paradigmatic calculus for parallel and concurrent computation. In Pi-calculus, processes communicate through channels that can carry values and channel names. We will define notions of sequential and parallel complexity for Pi-calculus, and present a type system that provides an upper bound on the time complexity of processes. This is based on joint work with Alexis Ghyselen (ESOP 2021). Based on: link.springer.com/chap.....9-3_3 |
Fri 9th Jul all day | Seminar - Antonio AL SERHALI Title: Integrating Schema-Based Cleaning into Automata Determinization Abstract : Schema-based cleaning for automata on trees or nested words was proposed recently to compute smaller deterministic automata for regular path queries on data trees. The idea is to remove all rules and states, from an automaton for the query, that are not needed to recognize any tree recognized by a given schema automaton. Unfortunately, how- ever, deterministic automata for nested words may still grow large for au- tomata for XPath queries, so that the much smaller schema-cleaned ver- sion cannot always be computed in practice. We therefore propose a new schema-based determinization algorithm that integrates schema-based cleaning directly. We prove that schema-based determinization always produces the same deterministic automaton as schema-based cleaning after standard determinization. Nevertheless, the worst-case complex- ity is considerably lower for schema-based determinization. Experiments confirm the relevance of this result in practice. |
Fri 4th Jun 10:00 am 12:30 pm | Séminaire Pierre Ohlmann Zoom link: univ-lille-fr.zoom.us/j/95419000064 Titre: Lower bound for arithmetic circuits via the Hankel matrix Abstract: We study the complexity of representing polynomials by arithmetic circuits in both the commutative and the non-commutative settings. To analyse circuits we count their number of parse trees, which describe the non-associative computations realised by the circuit. In the non-commutative setting a circuit computing a polynomial of degree d has at most 2^{O(d)} parse trees. Previous superpolynomial lower bounds were known for circuits with up to 2^{d^{1/3-ε}} parse trees, for any ε>0. Our main result is to reduce the gap by showing a superpolynomial lower bound for circuits with just a small defect in the exponent for the total number of parse trees, that is 2^{d^{1-ε}}, for any ε>0. In the commutative setting a circuit computing a polynomial of degree d has at most 2^{O(d \\log d)} parse trees. We show a superpolynomial lower bound for circuits with up to 2^{d^{1/3-ε}} parse trees, for any ε>0. When d is polylogarithmic in n, we push this further to up to 2^{d^{1-ε}} parse trees. While these two main results hold in the associative setting, our approach goes through a precise understanding of the more restricted setting where multiplication is not associative, meaning that we distinguish the polynomials (xy)z and yz). Our first and main conceptual result is a characterization result: we show that the size of the smallest circuit computing a given non-associative polynomial is exactly the rank of a matrix constructed from the polynomial and called the Hankel matrix. This result applies to the class of all circuits in both commutative and non-commutative settings, and can be seen as an extension of the seminal result of Nisan giving a similar characterization for non-commutative algebraic branching programs. Our key technical contribution is to provide generic lower bound theorems based on analyzing and decomposing the Hankel matrix, from which we derive the results mentioned above. The study of the Hankel matrix also provides a unifying approach for proving lower bounds for polynomials in the (classical) associative setting. We demonstrate this by giving alternative proofs of recent lower bounds as corollaries of our generic lower bound results. |
Fri 28th May 10:00 am 11:00 am | Seminar Anastasia Dimou Title: Knowledge graph generation and validation |
Fri 21st May 10:00 am 12:00 pm | Seminar Dimitrios Myrisiotis Title : One-Tape Turing Machine and Branching Program Lower Bounds for MCSP Abstract: eccc.weizmann.ac.il/report/2020/103/ Speaker' webpage : dimyrisiotis.github.io/ zoom |
Fri 7th May 10:00 am 12:00 pm | Seminar Nicole Schweikardt Title: Spanner Evaluation over SLP-Compressed Documents Abstract: We consider the problem of evaluating regular spanners over compressed documents, i.e., we wish to solve evaluation tasks directly on the compressed data, without decompression. As compressed forms of the documents we use straight-line programs (SLPs) -- a lossless compression scheme for textual data widely used in different areas of theoretical computer science and particularly well-suited for algorithmics on compressed data. In terms of data complexity, our results are as follows. For a regular spanner M and an SLP S that represents a document D, we can solve the tasks of model checking and of checking non-emptiness in time O(size(S)). Computing the set M(D) of all span-tuples extracted from D can be done in time O(size(S) size(M(D))), and enumeration of M(D) can be done with linear preprocessing O(size(S)) and a delay of O(depth(S)), where depth(S) is the depth of S's derivation tree. Note that size(S) can be exponentially smaller than the document's size |D|; and, due to known balancing results for SLPs, we can always assume that depth(S) = O(log(|D|)) independent of D's compressibility. Hence, our enumeration algorithm has a delay logarithmic in the size of the non- compressed data and a preprocessing time that is at best (i.e., in the case of highly compressible documents) also logarithmic, but at worst still linear. Therefore, in a big-data perspective, our enumeration algorithm for SLP-compressed documents may nevertheless beat the known linear preprocessing and constant delay algorithms for non-compressed documents. [This is joint work with Markus Schmid, to be presented at PODS'21.] Link to the paper: arxiv.org/pdf/2101.10890.pdf for the paper at least Link to the ACM video: TBA |
Fri 30th Apr 10:00 am 12:00 pm | Présentation de NetworkDisk Je présenterais mon projet avec Bruno: NetworkDisk. Abstract and Title: TBA link to the project: TBA |
Fri 9th Apr 10:00 am 12:00 pm | Seminaire Pascal Weil titre: Problèmes algorithmiques en théorie des groupes infinis resumé: Malgré le titre très général, il s'agira uniquement de problèmes concernant les sous-groupes de groupes infinis, et même juste les sous-groupes de groupes libres. Les résultats et méthodes que je présenterai sont issus de près de 40 ans de littérature et sont dûs à un grand nombre d'auteurs. Je commencerai par poser le paysage, y compris pour ceux qui ne savent plus ce qu'est le groupe libre -- où l'on verra qu'on est, du point de vue algorithmique, dans une variante de la combinatoire des mots. Je présenterai ensuite l'outil central de la plupart des algorithmes efficaces sur les sous-groupes du groupe libre : la représentation de chaque sous-groupe finiment engendré par un graphe étiqueté et enraciné (disons : d'un automate :-)…) unique et facilement calculable à partir d'un ensemble de générateurs du sous-groupe considéré, qu'on appelle le graphe de Stallings. Le jeu consiste ensuite à traduire les problèmes algorithmiques sur les sous-groupes en problèmes algorithmiques sur les graphes de Stallings, et à résoudre ces problèmes de la façon la plus efficace possible. On considèrera notamment les problèmes suivants -- bon, juste le début de cette longue liste. - Le problème du mot généralisé : étant donnés k+1 éléments du groupe libre (ce sont des mots), le dernier appartient-il au sous-groupe engendré par les k premiers ? - Le problème de l'indice : étant donné un tuple d'éléments du groupe libre, le sous-groupe qu'ils engendrent est-il d'indice fini ? - Le problème de la base : étant donné un tuple d'éléments du groupe libre, trouver le rang, et une base du sous-groupe qu'ils engendrent. - Le problème de l'intersection : étant donnés deux tuples d'éléments du groupe libre, calculer l'intersection des sous-groupes qu'ils engendrent (ou calculer une base de cette intersection). - Le problème de la conjugaison : étant donnés deux tuples d'éléments du groupe libre, engendrent-ils le même sous-groupe ? deux sous-groupes conjugués ? - Et de nombreux autres problèmes (mots clés : minimalité de Whitehead, facteur libre, malnormalité, clôture par radical, clôture au sens de la topologie pro-p, etc…) title: Algorithmic problems in the theory of infinite groups abstract: In spite of the very general title, we will talk only about problems on subgroups of infinite groups, and in fact, only on subgroups of free groups . The results and methods I will present have been obtained over the past 40 years and are due to many researchers. I will start by setting the landscape, including for those who forgot what the free group is --- and we will see that we are dealing here, from the algorithmic point of view, with a variant of combinatorics on words. I will then present the tool that is central to most efficient algorithms on subgroups of free groups: the representation of each finitely generated subgroup by a labeled rooted graph (shall we say… an automaton?) which is unique and easily computable when a tuple of generators of the subgroup under consideration is given. This graph is called the Stallings graph. The game consists, then, in translating algorithmic problems on subgroups into algorithmic problems on Stallings graphs, and in solving these problems as efficiently as possible. We will discuss in particular the following problems (clearly: just the beginning of this long list). - The generalized word problem: given k+1 elements of the free group (these are words), does the last one belong to the subgroup generated by the k first ones? - The index problem: given a tuple of elements of the free group, does the subgroup they generate have finite index? - The basis problem: given a tuple of elements of the free group, find the rank and a basis of the subgroup they generate. - The intersection problem: given two tuples of elements of the free group, compute the intersection of the subgroups they generate (compute a basis of this intersection). - The conjugacy problem: given two tuples of elements of the free group, are the subgroups they generate equal? conjugated? - And many other problems (keywords: Whitehead minimality, free factors, malnormality, closure under radicals, closure in the sense of the pro-p topology, etc…) |
Fri 26th Mar 10:00 am 11:00 am | Séminaire Anne Etien Title: Managing structural and behavioral evolution in relational database: Application of Software Engineering techniques. Abstract: Relational databases play a central role in many information systems. Their schemas usually contain structural and behavioral entity descriptions. However, as any piece of software, they must continuously evolve to adapt to new requirements of a world in constant change. From an evolution point of view, problems are twofold: (1) relational database management systems do not allow inconsistencies i.e., no entity can reference a non existing entity; (2) stored procedures bodies are not described by meta-data i.e., DBMS as PostgreSQL consider stored procedure bodies as plain text and references to entities are unknown. As a consequence, evaluating the impact of an evolution of the database schema is a difficult task. In this seminar, we present a semi-automatic approach based on recommendations (sort of nested code transformations). Recommendations are proposed to architects who select the ones fitting their needs. Selected recommendations are then analysed and compiled to generate SQL script respecting the constraints imposed by the RDBMS. To support recommendations, we designed a meta-model for relational databases easing computation of change impact. We performed an experiment to validate the approach by reproducing a real evolution on a database. The results of our experiment show that our approach is able to reproduce exactly a manual modification in 75% less time. Zoom link: univ-lille-fr.zoom.us/j/95419000064 |
Fri 19th Mar 10:00 am 12:00 pm | Seminar Pablo Ferragin Title: Theory and practice of learning-based compressed data structures Presenter: Giorgio Vinciguerra Abstract: We revisit two fundamental and ubiquitous problems in data structure design: predecessor search and rank/select primitives. We show that real data present a peculiar kind of regularity based on geometric considerations. We name it “approximate linearity”. We thus expand the horizon of compressed data structures by presenting two solutions for the problems above that discover, or “learn”, in a principled algorithmic way, these approximate linearities. We provide a walkthrough of these new theoretical achievements, also with a focus on open-source libraries and their experimental improvements. We conclude by discussing the plethora of research opportunities that these new learning-based approaches to data structure design open up. Zoom link: univ-lille-fr.zoom.us/j/95419000064 |
Fri 12th Mar 10:00 am 12:00 pm | Seminar: Antonio AL SERHALI Title: Can Earliest Query Answering on Nested Streams be achieved in Combined Linear Time? |
Fri 19th Feb 10:00 am 11:00 am | Seminar: Bernardo Subercaseau Title: Foundations of Languages for Interpretability. Abstract: The area of interpretability in Machine Learning aims for the design of algorithms that we humans can understand and trust. One of the fundamental questions of interpretability is: given a classifier M, and an input vector x, why did M classify x as M(x)? In order to approximate an answer to this "why" question, many concrete queries, metrics and scores have emerged as proxies, and their complexity has been studied over different classes of models. Many of these analyses are ad-hoc, but they tend to agree on the fact that these queries and scores are hard to compute over Neural Networks, but easy to compute over Decision Trees. It is thus natural to think of a more general approach, like a query language in which users could write an arbitrary number of different queries, and that would allow for a generalized study of the complexity of interpreting different ML models. Our work proposes foundations for such a language, tying to First Order Logic, as a way to have a clear understanding of its expressiveness and complexity. We manage to define a minimalistic structure over FO that allows expressing many natural interpretability queries over models, and we show that evaluating such queries can be done efficiently for Decision Trees, in data-complexity. Zoom link: univ-lille-fr.zoom.us/j/95419000064 |
Fri 12th Feb 10:00 am 12:00 pm | Seminar: Florent Capelli Title: Regularizing the delay of enumeration algorithms Zoom link: univ-lille-fr.zoom.us/j/95419000064 Abstract: Enumeration algorithms are algorithms whose goal is to output the set of all solutions to a given problem. There exists different measures for the quality of such algorithm, whose relevance depends on what the user wants to do with the solutions set. If the goal of the user is to explore some solutions or to transform the solutions as they are outputted with a stream-like algorithm, a relevant measure of the complexity of an enumeration algorithm is the delay between the output of two distinct solutions. Following this line of thoughts, significant efforts have been made by the community to design polynomial delay algorithms, that is, algorithms whose delay between the output of two new solutions is polynomial in the size of the input. While this measure is interesting, it is not always completely necessary to have a bound on the delay and it is enough to ask for a guarantee that running the algorithm for O(t poly(n)) will result in the output of at least t solutions. Of course, by storing each solution seen and outputting them regularly, one can simulate a polynomial delay but if the number of solutions is large, it may result in a blow up in the space used by the enumerator. In this talk, we will present a new technique that allow to transform such algorithm into polynomial delay algorithm using polynomial space. This is joint work with Yann Strozecki. |
Fri 15th Jan 10:00 am 12:00 pm | Séminaire de Kim Nguyễn Titile: The BOLDR project Abstract: I n this presentation, I will give an account of the BOLDR project and perspectives in the field of language integrated queries. Several classes of solutions allow programming languages to express queries: specific APIs such as JDBC, Object-Relational Mappings (ORMs) such as Hibernate, and language-integrated query frameworks such as Microsoft's LINQ. However, most of these solutions do not allow for efficient cross-databases queries, and none allow the use of complex application logic from the programming language in queries. We study the design of a new language-integrated query framework called BOLDR that allows the evaluation in databases of queries written in general-purpose programming languages containing application logic, and targeting several databases following different data models. In this framework, application queries are translated to an intermediate representation. Then, they are typed with a type system extensible by databases in order to detect which database language each subexpression should be translated to. This type system also allows us to detect a class of errors before execution. Next, they are rewritten in order to avoid query avalanches and make the most out of database optimizations. Finally, queries are sent for evaluation to the corresponding databases and the results are converted back to the application. Our experiments show that the techniques we implemented are applicable to real-world database applications, successfully handling a variety of language-integrated queries with good performances. This talk will give an overview of what has been achieved so far (mainly in the context of Julien Lopez' PhD Thesis) and will glimpse at preliminary work that is being done in the context of a collaboration with Oracle Labs. |
Fri 8th Jan 10:45 am 12:30 pm | Séminaire @ Lê Thành Dũng (Tito) Nguyễn Title: The planar geometry of first-order string transductions (joint work with Pierre Pradic) Abstract: hal.archives-ouvertes......ument We propose a new machine model recognizing star-free languages, with a geometric flavor. Our starting point is the characterization of regular languages using two-way automata (2DFA). The idea is to take seriously the visual representations found throughout the literature of the behavior of a 2DFA on a word ; by putting a total order on the set of states, one can formally define what it means for such a behavior to be planar, in a sense analogous to the planarity of combinatorial maps. Star-free languages are then exactly the languages recognized by "planar 2DFA". We also show that the corresponding planar transducer model characterizes the class of first-order transductions (a.k.a. aperiodic regular functions). If time allows, the talk will briefly discuss the connections of this work with the non-commutative lambda-calculus (cf. our recent paper Aperiodicity in a non-commutative logic, ICALP'20). |
2020 | |
Thu 17th Dec 2:00 pm 4:00 pm | Nofar Carmeli Speaker: Nofar Carmeli (nofar.carme.li/) Zoom link: univ-lille-fr.zoom.us/j/95419000064 Title: The Complexity of Answering Unions of Conjunctive Queries. Abstract: We discuss the fine-grained complexity of enumerating the answers to a query over a relational database. With the ideal guarantees, linear time is required before the first answer to read the input and determine its existence, and then we need to print the answers one by one. Consequently, we wish to identify the queries that can be solved with linear preprocessing time and constant or logarithmic delay between answers. A known dichotomy classifies CQs into those that admit such enumeration and those that do not. The computationally expensive component of query answering is joining tables, which can be done efficiently if and only if the join query is acyclic. However, the join query usually does not appear in a vacuum; for example, it may be part of a larger query, or it may be applied to a database with dependencies. We inspect how the complexity changes in these settings and chart the borders of tractability within. In addition, we consider the task of enumerating query answers with a uniformly random order, and we propose to do so using an efficient random-access structure for representing the set of answers. We also prove conditional lower bounds showing that our algorithms capture all tractable queries in some cases. Among our results, we show that a union of tractable conjunctive queries may be intractable w.r.t. random access; on the other hand, a union of intractable conjunctive queries may be tractable w.r.t. enumeration. |
Fri 11th Dec 10:00 am 11:30 am | Alexandre Vigny Title: Elimination Distance to Bounded Degree on Planar Graphs Link to the zoominar: univ-lille-fr.zoom.us/j/95419000064 Abstract: What does it mean for a graph to almost be planar? Or to almost have bounded degree? On such simple graphs classes, some difficult algorithmic problems become tractable. Ideally, one would like to use (or adapt) existing algorithms for graphs that are "almost" in such a simple class. In this talk, I will discuss the notion of elimination distance to a class C, a notion introduced by Bulian and Dawar (2016). The goals of the talk are: 1) Define this notion, and discuss why it is relevant by presenting some existing results. 2) Show that we can compute the elimination distance of a given planar graph to the class of graph of degree at most d. I.e. answer the question: "Is this graph close to a graph of bounded degree?" The second part is the result of a collaboration with Alexandre Lindermayer and Sebastian Siebertz. |
Fri 4th Dec 10:00 am 11:00 am | Seminar: Pierre Pradic Title: Extracting nested relational queries from implicit definitions Abstract: arxiv.org/pdf/2005.06503.pdf In this talk, I will present results obtained jointly with Michael Benedikt establishing a connection between the Nested Relational Calculus (NRC) and sets implicitly definable using Δ₀ formulas. Call a formula φ(I,O) an implicit definition of the relation O(x,...) in terms of I(y,...) if O is functionally determined by I: for every I, O, O', if both φ(I,O) and φ(I,O') hold, then we have O ≡ O'. When φ is first-order and I and O are relations over base sorts, then Beth's definability theorem states that there is a first-order formula ψ(I,x,...) corresponding to O whenever φ(I,O) holds. Further, this explicit definition ψ can be effectively be computed from a sequent calculus proof witnessing that φ is functional. This allows for practical use of implicit definitions in the context of database programming, as there is a well-established link between fragments of explicitly FO definable relations and relational calculi. NRC is a conservative extension of relational calculi from database theory with limited powerset types in addition to tupling and anonymous base types. NRC expressions thus not only encompass flat relations over primitive datatypes like SQL but also nested collections, while remaining useful in practice. We extend the above correspondence between first-order logic and flat relational queries to NRC and implicit definitions using set-theoretical Δ₀ formulas over (typed) nested collection. Our proof of the equivalence goes through a notion of Δ₀-interpretation and a generalization of Beth definability for multi-sorted structures. This proof is non-constructive and thus does not yield any useful algorithm for converting implicit definitions into NRC terms. Using an approach more closely related to proof-theoretic interpolation, we give a constructive proof of the result restricted to intuitionistic provability, i.e, when the input functionality proof π of φ(I,O) is carried out in intuitionistic logic. Further, if π is cut-free, this can be done efficiently. Whether or not there exists a polynomial-time procedure working with classical proofs of functionality is still an open problem. I will focus on the effective result for the talk, and if time allows, discuss the difficulties with extending it to classical logic. I will not assume any background in either database or model theory. |
Fri 27th Nov 10:00 am 11:30 am | Seminar: Charles Paperman Title: Stackless processing of streamed trees Abstract: In this talk, I will first present the state of the art of efficiency implementation of streaming-text algorithms on modern architecture. Then some recent results on the extraction of information on streamed of structured documents without stack overhead. For more info: paperman.name/data/pub.....d.pdf |
Fri 13th Nov 10:00 am 12:00 pm | Seminar: Mikaël Monet Title: The Complexity of Counting Problems over Incomplete Databases Abstract: In this presentation, I will talk about various counting problems that naturally arise in the context of query evaluation over incomplete databases. Incomplete databases are relational databases that can contain unknown values in the form of labeled nulls. We will assume that the domains of these unknown values are finite and, for a Boolean query $q$, we will consider the following two problems: given as input an incomplete database $D$, (a) return the number of completions of $D$ that satisfy $q$; or (b) return or the number of valuations of the nulls of $D$ yielding a completion that satisfies $q$. We will study the computational complexity of these problems when $q$ is a self-join--free conjunctive query, and study the impact on the complexity of the following two restrictions: (1) every null occurs at most once in $D$ (what is called *Codd tables*); and (2) the domain of each null is the same. Roughly speaking, we will see that counting completions is much harder than counting valuations, and that both (1) and (2) can reduce the complexity of our problems. I will also talk about the approximability of these problems and prove that, while counting valuations can efficiently be approximated, in most cases counting completions cannot. On our way, we will encounter the counting complexity classes #P, Span-P and Span-L. The presentation will be based on joint work with Marcelo Arenas and Pablo Barcelo; see arxiv.org/abs/1912.11064 |
Fri 16th Oct 11:00 am 12:00 pm | Seminar: Aurélien Lemay Title: ShEx Learning from Typed Graphs Abstract: In knowledge graphs, schemas are becoming a new asset to describe the organization of data. The new world-leading format Shex is becoming a de-facto standard in the industry that allows defining flexible and powerful schemas. In this context, the inference of schemas can become a solution to provide shex expressions that describe already existing data. Typically, the inference starts from untyped graphs. However, these tasks appears to be more complex than expected in general, and is possible only for subclasses of Shex. The inference of schemas from typed graph gives a baseline for those algorithms. Its comprehension allows to understand better the underlying difficulties of the task. It presents already unexpected difficulties. We present an algorithm that infers Shex-defined schemas from fully typed graphs. We also present some encountered difficulties, as well as the limitations of the approach. |
Fri 24th Jul 2:30 pm 4:30 pm | Momar Sakho, PhD defense |
Wed 8th Jan 1:30 pm 3:30 pm | Introduction to argumentation theory Salle Agora 1, Bâtiment ESPRIT |
2019 | |
Thu 19th Dec 11:00 am 1:30 pm | Thèse L. Gallois amphi Bâtiment B Inria |
Fri 13th Dec 11:45 am 1:00 pm | 1. On Parsing Gpath (Jérémy and Antonio) 2. On Nested Regular Expression (Joachim) |
Fri 13th Dec 10:30 am 11:45 am | Repet Lily pour l'équipe "Lille-Salle B31 " |
Tue 24th Sep 10:00 am 11:00 am | Stijn Vansummeren Title: General Dynamic Yannakakis: Conjunctive Queries with Theta Joins Under Updates Abstract: The ability to efficiently analyze changing data is a key requirement of many real-time analytics applications like Stream Processing, Complex Event Recognition, Business Intelligence, and Machine Learning. Traditional approaches to this problem are based either on the materialization of subresults (to avoid their recomputation) or on the recomputation of subresults (to avoid the space overhead of materialization). Both techniques have recently been shown suboptimal: instead of fully materializing results and subresults, one can maintain a data structure that supports efficient maintenance under updates and can quickly enumerate the full query output, as well as the changes produced under single updates. In our work we are concerned with designing a practical family of algorithms for dynamic query evaluation based on this idea, and for queries featuring both equi-joins and inequality joins, as well as certain forms of aggregation. Our main insight is that, for acyclic conjunctive queries, such algorithms can naturally be obtained by modifying Yannakakis' seminal algorithm for processing acyclic joins in the static setting. In this talk I present the main ideas behind this modfication, offset it against the traditional ways of doing incremental view maintenance, and discuss recent extensions such as dealing with general theta-joins. Amphitheater of INRIA Building B. |
Tue 25th Jun 11:30 am 5:30 pm | Happy Hours Inria Lille |
Tue 25th Jun 10:30 am 11:30 am | Seminar Véronique Benzaken and Évelyne Contejean Elles présenteront un outil qui prend en entrée une requête SQL et sa compilation par Postrgres sous forme de plan d'exécution, et démontre (avec Coq) que la requête initiale est équivalente au plan d'exécution. Lille-Salle B21 |
Fri 21st Jun 11:00 am 12:00 pm | Charles |
Fri 24th May 11:00 am 12:00 pm | Seminaire Sławek |
Fri 10th May 11:00 am 12:00 pm | Seminaire Iovka |
Fri 12th Apr 11:00 am 12:30 pm | Alexandre Vigny in Links Seminar |
Fri 5th Apr 11:00 am 12:00 pm | Semyon Grigorev in Links' seminar |
Fri 5th Apr 11:00 am 12:30 pm | Talk of Semyon Grigorev Title: Parsing techniques for context-free path querying Abstract: Context-free path querying (CFPQ) is a case of language constrained path querying: the way to specify constraints on paths in a graph in terms of formal languages. In CFPQ language is restricted to be a context-free. Classical parsing techniques and algorithms, such as generalized LR and LL parsing, or parser combinators, can be used for CFPQ. Results of adaptation of different parsing techniques for CFPQ will be presented. B31 |
Fri 22nd Mar 10:00 am 11:30 am | Seminar LINKS by Aurelien Lemay "Tutorial: Grammatical Inference" |
Fri 8th Mar 11:00 am 12:00 pm | Seminar Momar Title: Regular Matching and Inclusion on Compressed Tree Patterns with Context Variables
Abstract: We study the complexity of regular matching and inclusion for compressed tree patterns extended by context variables. The addition of context variables to tree patterns permits us to properly capture compressed string patterns but also compressed patterns for unranked trees with tree and hedge variables. Regular inclusion for the latter is relevant to certain query answering on Xml streams with references. |
Fri 15th Feb 11:00 am 12:00 pm | Seminar [Florent] |
Wed 13th Feb 1:30 pm 2:30 pm | 30mn de science : Florent Capelli on Knowledge Compilation Inria salle Plénière (Bâtiment A) |
Fri 1st Feb 11:00 am 12:30 pm | Bruno Guillon in Links' seminar Title: Finding paths in large graphs Abstract: When dealing with large graphs, classical algorithms for finding paths such as Dijkstra's Algorithm are unsuitable, because they require to perform too many disk accesses. To avoid this while keeping a data structure of size quasi-linear in the size of the graph, we propose to guide the path search with a distance oracle, obtained from a topological embedding of the graph. I will present fresh experimental research on this topic, in which we obtain graph embeddings using learning algorithms from natural language processing. On some graphs, such as the graph of publications from DBLP, our topologically-guided path search allows us to visit a small portion of the graph only, in average. This is joint work with Charles Paperman. B21 Room |
2018 | |
Fri 23rd Nov 11:00 am 12:30 pm | Filip Mazowiecki in Links' seminar Title: Containment for Probabilistic automata. Abstract: This is an ICALP 2018 paper. We analyze when the model of probabilistic automata has decidable properties, when restricting the ambiguity. The notion of ambiguity is usually used in weighted automata or transducers, but we follow a recent paper by Fijalkow, Riveros and Worrell, which introduced this approach. We do not solve everything but our decidability results rely unexpectedly on Schanuel's conjecture and we provide some geometric intuition behind the hardness of the problem. |
Fri 16th Nov 11:00 am 12:30 pm | Aurelien Lemay's Habilitation defense IRCICA |
Thu 15th Nov 4:30 pm 5:30 pm | Andreas Maletti in Aurélien Lemay's prehabilitation seminar Lille-Salle B21 |
Thu 15th Nov 3:30 pm 4:30 pm | Henning Fernau in Aurélien Lemay's prehabilitation seminar: Lille-Salle B21 |
Fri 9th Nov 11:00 am 12:30 pm | Talk of Bruno Guillon Abstract: The time complexity of 1-limited automata is investigated from a descriptional complexity view point. Though the model recognizes regular languages only, it may use quadratic time in the input length. We show that, with a polynomial increase in size and preserving determinism, each 1-limited automaton can be transformed into a linear-time equivalent one. We also obtain polynomial transformations into related models, including weight-reducing Hennie machines (i.e., one-tape Turing machines syntactically forced to operate in linear-time), and we show exponential gaps for converse transformations in the deterministic case. |
Fri 26th Oct 11:00 am 12:30 pm | Momar Sakho in Links seminar "Lieu : Lille, Salle : A12" |
Thu 18th Oct 4:00 pm 5:00 pm | Talk of Mikael Monet Title: Combined Complexity of Probabilistic Query Evaluation Abstract: Query evaluation over probabilistic databases (probabilistic query evaluation, or PQE) is known to be intractable in many cases, even in data complexity, i.e., when the query is fixed. Although some restrictions of the queries and instances have been proposed to lower the complexity, these known tractable cases usually do not apply to combined complexity, i.e., when the query is not fixed. This talk gives an overview of my PhD research, which investigates which queries and instances ensure the tractability of PQE in combined complexity. I will first present our work on PQE of conjunctive queries on binary signatures, which can be rephrased as a probabilistic graph homomorphism problem. We restrict the query and instance graphs to be trees and show the impact on the combined complexity of diverse features such as edge labels, branching, or connectedness. This is joint work with Antoine Amarilli and Pierre Senellart and was presented at PODS'2017. Second, we will explore the combined complexity of evaluating queries on treelike databases, i.e., databases whose treewidth is bounded by a constant. We introduce a class of queries (named 'CFG-Datalog') which generalizes many known query languages that are tractable in this context. Specifically, we show that the (non-probabilistic) evaluation of CFG-Datalog on treelike databases can be solved with complexity linear in the product of the instance size and of the query size. In the process, we introduce a new representation of the provenance of a query on a database, based on cyclic Boolean circuits. This is joint work with Antoine Amarilli, Pierre Bourhis, and Pierre Senellart, and was presented at ICDT'2017. Last, we will move to the field of knowledge compilation and present our work that connects various notions of width for Boolean circuits. We show that circuits of bounded treewidth can be efficiently compiled into structured deterministic decomposable normal forms (d-SDNNFs), which in particular allows efficient probability computation. We show the implications of this result for PQE of CFG-Datalog on treelike databases. We also prove general lower bounds on knowledge compilation formalisms, which imply lower bounds for provenance computation. This is joint work with Antoine Amarilli and Pierre Senellart and was presented at ICDT'2018. "Lieu : Lille, Salle : B21" |
Fri 28th Sep 10:15 am 11:45 am | José Lozano Links seminar |
Fri 21st Sep 10:30 am 12:00 pm | Fabian Reiter in Links' Seminar: Descriptive distributed complexity This talk connects two classical areas of theoretical computer science: descriptive complexity and distributed computing. The former is a branch of computational complexity theory that characterizes complexity classes in terms of equivalent logical formalisms. The latter studies algorithms that run in networks of interconnected processors. Although an active field of research since the late 1970s, distributed computing is still lacking the analogue of a complexity theory. One reason for this may be the large number of distinct models of distributed computation, which make it rather difficult to develop a unified formal framework. In my talk, I will outline how the descriptive approach, i.e., connections to logic, could be helpful in this regard. Salle B21 |
Fri 7th Sep 11:00 am 12:30 pm | Rustam Azimov in Links Seminar: "Context-Free Path Querying by Matrix Multiplication" |
Fri 25th May 10:00 am 11:30 am | Nicolas Crosetti in Links' Seminar: Dependency weighted aggregation Lille B21 |
Fri 27th Apr 10:30 am 12:30 pm | Yann Strozecki in Links' Seminar: Methods in enumeration In enumeration we are interested in generating a set of solutions, while bounding the time needed to generate one solution. We will first present the complexity measures used in this context, simple theoritical results and a few open questions. We then introduce classical problems in this area such as the enumeration of: trees, models of a DNF, model of a FO or MSO formula, the maximal cliques of a graph, circuits of a matroid ... We use them to illustrate the algorithmic toolbox of enumeration (Gray Code, backtrack search, reverse search, saturation...). Lille B21 |
Wed 25th Apr 2:15 pm 3:45 pm | Nicolas Stage Jan's office |
Fri 20th Apr 2:15 pm 3:45 pm | Nicolas Stage Jan's office |
Fri 13th Apr 2:15 pm 3:45 pm | Nicolas Stage Jan's office |
Fri 13th Apr 10:00 am 12:00 pm | Iovka Boneva and Jérémie Dusart in Links' Seminar: Shape Expressions Schemas 2.0 : Semantics and Implementation We will present the semantics of the ShEx language, its implementation in java, and future directions of research. Salle B21 |
Fri 6th Apr 2:15 pm 3:45 pm | Nicolas Stage Jan's office |
Fri 30th Mar 2:15 pm 3:45 pm | Nicolas Stage Jan's office |
Fri 23rd Mar 10:00 am 11:30 am | Paul Gallot: High-Order Tree Transducers Paul présentera le papier de Sylvain, Aurélien et Paul, soumis à LICS 2018, sur le sujet des transducteurs d'arbres d'ordre supérieur. |
Wed 21st Mar 2:00 pm 3:15 pm | répétition Delta |
Fri 16th Mar 10:00 am 11:30 am | Luc Dartois in Links' Seminar: A Logic for Word Transductions with Synthesis In this talk I present a logic, called LT, to express properties of transductions, i.e. binary relations from input to output (finite) words. I argue that LT is a suitable candidate as a specification language for verification of non reactive systems, extending the successful approach of verifying synchronous systems via Mealy Machines and MSO. In LT, the input/output dependencies are modelled via an origin function which associates to any position of the output word, the input position from which it originates. LT is well-suited to express relations (which are not necessarily functional), and can express all regular functional transductions, i.e. transductions definable for instance by deterministic two-way transducers. Despite its high expressive power, LT has decidable satisfiability problems. The main contribution is a synthesis result: it is always possible to synthesis a regular function which satisfies the specification. Finally, I explicit a correspondence between transductions and data words. As a side-result, we obtain a new decidable logic for data words. Inria Lille |
Fri 9th Mar 10:00 am 11:00 am | Benjamin Bergougnoux : Counting minimal transversals of hypergraphs A transversal of a hypergraph H is a subset of vertices that intersects all the hyper-edges H. The enumeration and the counting of the minimal transversals have a lot of applications in many domains (graph theory, AI, datamining, etc). Counting problems are generally harder than theirs associated decision problems. For example, finding a minimal transversal is doable in polynomial time but counting them is #P-complet (the equivalent of NP-complet for counting problems). We have proved that we can count the minimal transversals of any beta-acyclique hypergraph in polynomial time. Our result is based on a recursive decomposition of the beta-acyclique hypergraph founded by Florent Capelli and by the introduction of a new notion that generalize the minimal transversals. A lot of exciting open questions live in the neighborhood of our result. In particular, our algorithm is able to count the minimum dominating set of a strong-chordal graph. But counting the minimum dominating set is #P-complete on split graphs. Is it the beginning of a complete characterization of the complexity of counting minimal dominating sets in dense graphs ? Salle B21 |
Fri 16th Feb 10:30 am 11:30 am | Victor Marsault : Formal semantics of the query-language Cypher Cypher is a query-language for property-graphs. It was originally designed and implemented as part of the Neo4j graph database, and it is currently used by several commercial database products and researchers. The semantics of Cypher queries is currently described using natural language and, as a result, it is often not well defined. This work is part of a project to define a full denotational semantics of Cypher queries. The talk will first present the main features of Cypher through examples, including the core mecanism: graph pattern-matching, and then will describe the formal semantics in its current state. Salle B21 - INRIA Institut National Recherche Informatique Automatique; 40 Avenue Halley, 59650 Villeneuve d'Ascq, France |
Wed 31st Jan 5:30 pm 7:00 pm | Bien avant l'avènement des ordinateurs personnels, de l'internet et des smartphones , l'Interaction Homme-Machine (IHM) était déjà une préoccupation au cœur de certaines des visions qui ont contribué à forger l'informatique moderne, qu'elle soit personnelle ou professionnelle. Pour autant, la conception et l'étude des interactions est encore souvent considérée comme secondaire dans la conception des systèmes, la priorité étant souvent mise sur le développement des fonctionnalités plutôt que sur les moyens pour les utiliser. Cette situation s'est progressivement améliorée, avec notamment l'avènement des dispositifs tactiles (smartphones et tablettes) ou de divertissement (consoles de jeux) pour lesquels l'argument de simplicité d'utilisation a détrôné celui de la puissance intrinsèque. Cela a bien évidemment permis de populariser et démocratiser l'accès à la technologie. Mais une conséquence est, selon nous, un relatif appauvrissement des possibilités offertes par ces technologies paradoxalement plus puissantes que jamais. En masquant la complexité plutôt qu'en aidant à la maîtriser, en entretenant le mythe qu'avec ces dispositifs il est aisé pour chacun de faire beaucoup sans efforts, la tendance est à sacrifier le potentiel de l'outil informatique et la performance des utilisateurs pour la rapidité de prise en main, sans permettre un usage plus avancé, plus performant, et peut-être plus gratifiant pour l'utilisateur. Cet équilibre entre simplicité d'usage et puissance de l'outil est un compromis difficile à trouver, et c'est selon nous un des défis et une difficulté majeure de l'IHM : observer et comprendre les phénomènes sensorimoteurs et psychomoteurs, cognitifs, sociaux et technologiques mis en œuvre lors de l'interaction entre des personnes et des systèmes afin d'améliorer cette interaction et d'en guider la conception pour encapaciter les utilisateurs. Le but étant finalement de leur permettre de réaliser ce qu'il leur serait impossible de faire sans cet outil, même si cela requiert de leur part des efforts certains d'apprentissage. Dans ce séminaire, nous commencerons par présenter ce qu'est l'Interaction Homme-Machine en tant que domaine de recherche avec ses objectifs, ses méthodes et ses pratiques. Ensuite, au travers d'une brève histoire de l'informatique sous le prisme de l'interaction, nous évoquerons quelques innovations d'aujourd'hui qui découlent des visions de pionniers du domaine, en considérant notamment ce compromis simplicité / puissance de l'outil. Nous verrons aussi avec des exemples et contre-exemples issus de nos environnements numériques actuels, ainsi qu'avec des travaux de recherche récents, que ces visions portent encore de nombreux défis présents et futurs de l'IHM. En particulier, nous conclurons en discutant de la nécessité d'adopter une approche centrée utilisateur et interaction à l'heure des grands défis scientifiques, technologiques et sociétaux du numérique tels que la conception des systèmes autonomes ou le traitement et l'exploitation automatique des données. Mots-clés : Machines et langages Algorithme Interaction Homme machine (IHM). Liliad |
Wed 31st Jan 4:00 pm 5:30 pm | Cours extérieur de Gérard Berry du Collège de France Le centre Inria Lille - Nord Europe reçoit Gérard Berry, du Collège de France pour son cours sur la photographie numérique. Ce cours se prolongera par un séminaire de Stéphane Huot, responsable de l'équipe Mjolnir. Cette manifestation sera suivie d'un cocktail au cours duquel Isabelle Herlin, directrice du centre de recherche Inria Lille - Nord Europe présentera ses voeux. Date : 31/01/2018 Lieu : Lilliad, Campus Université Lille - sciences et technologies - 2 avenue Jean Perrin, Villeneuve d'Ascq Programme 15h30 : Accueil 15h45 : Introduction par Isabelle Herlin 16h - 17h30 : Cours de Gérard Berry, "La photographie numérique, un parfait exemple de la puissance de l'informatique" 17h30 - 18h30 : Séminaire de Stéphane Huot, "Interaction humain-machine : passé composé et futur simple... ou l'inverse" 18h30 - 18h45 : Questions aux deux orateurs 19h - 20h30 : Cocktail Cours de Gérard Berry Bio express : Gérard Berry est informaticien, professeur au Collège de France où il est titulaire de la chaire d'Algorithmes, machines et langages. Résumé L’appareil photo numérique est un excellent exemple de l’évolution actuelle des systèmes cyberphysiques, c’est-à-dire des systèmes couplant intimement mécanique, physique, électronique et logiciel. C’est aussi un exemple merveilleux et accessible à tous de la puissance des méthodes de l’informatique par rapport à celles de la physique et de la mécanique seules. Le cours présentera la panoplie des algorithmes embarqués dans les appareils photos modernes et dans les logiciels de postproduction, puis discutera l’impact majeur qu’ils ont sur la conception des appareils et des objectifs, totalement bouleversée en ce moment, et celui qu’ils ont sur les photographes professionnels ou amateurs. La photographie argentique, fort ancienne, n’a que lentement progressé au cours du XXe siècle : amélioration lente des pellicules et papiers, introduction de l’exposition automatique calculée analogiquement à partir de cellules photo-électriques, visée télémétrique ou reflex, tout cela a demandé des dizaines d’années. Au contraire, à partir de la commercialisation du premier appareil numérique en 1990, la photographie numérique a évolué extrêmement vite. En 2003, on trouvait déjà des appareils semi-professionnels corrects et, dès 2009, des appareils reflex de haute qualité à un prix abordable. Maintenant, il existe toute une panoplie d’appareils de tailles variées, tous capables de fournir des images de grande qualité. Même les téléphones sont devenus de très bons appareils photos et caméras vidéo, principalement grâce aux algorithmes qu’ils mettent en œuvre. Comme ils savent faire bien d’autres choses, par exemple envoyer immédiatement les images sur Internet, ils sont en train de remplacer les anciens petits appareils compacts et de servir d’équipement unique pour les photographes occasionnels et pour tous dans les pays où la photo argentique était d’un coût inabordable pour les habitants. La logique de la photo numérique est ainsi devenue très différente de celle de l’argentique, ce qui n’empêche cependant pas que cette dernière garde toujours les faveurs de certains artistes. Qu’est-ce qui a permis cette révolution et pourquoi est-elle allée aussi vite ? Il y a trois raisons principales : la conception par les physiciens et la fabrication industrielle en grand volume de capteurs de haute qualité ; l’augmentation considérable de la puissance et la diminution de la dépense énergétique des ordinateurs embarqués, grâce à la fameuse loi de Moore ; enfin, et surtout, l’amélioration continue des algorithmes de la photographie, qui jouent en fait un rôle plus important que celui des capteurs. Dans les quinze dernières années, nous avons gagné au moins 4 degrés de sensibilité, dont les trois quarts grâce aux algorithmes. Même des appareils aux capteurs relativement petits savent faire des photos de très haute qualité à 3200 ISO, ce qui était complètement impossible avec l’argentique. Le cours détaillera d’abord la suite des transformations algorithmiques subtiles qui permettent le développement des images des données numériques du capteur, aboutissant à l’image finale en gérant au mieux la lumière, la netteté et le bruit. Ensuite, il étudiera les algorithmes dédiés à la correction automatique des divers défauts optiques des objectifs ; il montrera que la puissance de ces algorithmes fait que ces objectifs ne seront plus conçus comme auparavant : leur conception intègre désormais totalement physique et algorithmique, fournissant des optiques de meilleure qualité, moins encombrantes, plus légères et moins chères. Il insistera sur l’importance que prennent les nouveaux traitements fondés sur la fusion de prises de vue successives pour l’amélioration de la qualité selon divers objectifs (lumière, bruit, profondeur de champ, etc.), en particulier pour les téléphones. Il montrera pourquoi fonder les nouveaux appareils directement sur les algorithmes modifie de plus en plus le cœur de leur conception, ce qui fait que bien d’autres nouveautés surprenantes pourront apparaître. Des évolutions similaires bouleversent d’ailleurs tout autant les imageries médicale et astronomique. Enfin, le cours soulignera l’importance des nouveaux algorithmes destinés à l’amélioration de l’ergonomie de la prise de vue, qui rendent la vie technique du photographe bien plus facile sur quasiment tous les aspects : interaction humain-machine bien conçue, stabilisation du capteur et de l’objectif pour supprimer le flou de bougé, gestion sophistiquée de la lumière et de la mise au point, nombreuses aides à la prise de vue dans le viseur devenant électronique, liaison directe avec les ordinateurs et téléphones. Séminaire de Stéphane Huot Résumé Bien avant l'avènement des ordinateurs personnels, de l'internet et des smartphones , l'Interaction Homme-Machine (IHM) était déjà une préoccupation au cœur de certaines des visions qui ont contribué à forger l'informatique moderne, qu'elle soit personnelle ou professionnelle. Pour autant, la conception et l'étude des interactions est encore souvent considérée comme secondaire dans la conception des systèmes, la priorité étant souvent mise sur le développement des fonctionnalités plutôt que sur les moyens pour les utiliser. Cette situation s'est progressivement améliorée, avec notamment l'avènement des dispositifs tactiles (smartphones et tablettes) ou de divertissement (consoles de jeux) pour lesquels l'argument de simplicité d'utilisation a détrôné celui de la puissance intrinsèque. Cela a bien évidemment permis de populariser et démocratiser l'accès à la technologie. Mais une conséquence est, selon nous, un relatif appauvrissement des possibilités offertes par ces technologies paradoxalement plus puissantes que jamais. En masquant la complexité plutôt qu'en aidant à la maîtriser, en entretenant le mythe qu'avec ces dispositifs il est aisé pour chacun de faire beaucoup sans efforts, la tendance est à sacrifier le potentiel de l'outil informatique et la performance des utilisateurs pour la rapidité de prise en main, sans permettre un usage plus avancé, plus performant, et peut-être plus gratifiant pour l'utilisateur. Cet équilibre entre simplicité d'usage et puissance de l'outil est un compromis difficile à trouver, et c'est selon nous un des défis et une difficulté majeure de l'IHM : observer et comprendre les phénomènes sensorimoteurs et psychomoteurs, cognitifs, sociaux et technologiques mis en œuvre lors de l'interaction entre des personnes et des systèmes afin d'améliorer cette interaction et d'en guider la conception pour encapaciter les utilisateurs. Le but étant finalement de leur permettre de réaliser ce qu'il leur serait impossible de faire sans cet outil, même si cela requiert de leur part des efforts certains d'apprentissage. Dans ce séminaire, nous commencerons par présenter ce qu'est l'Interaction Homme-Machine en tant que domaine de recherche avec ses objectifs, ses méthodes et ses pratiques. Ensuite, au travers d'une brève histoire de l'informatique sous le prisme de l'interaction, nous évoquerons quelques innovations d'aujourd'hui qui découlent des visions de pionniers du domaine, en considérant notamment ce compromis simplicité / puissance de l'outil. Nous verrons aussi avec des exemples et contre-exemples issus de nos environnements numériques actuels, ainsi qu'avec des travaux de recherche récents, que ces visions portent encore de nombreux défis présents et futurs de l'IHM. En particulier, nous conclurons en discutant de la nécessité d'adopter une approche centrée utilisateur et interaction à l'heure des grands défis scientifiques, technologiques et sociétaux du numérique tels que la conception des systèmes autonomes ou le traitement et l'exploitation automatique des données. Mots-clés : Machines et langages Algorithme Interaction Homme machine (IHM). Lililad |
Wed 31st Jan 3:30 pm 8:30 pm | Le centre Inria Lille - Nord Europe reçoit Gérard Berry, du Collège de France pour son cours sur la photographie numérique. Ce cours se prolongera par un séminaire de Stéphane Huot, responsable de l'équipe Mjolnir. Cette manifestation sera suivie d'un cocktail au cours duquel Isabelle Herlin, directrice du centre de recherche Inria Lille - Nord Europe présentera ses voeux. Programme 15h30 : Accueil 15h45 : Introduction par Isabelle Herlin 16h - 17h30 : Cours de Gérard Berry, "La photographie numérique, un parfait exemple de la puissance de l'informatique" 17h30 - 18h30 : Séminaire de Stéphane Huot, "Interaction humain-machine : passé composé et futur simple... ou l'inverse" 18h30 - 18h45 : Questions aux deux orateurs 19h - 20h30 : Cocktail Liliad |
Fri 19th Jan 10:00 am 12:00 pm | Sylvain Salvati: "On magic set rewriting for Datalog" Cet exposé se veut une introduction à la transformation de programmes datalog. En particulier, je présenterai la transformation appelée "supplementary magic set rewriting" qui permet d'obtenir des programmes datalog dont l'évaluation semi-naïve se comporte de façon similaire à l'évaluation des programmes originaux par résolution SLD. Je montrerai l'algorithme et des exécutions de programmes sur des exemples issus de problèmes d'analyses grammaticales. Lille B21 |
2017 | |
Fri 10th Nov 10:00 am 11:00 am | Momar Sakho: "Complexity of Certain Query Answering on Hyperstreams" A hyperstream is a sequence of streams with references to others. We study the complexity of computing certain answers for queries defined by automata and evaluated on hyperstreams of words. We show that the problem is PSPACE-complete for deterministic query automata, but that it can be solved in PTime for linear hyperstreams even with factorization. Salle B21 |
Fri 3rd Nov 10:30 am 12:00 pm | Joanna Ochremiak, Paris 7: "Proof complexity of constraint satisfaction problems" Many natural computational problems, such as satisfiability and systems of equations, can be expressed in a unified way as constraint satisfaction problems (CSPs). In this talk I will show that the usual reductions preserving the complexity of the constraint satisfaction problem preserve also its proof complexity. As an application, I will present two gap theorems, which say that CSPs that admit small size refutations in some classical proof systems are exactly the constraint satisfaction problems which can be solved by Datalog. This is joint work with Albert Atserias. B21 |
Fri 13th Oct 11:00 am 1:00 pm | Dimitri Gallois: On parallel rewriting B21 |
Fri 29th Sep 10:00 am 12:00 pm | Nicolas Bacquey: "An algorithm for deciding the equivalence of tree transducers" As an extension of word transformations, tree transformations have numerous applications in computer science : XSLT transformations, Unix packages installation and removal, databases queries... Likewise, there are many formal models to describe these transformations. However, the proof of formal properies on these models is often difficult, or even undecidable. In this talk, I will be interested in one of the simplest model for tree transformations, namely deterministic top-down tree transducers (DTOP). It has been known for a while that the equivalence problem of DTOPs can be solved via an earliest normal form comparison algorithm, that is in 2EXPTIME. However, when applying this algorithm to practical cases, it seemed that the worst case was not bound to happen often, if ever. I will present a new algorithm for the problem, based on the search of counterexamples via the expansion and unification of a set of rules over states of DTOPs. The most interesting feature of this algorithm is that it runs in exponential time, thus proving that the equivalence problem of DTOPs is in fact EXPTIME-complete. Lille B31 |
Thu 6th Jul all day | ANR Headwork: General Meeting Rennes |
Fri 16th Jun all day | 09h15-09h45 Coffee Welcome 09h45-10h30 Michel de Rougemont: Approximate integration of streaming graph edges 10h30-11h15 Florent Cappelli: Understanding the complexity of #SAT using knowledge compilation 11h15-11h45 Yann Strozecki: Enumerating maximal solutions of saturation problems 12h00 Lunch 14h00 Discussion libre 16h00 End Inria Lille |
Thu 15th Jun all day | 09h15-09h45 Welcome coffee 09h45-10h30 Pierre Bourhis: Introduction of circuit from database queries 10h30-11h15 Jen Keppeler: Answering FO+MOD queries under updates on bounded degree databases 11h15-12h00 Antoine Amarilli: Enumeration of valuation of circuits 12h00-13h30 Lunch + Café 13h30-14h30 Jan Ramon: Question around IA 14h30-15h15 Ahmet Kara: Covers of Query Results 15h15-15h45 Break 15h45-16h30 Alexandre Vigny: Constant delay enumeration for FO queries over databases with local bounded expansion 20h00 Dinner at Le Palermo Inria Lille |
Fri 9th Jun 10:30 am 12:30 pm | Valentin Montmirail: "A Recursive Shortcut for CEGAR: Application to the Modal Logic K Satisfiability Problem" Counter-Example-Guided Abstraction Refinement (CEGAR) has been very successful in model checking. Since then, it has been applied to many different problems. It is especially proved to be a highly successful practical approach for solving the PSPACE complete QBF problem. In this paper, we propose a new CEGAR-like approach for tackling PSPACE complete problems that we call RECAR (Recursive Explore and Check Abstraction Refinement). We show that this generic approach is sound and complete. Then we propose a specific implementation of the RECAR approach to solve the modal logic K satisfiability problem. We implemented both CEGAR and RECAR approaches for the modal logic K satisfiability problem within the solver MoSaiC. We compared experimentally those approaches to the state-of-the-art solvers for that problem. The RECAR approach outperforms the CEGAR one for that problem and also compares favorably against the state-of-the-art on the benchmarks considered. "Lille-Salle B21" |
Tue 6th Jun to Fri 9th Jun all day | Visit of Jean-Marc Talbot, Université de Marseille |
Fri 2nd Jun all day | Visit of Floris Geerts, University of Antwerp |
Fri 21st Apr all day | Visit of Florent Capelli, London University |
Fri 24th Mar all day | Visit of Charles Paperman, Université Paris 7 Université Paris 7 www.liafa.univ-paris-diderot.fr/~paperman/ INRIA Institut National Recherche Informatique Automatique 40 Avenue Halley, 59650 Villeneuve d'Ascq, France |
Wed 15th Mar 10:30 am 12:00 pm | Emmanuel Filliot, Université Libre de Bruxelles: "Automata, Logic and Algebra for Word Transductions" This talk will survey old and recent results about word transductions, i.e. functions mapping (finite) words to words. Connections between automata models (transducers), logic and algebra will be presented. Starting with rational functions, defined by (one-way) finite transducers, and the canonical model of bimachines introduced by Reutenauer and Schützenberger, the talk will also target the more expressive class of functions defined by two-way transducers and their equivalent MSO-based formalism. "Lille-Salle B21" |
Wed 15th Mar all day | Visit of Emmanuel Filliot, Université Libre de Bruxelles |