Links' Seminars and Public Events |
2019 | |
---|---|
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 |