Résumés des exposés

Exposés du 3 au 5 avril

• Meghyn Bienvenu ‐ exposé invité ‐ (Laboratoire d'Informatique, de Robotique et de Microélectronique de Montpellier, CNRS & Université Montpellier)

  L'interrogation de données en présence d'ontologies : Exploiter les connaissances pour mieux tirer parti des données

  Ces dernières années ont vu un intérêt grandissant pour l’interrogation de données en présence d'ontologies ("ontology-mediated query answering", ou OMQA, en anglais), un nouveau paradigme en gestion de données qui vise à exploiter des connaissances sémantiques décrites par une ontologie afin d'améliorer la réponse aux requêtes. Les ontologies ont plusieurs avantages : elles permettent d'enrichir le vocabulaire d’interrogation des données, de relier les vocabulaires de différentes sources de données, et à pallier l’incomplétude des données en permettant l’inférence de nouveaux faits. Par contre, cette expressivité accrue complexifie la tâche de calculer les réponses aux requêtes. Dans ce contexte, la réécriture de requêtes, qui réduit OMQA à la réponse aux requêtes classique (sans ontologies), est une technique algorithmique particulièrement intéressante, car elle permet de bénéficier des bonnes performances et maturité des systèmes de gestion de bases de données.
  Dans cet exposé, je commencerai par donner une courte introduction à OMQA, un sujet de recherche très actif à la croisée des domaines de l’intelligence artificielle et des bases de données. Ensuite, je considérerai deux questions naturelles en lien avec la réécriture de requêtes (concernant l'existence et la taille des réécritures) et présenterai des solutions obtenues grâce à des techniques issues de différents champs de l'informatique théorique (complexité de circuits, automates, problèmes de satisfaction de contraintes).

• Isabelle Bloch (Laboratoire de Traitement et Communication de l'Information, Télécom ParisTech)

  Morphologie mathématique sur des hypergraphes

  Nous présentons des travaux réalisés en collaboration avec Alain Bretto (Université de Caen) sur la morphologie mathématique sur des hypergraphes. Nous définissons des treillis sur les hypergraphes, qui en donnent la structure algébrique. Cela conduit à la définition d'opérateurs morphologiques, tels que des dilatations (qui commutent avec le sup du treillis) et des érosions (qui commutent avec l'inf). Des mesures de similarité et de distances entre hypergraphes seront également décrites, construites à partir de valuations et d'opérateurs morphologiques. Enfin nous suggérons des liens avec l'analyse formelle de concepts.

• Marthe Bonamy (Laboratoire Bordelais de Recherche en Informatique, CNRS & Université de Bordeaux & Bordeaux INP)

  Reconfiguration combinatoire

  Reconfigurer une solution d'un problème donné, c'est lui appliquer des opérations élémentaires successives sans quitter l'espace des solutions. Un tel besoin apparaît naturellement dans des situations dynamiques où une solution donnée est déjà en place et doit être modifiée, sans qu'une rupture de service puisse être envisagée. Plusieurs grandes questions sont étudiées : quelles opérations élémentaires garantissent que toute autre solution peut être ainsi atteinte ? À opérations fixées, quelle est la complexité de décider si une autre solution donnée peut être atteinte ? Que dire du nombre d'opérations nécessaires pour cela ? Dans cet exposé, nous discuterons de divers résultats positifs et négatifs autour de problèmes de graphes.

• Ahmed Bouadjani (Institut de Recherche en Informatique Fondamentale, CNRS & Université Paris-Diderot)

  On verifying robustness of concurrent systems

  Concurrent systems are in general used by their clients under strong assumptions on their visible behaviors. This allows a modular design approach: at the level of the client, these assumptions allow to reason in an abstract way about the behaviors of the invoked systems. For instance, the users of a shared memory may assume that the implementation of the memory is sequentially consistent, which means that it behaves according to the standard interleaving model where write/read operations are considered to be atomic, and immediately visible to all parallel users. In an another context, the users of web services may consider that their requests are handled atomically in a serial way, etc. However, for performance reasons, the implementations of concurrent systems tend to parallelize operations, and to use optimizations (including reordering of actions) in order to increase the throughput of the system. This leads in general to relaxations in the semantics guaranteed by these implementations w.r.t. to strong consistency models. In this talk, we will address to issue of checking that a given program of the client is robust against this kind of relaxations, i.e., the observable behaviors of the client are the same under both the strong and relaxed consistency models. Robustness corresponds to a correctness criterion that ensures the preservation of all properties that can be proved assuming strong consistency. We show that this property can be checked efficiently in several cases by linear reductions to state reachability problems.

• Marie-Paule Cani ‐ exposé invité ‐ (Laboratoire d'informatique de l'École polytechnique, CNRS & École polytechnique)

  Modélisation expressive des mondes virtuels : Nouvelles avancées en informatique graphique

  L'informatique graphique a vu récemment émerger des systèmes d'aide à la création 3D qui combinent des modèles géométriques contraints, exprimant des connaissances a priori, avec un contrôle gestuel inspiré du dessin ou de la sculpture. Etendre cette "modélisation expressive" à la synthèse de mondes virtuels complets - typiquement des terrains parcourus de cours d'eau et peuplés de myriades d'éléments comme des rochers ou des plantes, avec les contraintes de cohérence que cela implique - demande un passage à l'échelle difficile. Nous montrerons à travers une série d'exemples comment un contrôle interactif peut être entrelacé avec le maintien de la cohérence, et comment des outils issus de l'apprentissage statistique et de l'interpolation de distributions d'éléments peuvent être exploités pour peupler les paysages.

• Frédéric Chyzak (Inria Saclay) — Remplace un exposé initialement annoncé par Assia Mahboubi.
  

  Bijections par automates pour quelques modèles de marches combinatoires sur le réseau carré
  

  Dans le réseau Z², on s'intéresse aux marches de longueur n partant de l'origine et qui empruntent les pas Nord, Ouest et Sud-Est. On considère d'une part les marches confinées au plan des ordonnées positives et terminant sur l'axe des abscisses, et d'autre part les marches confinées aux quart de plan des abscisses et ordonnées positives. Pour tout n, il y a autant de marches de chaque nature. Il y a plusieurs façons d'établir ce résultat : une première approche consiste à expliciter le cardinal, identique, de ces deux classes ; une deuxième à identifier leur série génératrice, identique ; enfin, on exhibe classiquement une bijection tout à fait explicite entre les deux classes de marches. Dans cet exposé, on met en place un nouveau calcul de la bijection par le biais d'un automate réalisant une transduction. Le résultat se généralise dans diverses directions qui intéressent la combinatoire : la bijection obtenue se raffine en préservant des paramètres sur la position finale des marches ; une bijection analogue existe entre des modèles à 6 pas ; une autre bijection permet de considérer des modèles à pas plus longs.
  Exposé sur la base de travaux en cours avec A. Bostan, A. Mahboubi et K. Yeats.

• Jérémie Detrey (Laboratoire lorrain de recherche en informatique et ses applications, CNRS & Université de Lorraine & Inria Nancy Grand Est)

  Factoring integers with ECM on the Kalray MPPA-256 processor

  The Kalray MPPA-256 is a recent low-power chip which embeds 256 32-bit cores. As such, it can be used as an efficient co-processor for accelerating computations, bridging the gap between usual CPUs and the more throughput-oriented GPUs, all the while consuming far less power.
  In this talk, we will present a fast and energy-efficient implementation of the Elliptic Curve Method (ECM, an algorithm for factoring integers) on this platform. After a brief presentation of the ECM and of its important role in cryptanalysis, especially in the context of factoring RSA keys, we will glance at some of the key architectural features of the MPPA-256. We will then present an optimized library for multiprecision modular arithmetic, on top of which the ECM implementation was built, before concluding with a few benchmarks and comparisons with the state of the art.
  This is a joint work with Masahiro Ishii, Pierrick Gaudry, Atsuo Inomata, and Kazutoshi Fujikawa.

• Julie Digne (Laboratoire d'informatique en image et systèmes d'information, CNRS & INSA Lyon & Université Claude Bernard Lyon 1 & Université Lumière Lyon 2 & École Centrale de Lyon)

  Modélisation de formes par l'exploitation de similarités

  La plupart des surfaces d'objets numérisés présentent de fortes similarités, définies comme des répétitions ou de petites variations de motifs géométriques. Cette propriété est due à la matière des objets (pierre, bois...), aux outils d'usinage utilisés ou à une volonté artistique. Dans cet exposé, nous expliquons comment ces variations locales peuvent être détectées et exploitées dans le cadre de tâches classiques du traitement numérique de la géométrie, comme le débruitage, la compression ou le rééchantillonnage.

• Frédéric Dupuis (Laboratoire lorrain de recherche en informatique et ses applications, CNRS & Université de Lorraine & Inria Nancy Grand Est)

  Cryptographie quantique avec des appareils malicieux

  La mécanique quantique nous permet d'accomplir certaines tâches cryptographiques qui sont impossibles classiquement, comme par exemple générer une clé secrète entre deux participants seulement à l'aide d'un canal public. Or, ces protocoles quantiques supposent que les participants ont accès à des appareils qui fonctionnent exactement selon les spécifications. En pratique, une telle perfection est malheureusement difficile à atteindre. Pire : l'appareil pourrait même être fourni par un manufacturier malicieux tentant de briser le protocole pour son propre compte. Pour mitiger ce problème, des protocoles dont la sûreté peut être vérifiée seulement à partir du comportement observable des appareils ont été développés. La sûreté de ces protocoles dits « device independent » est cependant beaucoup plus difficile à démontrer. Dans cet exposé, je présenterai une nouvelle méthode permettant de borner la quantité d'aléa généré par un processus quantique à n étapes, et qui mène à des bornes de sécurité optimales pour plusieurs protocoles cryptographiques.
  Travail conjoint avec Rotem Arnon-Friedman, Omar Fawzi, Renato Renner et Thomas Vidick.

• Samuele Giraudo (Laboratoire d'informatique Gaspard-Monge, CNRS & Université Paris-Est Marne-la-Vallée & ESIEE Paris & École des Ponts ParisTech)

  Algebraic structures, series, and enumeration

  Endowing families of combinatorial objects (like words, permutations, or trees) with operations (like concatenation, shuffle, or grafting) leads to the construction of algebraic structures. The algebraic study of these structures highlights combinatorial properties of their underlying combinatorial objects. We present these ideas applied to many examples, including generalizations of formal power series with the aim to enumerate families of combinatorial objects.

• Russel Harmer (Laboratoire de l'Informatique du Parallélisme, CNRS & ENS Lyon & Université Claude Bernard Lyon 1 & Inria)

  Bio-Curation for Cellular Signalling: the KAMI Project

  The general question of what constitutes bio-curation for rule-based modelling of cellular signalling is posed. A general approach to the problem is presented, based on rewriting in hierarchies of graphs, together with a specific instantiation of the methodology that addresses our particular bio-curation problem. The current state of the ongoing development of the KAMI [Knowledge Aggregator & Model Instantiator] bio-curation tool, based on this approach, is detailed along with our plans for future development.

• Philippe Jacquet ‐ exposé invité ‐ (Nokia - Bell Labs)

  Joint Complexity with suffix and hyper-suffix trees

  The joint complexity has been introduced for DNA comparison and has been successfully applied to natural text sampling and clustering. It consists into enumerating the common factors between two texts without taking into consideration languages, grammars and vocabularies. Therefore it is extremely fast to compute via the use of suffix trees. The larger is the joint complexity the closer are the texts in meanings. It provides results at least as accurate as machine learning but without any training and at unprecedented speed. It has been successfully experimented on Twitter flows. Furthermore, it can be precisely analysed via combinatorics and generating functions when the text generation process are Markovian with finite memory. The process of text clustering can even again been accelerated via the use of hyper-suffix trees which have been recently invented. We have called this new branch of Artificial Intelligence which uses combinatorics and fast algorithms, the "accelerated AI". (The talk is based on joint work with Gerard Burnside.)

• Irène Marcovici (Institut Élie Cartan de Lorraine, CNRS & Université de Lorraine)

  Automates cellulaires et phénomènes d'auto-organisation : le rôle de l'aléa

  Les automates cellulaires sont des systèmes dynamiques pour lesquels le temps et l'espace sont discrets. Ils permettent de modéliser l'évolution d'un ensemble de composantes interagissant entre elles de manière locale : au cours du temps, chacune actualise son état en fonction de ce qu'elle perçoit de son voisinage.
  En étudiant certains automates cellulaires, on peut observer des phénomènes d'auto-organisation : à partir d'un état initial désordonné, les mises à jour successives des cellules par la règle locale conduisent à l'apparition d'une structure macroscopique.
  A l'inverse, si l'on souhaite parvenir à un certain comportement global, on peut chercher à concevoir une règle locale permettant de l'atteindre de manière décentralisée. J'exposerai différents problèmes de ce type (obtention de consensus, synchronisation, correction d'erreurs...), en étudiant l'influence que peut avoir l'introduction d'aléa dans les configurations initiales ou dans les dynamiques. La présentation sera inspirée de travaux communs avec Nazim Fatès.

• María Naya-Plasencia (Inria Paris)

  New Results on Quantum Symmetric Cryptanalysis

  The security of symmetric cryptography is completely based on cryptanalysis: we only gain confidence in the security of a symmetric primitive through extensive and continuous scrutiny. It is therefore not possible to determine whether a symmetric primitive might be secure or not in a post-quantum world without first understanding how a quantum adversary could attack it. In this talk we will provide an overview of the subject and present some recent results on symmetric quantum cryptanalysis: some attacks exploiting Simon's algorithm, quantization of some classical attacks, a new efficient quantum collision search algorithm and an analysis of the use of modular additions on symmetric primitives. We will discuss some implications of these results in quantum-safe symmetric cryptography.

• Michaël Rao ‐ exposé invité ‐ (Laboratoire de l'Informatique du Parallélisme, CNRS, ENS Lyon, Inria, Université Claude Bernard Lyon 1)

  Recherche exhaustive des pentagones convexes pavant le plan

  Quand on cherche à caractériser les formes convexes pouvant paver le plan (en s’autorisant les rotations et miroirs), seul le cas des pentagones restait ouvert. De 1918 à 2015, 15 différents types de pentagones pouvant paver le plan ont été découverts. Je présente une recherche exhaustive de tous les pentagones convexes pavant le plan, qui permet de clore cette question. La preuve se sépare en deux parties : la première montre, en utilisant la compacité, qu'on peut se limiter à un ensemble de 371 familles, et la seconde est une recherche exhaustive informatisée, pour chacune des 371 familles, qui ne trouve aucun nouveau type de pentagones que les 15 types connus.

• Pierre-Alain Reynier (Laboratoire d'Informatique et Systèmes, CNRS & Université d'Aix-Marseille & Université de Toulon)

  Register Minimisation of Streaming String Transducers

  Streaming String Transducers (SST) extend finite-state automata with registers, used to store partial output words. On each transition, these registers are updated using concatenation involving registers and constant output words. In this work, we focus on deterministic SST and consider the problem of register minimisation: given a SST, does there exist an equivalent SST with at most k registers?
  In this talk, I will present how to solve this problem for two subclasses of SST in which updates do not involve concatenation of registers. Our proof techniques rely on a generalisation of the twinning property, a property introduced by Choffrut in 1977. Our results also have consequences for (classical) finite-state transducers.

• Glynn Winskel ‐ exposé invité ‐ (University of Cambridge, Computer Laboratory)

  The true concurrency of Herbrand's theorem

  The brilliant French mathematician Jacques Herbrand died in 1931 in a mountaineering accident at the age of 23. Despite his youth he has two major theorems to his name. One is a foundational result in logic. Herbrand's Theorem is perhaps the first example of information being extracted from a formula in predicate calculus from the bare fact of its provability. In its simplest form his theorem states that if an existential formula of predicate calculus is provable then so is a disjunction got by instantiating its body with finitely many witnesses. More generally, Herbrand showed how an arbitrary formula in the predicate calculus is provable only if a quantifier-free disjunctive formula is provable. Herbrand's proof didn't work directly off the composition of the original formula. Indeed, it seems to be folklore that there is a problem in giving a compositional proof of Herbrand's Theorem. This is made precise by Kohlenbach who shows that one cannot hope directly to use collections of Herbrand witnesses for provable A and (A implies B) to give a collection for B. That leaves open the possibility of making some richer data compositional. In this talk I will sketch how it is useful to regard a classical proof as a distributed strategy. In this way we can obtain a compositional proof of Herbrand's theorem. The `true concurrency' in the title refers to the approach to distributed computation initiated by Carl Adam Petri; in modelling a proof as distributed computation we shall take careful account of the causal dependencies between events intrinsic to the proof. In effect, we exhibit the computational content of a classical proof as a distributed computation. (The talk is based on joint work with Aurore Alcolei and Pierre Clairambault at ENS Lyon, and Martin Hyland at the University of Cambridge.)

Exposés du 6 avril, en hommage à Maurice Nivat

• Pierre-Louis Curien (Laboratoire Preuves, Programmes et Systèmes, CNRS & Inria & Université Paris 7)

  Maurice : ses travaux, son action, sa marque

• Paul Gastin (Laboratoire Spécification et Vérification, CNRS & ENS de Cachan)

  Regular transducer expressions for two-way deterministic transducers

  Functional MSO transductions, deterministic two-way transducers, as well as streaming string transducers are all equivalent models for regular functions. We show that every regular function, either on finite words or on infinite words, captured by a deterministic two-way transducer, can be described with a regular transducer expression (RTE). RTEs are constructed from constant functions using the combinators if-then-else (deterministic choice), Hadamard product, and unambiguous versions of the Cauchy product, the 2-chained Kleene-iteration and the 2-chained omega-iteration.

• Catuscia Palamidessi (Inria Saclay / Laboratoire d'informatique de l'École polytechnique, CNRS & École polytechnique)

  Differential Privacy and Applications to Location Privacy

  In this talk, we review the notion of Differential Privacy, its implications in terms of Bayesian Adversary, and we discuss typical implementations from the point of view of their optimality with respect to utility. Then, we consider an extension of differential privacy to general metric domains, and the consequences for the optimality results. Finally, we show an instantiation to the case of location privacy, leading to the notion of geo-indistinguishability.

• Gérard Roucairol (Académie des technologies)

  Comment nous avons formalisé le parallélisme à travers la théorie des langages

• Laurent Vuillon (LAboratoire de MAthématiques, CNRS & Université de Savoie)

  Une approche informatique théorique des nombres de Markoff

  Nous allons revenir dans la première partie de l'exposé sur l'apport de Maurice Nivat aux pavages du plan et à la géométrie discrète. Nous évoquerons, bien sûr, le théorème de Beauquier-Nivat et ses nombreux prolongements en informatique théorique et algorithmique. Nous montrerons, ainsi, que Maurice aimait beaucoup faire de la recherche en géométrie discrète et en particulier coder des objets géométriques par des mots. Dans cet esprit et dans la seconde partie de l'exposé, nous montrerons comment le codage de segments discrets de la grille Z² et l'informatique théorique donnent de nouveaux outils pour attaquer la conjecture plus que centenaire de Frobenius sur les nombres de Markoff.