Links' Seminars and Public Events |

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 rewritingB21 |

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 MeetingRennes |

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 7Université 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 |

Wed 1st Feb 11:00 am 12:30 pm | Pierre Bourhis: The ChaseInria Lille |

Fri 20th Jan 10:30 am 12:30 pm | Pierre Bourhis: "Tree Automata for Reasoning in Databases and Artificial Intelligence"In database management, one of the principal task is to optimize the queries to evaluate them efficiently. It is in particular the case for recursive queries for which their evaluation can lead to crawl all the database. In particular, one of the main question is to minimize the queries in order to avoid to evaluate useless parts of the query. The core theoretical question around this line of work is the problem of inclusion of a query in another. Interestedly, this question is related to an important question in IA which is to answer a query when the data is incomplete but rules are given to derive new information. This problem is called certain query answering. In both context, if both problem are undecidable in general, there are fragments based on guardedness that are decidable due to the fact there exists witness of the problems that have a bounded tree width and that their encoding in trees is regular. Furthermore, the queries can be translated in MSO. In both contexts, Courcelle’s Theorems imply the decidability of both problems. I will present to the different results on the translation of logic class of formula for our problems into tree automata to obtain tight bounds to the problems of inclusion of recursive queries or certain query answering. Inria Lille |

Wed 11th Jan 2:15 pm 3:25 pm | Michael vanden Boom, Oxford University : Decidable fixpoint logicsFixpoint logics can express dynamic, recursive properties, but often fail to have decidable satisfiability. A notable exception to this is the family of well-behaved "guarded" fixpoint logics, which subsume a variety of query languages and integrity constraints of interest in databases and knowledge representation. In this talk, I will survey some recent results about these logics. Lille B21 |

Mon 9th Jan to Fri 13th Jan all day | Visite Michael vanden Boom, Oxford University |

2016 | |

Fri 9th Dec all day | Kickoff HeadworkParis MNHN |

Fri 18th Nov 10:30 am 12:00 pm | Florent Capelli Links Seminar"Lille-Salle B21" |

Fri 18th Nov all day | Florent Capelli visit |

Tue 8th Nov 2:30 pm 4:30 pm | Seminar Link by Helmut Seidl: "Equivalence of Deterministic Top-Down Tree-to-String Transducers is Decidable"Abstract: We show that equivalence of deterministic top-down tree-to-string transducers is decidable, thus solving a long standing open problem in formal language theory. We also present efficient algorithms for subclasses: polynomial time for total transducers with unary output alphabet (over a given top-down regular domain language), and co-randomized polynomial time for linear transducers, these results are obtained using techniques from multi-linear algebra. For our main result, we prove that equivalence can be certified by means of inductive invariants using polynomial ideals. This allows us to construct two semi-algorithms, one searching for a proof of equivalence, one for a witness of non-equivalence. "Lille-Salle B31 " |

Mon 7th Nov 2:00 pm 4:00 pm | PhD defense Adrien Boiret |

Fri 4th Nov all day | colis general meetingParis |

Thu 27th Oct 10:00 am 6:00 pm | Links day |

Thu 27th Oct all day | links day |

Thu 20th Oct 2:00 pm 4:00 pm | Seminar Links by Vincent Hugot: "Top-Down Transducers for Data Trees"Abstract: Tree transducers have a wide range of application domains ranging from compiler construction, program analysis, and computational linguistics, to semi-structured databases and file system transformations. A common application of these domains is to specify and verify transformations of data trees, i.e., trees whose nodes are labeled by data values from an infinite domain. Most existing classes of tree transducers and their formal studies, however, are restricted to trees over finite signatures without data. In this paper, we lift the most prominent class of top-down tree transducers to data trees, such that its good properties are preserved. In particular, we show that top-down transducers for data trees have a decidable equivalence problem, without imposing any linearity restriction as in previous approaches based on symbolic top-down tree transducers. "Lille-Salle B21" |

Thu 13th Oct 2:00 pm 3:00 pm | Seminar Christof Löding"Lille-Salle B21" |

Thu 13th Oct 2:00 pm 5:30 pm | comité de projet |

Thu 13th Oct to Fri 14th Oct all day | visit christof löding |

Fri 30th Sep all day | arrivée de Jose Lozano |

Thu 29th Sep 2:00 pm 4:00 pm | Seminar Links by Aurélien Lemay"Lille-Salle B21" |

Tue 27th Sep all day | Ircica fetes ces 10 ansLille |

Fri 9th Sep 2:00 pm 4:00 pm | Momar Sakho"Lille-Salle B21" |

Wed 7th Sep 11:00 am 12:00 pm | jason demagoj |

Wed 31st Aug 10:00 am 1:00 pm | Links Seminar by Domagoj Vrgoč: "Querying Graph with Data""Lille-Salle B21" |

