Links' Seminars and Public Events | ![]() ![]() |
2024 | |
---|---|
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 |