Thu 28th Jul all day | Visit of Serge Abiteboul and Victor Vianu |

Mon 11th Jul to Tue 12th Jul all day | Aggreg meetingMarseille |

Mon 27th Jun all day | Colis ANR project: general meetingInria Paris, Salle 119 "Ada Lovelace" |

Fri 24th Jun 2:00 pm 4:00 pm | Fatima Belkouch: on the hypercube algorithm for conjunctive queriesAbstract: We consider the problem of computing a conjunctive query on a large database in a parallel setting with p servers. Unlike traditional query processing, the complexity is no longer dominated by the number of disk accesses. Typically, a query is evaluated by a sufficiently large number of servers such that the entire data can be kept in the main memory of these servers. The dominant cost becomes that of communicating data and synchronizing among the servers. I will present some interesting results in [1, 2, 3, 4] dealing with the communication complexity of massively parallel computation of a query. The computation is performed in "rounds". First, I will present the Massively Parallel Communication (MPC) model to analyze the tradeoff between the number of rounds and the amount of communication required in a massively parallel computing environment. Then I will present the HyperCube (HC) algorithm that computes a full conjunctive query q in one round. I will discuss the communication complexity [2]. The main result is the optimal load O(m/p1/τ ) where τ is the fractional vertex cover of the hypergraph of q and m the input data size. References [1] Parallel Evaluation of Conjunctive Queries. Paris Koutris, Dan Suciu PODS2011 [2] Communication Steps for Parallel Query Processing. Paul Beame, Paris Koutris, Dan Suciu PODS2013 [3] Skew in Parallel Query Processing. Paul Beame, Paris Koutris Dan Suciu PODS'2014 [4] Worst-Case Optimal Algorithms for Parallel Query Processing. Paris Koutris, Paul Beame, Dan Suciu ICDT2016 "Lille-Salle B11" |

Thu 23rd Jun 2:00 pm 3:30 pm | Victor Vianu in PolarisAuditorium IRCICA |

Thu 23rd Jun all day | victor vianu visit |

Mon 20th Jun to Wed 22nd Jun all day | journee scientique inria à rennes |

Fri 17th Jun 9:00 am 12:30 pm | PhD Thesis Defense by Tom Sebastian: Evaluation of XPath Queries on XML streams with Networks of Early Nested Word AutomataAbstract: The challenge that we tackle in this thesis is the problem of how to answer XPath queries on XML streams with low latency, full coverage, high time efficiency, and low memory costs. We first propose to approximate earli- est query answering for navigational XPath queries by compilation to early nested word automata. It turns out that this leads to almost optimal la- tency and memory consumption. Second, we contribute a formal semantics of XPath 3.0. It is obtained by mapping XPath to the new query language λXP that we introduce. We then show how to compile λXP queries to net- works of early nested word automata, and develop streaming algorithms for the latter. Thereby we obtain a streaming algorithm that indeed covers all of XPath 3.0. Third, we develop an algorithm for projecting XML streams with respect to the query defined by an early nested word automaton. Thereby we are able to make our streaming algorithms highly time efficient. We have implemented all our algorithms with the objective to obtain an industrially applicable streaming tool. It turns out that our algorithms outperform all previous approaches in time efficiency, coverage, and latency. |

Thu 16th Jun 2:00 pm 4:00 pm | Nicolas Bacquey Links seminar: Introduction to uniform periodical computation : leader election on periodical cellular automata"Lille-Salle B21" |

Thu 16th Jun 10:00 am 12:00 pm | Hubie Chen, Semainar and Visit"Lille-Salle B21" |

Fri 22nd Apr 10:00 am 11:30 am | Assemblée générale Inria Lille |

Fri 1st Apr all day | Laurent d'Orazio (cancelled) |

Fri 25th Mar all day | Datacert ANR project: general meetingLyon |

Fri 18th Mar 10:30 am 12:00 pm | Charles Paperman: "Streaming and circuit complexity"Abstract: In this talk, I will present a connection between the streaming complexity and the circuit complexity of regular languages through a notion of streaming by block . This result provides tight constructions of boolean circuits computing an automaton, thanks to some classical and recent results on the circuit complexity of regular languages. I will apply this framework to the schema validation in streaming of XML-documents. Inria Lille |

Fri 18th Mar all day | Visit of Charles Paperman, Université Paris 7Inria Lille |

Fri 11th Mar 10:30 am 12:00 pm | Seminar Links by Sylvain Salvati: Behavioral verification of higher-order programsAbstract: Higher-order constructions make their way into main stream programming languages like Java, C++, python, rust... These constructions bring new challenges to the verification of programs as they make their control flow more complex. In this talk, I will present how methods coming from denotational semantics can prove decidable the verification of certain properties of higher-order programs. These properties are expressed by means of finite state automata of the possibly infinite execution trees generated by the programs and can capture safety properties but also liveness and fairness properties. |

Fri 11th Mar all day | Sylvain Salvati: visit and Talk |

Wed 9th Mar 1:30 pm 2:00 pm | cristan duriez 30 minutes de science inria lille |

Fri 4th Mar all day | Colis ANR project: general meetingInria Lille, Salle B21 |

Thu 3rd Mar all day | Kim Nguyen: visit for discussion with Links' members (no talk)Université Paris Sud www.lri.fr/~kn/ B218 |

Fri 19th Feb 11:00 am 3:00 pm | CNRS, Université Lens |

Thu 21st Jan 11:00 am 1:00 pm | Seminar by Vincent Penelle: "Rewriting high-order stack trees"Higher-order pushdown systems and ground tree rewriting systems can be seen as extensions of suffix word rewriting systems. Both classes generate infinite graphs with interesting logical properties. Indeed, the satisfaction of any formula written in monadic second order logic (respectively first order logic with reachability predicates) can be decided on such a graph. The purpose of this talk is to propose a common extension to both higher-order stack operations and ground tree rewriting. We introduce a model of higher-order ground tree rewriting over trees labelled by higher-order stacks (henceforth called stack trees), which syntactically coincides with ordinary ground tree rewriting at order 1 and with the dynamics of higher-order pushdown automata over unary trees. The infinite graphs generated by this class have a decidable first order logic with reachability. Formally, an order n stack tree is a tree labelled by order n-1 stacks. Operations of ground stack tree rewriting are represented by a certain class of connected DAGs labelled by a set of basic operations over stack trees describing of the relative application positions of the basic operations appearing on it. Applying a DAG to a stack tree t intuitively amounts to paste its input vertices to some leaves of t and to simplify the obtained structure, applying the basic operations labelling the edges of the DAG to the leaves they are appended to, until either a new stack tree is obtained or the process fails, in which case the application of the DAG to t at the chosen position is deemed impossible. This model is a common extension to those of higher-order stack operations presented by Carayol and of ground tree transducers presented by Dauchet and Tison. As further results we can define a notion of recognisable sets of operations through a generalisation. The proof that the graphs generated by a ground stack tree rewriting system have a decidable first order theory with reachability is inspired by the technique of finite set interpretations presented by Colcombet and Loding. "Lille-Salle B21" |

Thu 14th Jan all day | visite pierre senellart |

Tue 12th Jan to Thu 14th Jan all day | visite Antoine Amarilli |

2015 | |

Mon 14th Dec 2:00 pm 4:00 pm | Slawek Staworko's HDR defense: "Symbolic Inference Methods for Databases"M2, salle de réunion |

Fri 20th Nov 10:30 am 12:30 pm | Seminar Links by Stéphane Demri: "Separation Logic and Friends"Abstract: Separation logic is used as an assertion language for Hoare-style proof systems about programs with pointers, and there is an ongoing quest for understanding its complexity and expressive power. There are also a lot of activities to develop verification methods with decision procedures for fragments of practical use. Actually, there exist many variants for separation logic that can be viewed as fragments of second-order logic, as well as variants of modal or temporal logics in which models can be updated dynamically. In this talk, after introducing first principles on separation logic, issues related to decidability, computational complexity and expressive power are discussed. We provide several tight relationships with second-order logics, interval temporal logics or data logics, depending on the variants of the logic and on the syntactic resources available. "Lille-Salle B21" |

Fri 13th Nov 10:30 am 12:00 pm | Seminar Links by Iovka Boneva: "Shape Expressions Schemas"Abstract: Shape Expressions Schemas is an expressive schema and constraint language for RDF data. I am going to define the language, illustrate it with examples, then give a validation algorithm and talk about ongoing work. "Lille-Salle B21" |

Thu 29th Oct 10:00 am 12:00 pm | Seminar Links by Antoine Amarilli"Lille-Salle A11" |

Fri 9th Oct 10:30 am 12:30 pm | Seminar Links: Adrien Boiret"Lille-Salle B21" |

Thu 1st Oct 10:30 am 12:30 pm | Seminar Links by Eric Prud'hommeaux: Shape Expressions: (finally) a schema language for RDF graph structureInitial architects envinsioned RDF as a knowledge representation language, freeing users from syntactic limitations and revolutionizing the way information was exchanged. While inference and description logic are applied to RDF, the foundation of simple assertions composed of global, unambiguous identifiers, has many more mondane and practical applications. Distributed contributions to large (web-scale) data graphs demands adaptation of tree and stream-based validation techniques to operate over a graph. Shape Expressions performs an ordered traversal of RDF graphs to 1 validate of structural constraints. 2 perform generative semantic actions. "Lille-Salle B21" |

Fri 11th Sep 12:00 pm 1:00 pm | Florent Capelli |