École Jeunes Chercheurs en Informatique Mathématique 2012

• François Coste (Inria, IRISA, Rennes)
• Jacques Nicolas (Inria, IRISA, Rennes)

Les séquences d'acides des macro-molécules biologiques principales (ADN, ARN et protéines) forment une source de données très importante en génétique et biologie moléculaire. Elles peuvent être étudiées en tant que mots finis sur un alphabet de 4 ou 20 lettres.

La connaissance que l'on possède sur certaines familles de molécules ou certains mécanismes se traduit alors en termes de langages formels. Par rapport aux approches traditionnelles du domaine qui sont plutôt statistiques, l'apport des langages est leur capacité de modélisation de structures porteuses d'information.

Outre une introduction rapide au domaine de la biologie moléculaire, le cours abordera plusieurs questions qui se posent dans ce cadre, avec un souci pratique né du besoin de rationaliser l'analyse de ce type de données :

1. Quelle classe de langages pour modéliser les ensembles de mots réellement observables ?
2. Étant donnée une séquence, peut on la compresser en se servant de la structure sous-jacente inconnue du langage ?
3. Étant donné un ensemble de séquences, peut-on inférer des langages les acceptant possédant un certain pouvoir prédictif ?

• Damien Eveillard (Univ. Nantes, LINA, Nantes) [Transparents du cours]
• Morgan Magnin (École centrale Nantes, IRCCyN, Nantes) [Transparents du cours]
• Olivier Roux (École centrale Nantes, IRCCyN, Nantes)

La recherche dans le domaine de la vérification des comportements dynamiques des systèmes complexes passe par une phase cruciale qui concerne la modélisation. Plusieurs approches permettent de représenter formellement ces mécanismes en faisant une abstraction de la réalité étudiée. L'informatique permet de s'appuyer notamment sur des modélisations discrètes pour effectuer des analyses du fonctionnement des systèmes. Un obstacle majeur est de prendre en compte un nombre souvent très important de paramètres qui restent difficiles à évaluer. L'introduction du temps, en particulier, pose un problème sérieux quand il est pris dans sa dimension chronologique et même une difficulté essentielle pour sa dimension chronométrique. Dans ce cours, nous chercherons à montrer les motivations pour la modélisation et notamment en étudiant les principes des modélisations discrètes et hybrides appliqués dans le domaine de la biologie, puis nous développerons un certain nombre d'approches qui sont faites pour l'analyse de ces modèles.

Le cours insistera sur trois dimensions directrices :

1. La justification des modèles choisis.
2. L'échelle temporelle des systèmes étudiés, qui peut être très variable, par exemple dans le domaine de la biologie.
3. La possibilité de prise en compte du temps (notamment dans les aspects de délais et de durées).

Le cours sera composé de quatre parties :

1. Importance (et spécificités) de la dynamique en biologie.
2. Modélisation par réseaux de Pétri (fondements, exemples, introduction du temps).
3. Modélisations hybrides (modèles discrets et vérification chronologiques, modèles temporisés et vérification chronométrique, exemples et limitations).
4. Modélisations algébriques et pi-calcul (introduction, frappes de processus, simulations stochastiques, exemples d'applications).

• Valérie Berthé (CNRS, LIAFA, Paris) [Transparents du cours]
• Jérémie Bourdon (Univ. Nantes, Lina, Nantes)
• Anne Siegel (CNRS, IRISA, Rennes)

Les systèmes dynamiques sont utilisés quotidiennement dans différents domaines scientifiques, en particulier sous leurs formes numériques qui consiste à modéliser le comportement d'un système à l'aide d'équations différentielles, d'en ajuster les paramètres en introduisant différentes observations temporelles, puis à prédire le futur du système à l'aide de méthodes de simulation. L'objectif de ce cours est de montrer que le champ d'application des systèmes dynamiques est en fait bien plus général que le domaine du numérique, dès qu'on combine des résultats profonds sur le comportement d'un système avec des approches discrètes issues de l'informatique (combinatoire, analyse d'algorithme).

Dans une première partie, on illustrera comment les concepts issus de la dynamique, en particulier celui de "trajectoire qualitative" apparaissent dans différents domaines scientifiques, en particulier en informatique. On illustrera les propriétés du système peuvent être déduites d'observations plus ou moins partielles sur le système, en insistant sur les différents théorèmes dont ces propriétés peuvent être déduites.

Dans la suite du cours, on se concentrera sur les utilisations concrètes de ces résultats. Ainsi, la seconde partie du cours portera sur la simulation effective (sur ordinateur) de systèmes dynamiques discrets, en particulier les dynamiques liées à des systèmes de numération. Nous nous concentrerons, entre autres, sur l'étude des orbites périodiques. Nous ferons, de plus, le lien entre trajectoires simulées et trajectoires réelles, et introduirons quelques éléments de théorie ergodique effective, à travers l'exemple de l'algorithme d'Euclide.

La troisième partie du cours illustrera comment l'analyse en moyenne de systèmes dynamiques permet de comprendre les propriétés de multiples algorithmes, dès qu'ils peuvent être décrits par un langage ad-hoc : division euclidienne par exemple, mais aussi alignements de séquences biologiques (en relation avec le premier thème de l'école) ou étude du comportement de systèmes biologiques (en relation avec le troisième thème).

• Sylvie Boldo (Inria, LRI, Orsay)
• Guillaume Melquiond (Inria, LRI, Orsay)

Nous confions à nos ordinateurs de nombreux calculs (météo, simulations aéronautiques, jeux vidéos, feuilles Excel...) et nous considérons naturellement que l'ordinateur fournira une réponse juste.

Malheureusement, la machine utilise une arithmétique dite flottante, qui a ses contraintes. Ainsi, chaque calcul est effectué avec un certain nombre de chiffres (souvent environ 15 chiffres décimaux) et donc chaque calcul peut créer une erreur, certes faible, mais qui peut s'accumuler avec les précédentes pour fournir un résultat complètement faux.

Ce cours montrera tout d'abord la façon dont l'ordinateur calcule, mais aussi comment compenser ou tirer partie de ces erreurs. Il présentera ensuite la notion de preuve formelle qui permet de s'assurer de la correction d'un théorème mathématique et de sa preuve. Avec cela, on pourra produire des preuves d'algorithmes qui utilisent l'arithmétique des ordinateurs.

• Michel Coste (Univ. Rennes 1, IRMAR, Rennes) [Transparents du cours]
• Guillaume Moroz (Inria, LORIA, Nancy)
• Laurent Busé (Inria, EPI Galaad, Sophia Antipolis)

Session organisée par Delphine Boucher et Marie-Françoise Roy.

Le calcul formel a pour objet d'étude les manipulations symboliques effectives d'objets mathématiques. Il se situe à l'interface des mathématiques, de l'informatique et de différents domaines d'applications. Les thématiques mathématiques abordées par le calcul formel sont développées à la fois du point de vue de l'effectivité et de la complexité. D'autre part, les logiciels issus du calcul formel ont trouvé leur place dans de nombreux domaines.

Dans cette session dédiée au calcul formel, seront abordées des thématiques liées à la théorie de l'élimination pour les systèmes polynomiaux paramétrés ou non. Les domaines d'applications visés sont la modélisation géométrique et la robotique. En particulier, les problèmes de robotique abordés seront: planification de mouvement de robots, cinématique des robots parallèles et analyse de leurs singularités. On verra comment le calcul formel, notamment les algorithmes de géométrie algébrique réelle (carte routière, décomposition cylindrique algébrique) peuvent intervenir pour traiter ces problèmes. On parlera des limites de cette approche et de l'importance du choix de la modélisation pour traiter les problèmes.

Dans le cours de Guillaume Moroz, on abordera les liens entre la conception de robot et des notions classiques de géométrie algébrique réelle. La conception d'un mécanisme robotique tient compte de propriétés spécifiques. Le robot que l'on conçoit a-t-il des singularités parallèles ? Sérielles? Est-il cuspidal? Après avoir vu l'intérêt de ces propriétés en robotique, nous verrons comment ces notions peuvent se traduire géométriquement en termes de revêtement analytique et de multiplicité d'un point dans un idéal. Nous nous intéresserons aussi au problème de la conception d'un robot satisfaisant des propriétés spécifiées a priori.

Le cours de Laurent Busé portera sur la Représentation matricielle des courbes et surfaces algébriques paramétrées. La détermination des lieux d'intersections et des lieux singuliers associés à des courbes et des surfaces algébriques paramétrées est d'une importance capitale en modélisation géométrique. Après une courte introduction sur cette problématique, on proposera une nouvelle représentation de ces courbes et surfaces paramétrées. Cette dernière consiste essentiellement à caractériser un objet algébrique par la chute de rang d'une matrice plutôt que par l'annulation simultanée d'une famille de polynômes. Dans un deuxième temps, on montrera comment ces représentations, que l'on qualifiera de matricielles, permettent de traduire des problèmes géométriques en des problèmes d'algèbre linéaire classiques. En particulier, nous montrerons la contribution de cette approche aux problèmes d'intersections mentionnés en introduction.

Motivés par des applications en bio-informatique, nous étudions le problème du collectionneur de mots, i.e., le nombre moyen d'appels à un générateur aléatoire de mots d'un certain langage avant que la collection soit complète. L'originalité de cette instance du collectionneur de coupons non-uniformes réside dans la potentiellement grande multiplicité du nombre de mots d'une probabilité donnée.

La dystrophine est une protéine du cytosquelette, constituée d'un long domaine central, dans lequel 24 répétitions en faisceaux d'hélices alpha sont reliées en tandem. De nos jours, il n'existe toujours pas de modèle tout atome de cette région. La méthode de diffusion aux petits angles des rayons X (SAXS), à partir de laquelle des enveloppes moléculaires 3D sont générées, peut être combinée à un modèle gros grain (coarse-grained model), afin de relier différents niveaux de résolution. Nous proposons divers protocoles d'alignement des deux méthodes pour ainsi produire le premier modèle atomique du domaine central de la dystrophine.

Mots clés : Dynamique moléculaire, Dystrophine, Modèle gros grain, SAXS.

Les automates finis sont parmi les modèles de calcul les plus simples. Il en existe de nombreuses variantes : déterministe, nondéterministe, unidirectionnel, bidirectionnel... Du point de vue puissance de calcul, tous reconnaissent exactement les langages rationnels. Mais si l'on regarde la "taille" (souvent le nombre d'état) de ces modèles, il apparait des différences, certains se révèlent être beaucoup plus succints que d'autres. Au début des années 80, Sakoda et Sipser ont soulevé la question, toujours ouverte, du nombre d'état requis par un automate bidirectionnel déterministe pour simuler l'analogue nondéterministe. Il est conjecturé une séparation exponentielle entre ces deux modèles. Nous apportons ici une nouvelle approche de la question, en augmentant la puissance des automates bidirectionnels déterministes en ajoutant la possibilité de réaliser des choix nondéterministes uniquement en bordure du mot d'entrée. Nous construisons alors une réduction sous-exponentielle (polynomiale sous l'hypothèse L=NL) de ce modèle vers le cas bidirectionnel déterministe.

When the set of possible states of a system is finite, its behavior and its specification can be modeled by finite automata. Against, when the domain system is infinite, its verification is in general unreliable. Therefore, automatic verification of systems over infinite domain requires an extension of finite alphabet automata and regular models. The study of the theories of the finite words over infinite alphabet have been considered in database theory and many other typical application in control systems with an infinite data source. Current research is focused in identifying and adding some interesting properties whose verification in infinite systems is possible. The aim of this talk is to show the automaticity of the clone structure over a denumerable infinite alphabet. It allows us to deduce the decidability of more expressive theories.

La modélisation en agronomie permet d'économiser du temps et de l'argent et peut également être un bon outil d'aide à la décision. Le but de modéliser une ferme laitière est de pouvoir comprendre ou de prévoir l'impact de différentes stratégies de nutrition ou de différentes races d'animaux sur l'économie de la ferme et les gaz à effet de serre produits. Le modèle est développé en C/C++, individu centré avec pour pas de temps la journée. Tous les animaux sont modélisés depuis la naissance jusqu'à la sortie de la ferme en passant par les différentes étapes de leur vie : phase de croissance, de lactation, d'engraissement.

L'intérêt de modèles agronomiques est d'éviter un investissement (temporel tout comme monétaire) pour tester une conduite de ferme qui pourrait ne pas être avantageuse. En termes de croissance d'herbe à but de nutrition de vaches laitière, l'intérêt d'un modèle est de simuler la production d'herbe sur une année pour optimiser son utilisation dans l'alimentation des animaux. Le modèle final produit tiendra compte de la qualité des sols de l'exploitation (drainage, quantité de nutriments), des facteurs environnementaux (ensoleillement, pluie, température) ainsi que du management de l'exploitation (présence d'animaux sur les parcelles, fertilisation). Ce modèle sera ensuite joint avec le modèle global d'une ferme laitière développé par Elodie Ruelle.

Les techniques de criblage à haut débit pour la recherche de marqueurs biologiques sont de plus en plus utilisées notamment en bio-industries. Néanmoins l'interprétation des données générées par ces techniques reste un défi permanent. Dans ce travail nous présentons une nouvelle méthode d'analyse d'une biopuce musculaire du porc et nous la confrontons à des méthodes existantes. Il s'agit d'une méthode de clustering basée sur l'annotation fonctionnelle des gènes. Les méthodes statistiques que nous avons testées sur la puce donnent des résultats assez hétérogènes et difficilement interprétables. Néanmoins en se basant sur les données de l'ANOVA on peut dire que nous avons trois grands clusters SM1 et SM2 appartenant au muscle semi-membraneux et LD appartenant à la longe. Un outil développé localement basé sur le calcul de la similarité sémantique a été utilisée dans deux contextes. Nous l'avons utilisé d'une part pour regrouper les clusters similaires parmi les 48 gènes par DAVID après filtrage (19 pour SM1 et 29 pour SM2) cela nous a permis d'identifier la transcription et sa régulation comme clusters spécifique à SM2. Nous l'avons utilisé d'autre part pour générer 6 clusters fonctionnels pour SM1 et 5 pour SM2. La transcription apparaît bien dans deux groupes similaires de formant un groupe spécifique de SM2, mais également dans deux clusters de SM1.

Mots clés : Annotation fonctionnelle, distance, similarité, cluster

Les modèles mathématiques et informatiques permettent aujourd'hui une grande qualité dans la modélisation du monde du vivant.

Dans cet exposé, nous verrons une description d'un modèle appelé "réseau métabolique" ainsi que les problèmes posés par cette classe de modèles. La création d'un tel modèle utilise habituellement des principes basés sur l'optimisation linéaire. Nous étudierons l'intérêt de construire et d'étudier ce modèle en utilisant la programmation logique. Une telle approche permet de s'affranchir des contraintes fortes liées à l'optimisation linéaire et d'intégrer des connaissances biologiques dans la construction du modèle.

La signalisation cellulaire est un processus biologique essentiel qui permet à une cellule de réagir de façon adaptée à un ligand. Il est généralement décrit par l'activation successive de protéines, orientée de la membrane au noyau où des gènes cibles sont régulés. Un même type de récepteurs pouvant activer plusieurs voies de signalisations enchevêtrées, la signalisation cellulaire est considérée comme un système complexe. La création de modèles formels discrets est nécessaire à la compréhension globale de tels mécanismes. Le choix du formalisme est conditionné notamment par les données disponibles et les questions biologiques. Dans ce contexte, le formalisme de transitions gardées semble bien adapté aux faits biologiques décrivant des réseaux de signalisations. Nous avons développé CADBIOM (Computer Aided Design of BIOlogical Models), un logiciel qui permet de concevoir, simuler et questionner un modèle. Ces différentes caractéristiques seront présentées à travers l'exemple du TGF-beta. En conditions physiologiques, ce ligand régule l'homéostasie des cellules et bloque le cycle cellulaire. En revanche il est aussi impliqué dans des pathologies où il à un rôle opposé, favorisant la prolifération et la mobilité des cellules. La compréhension de ces différents effets est une étape primordiale pour l'identification de cibles thérapeutiques.

We consider a homogeneous function V and the associated dynamical system $\ddot{q}=-\nabla V(q)$. One of the most interesting property of such system is integrability, meaning the existence of some functions $I(q,\dot{q})$ called first integrals such that $\dot{I}=0$. We are interested in an algorithm capable of either finding a first integral or proving that such a function does not exist, using two different approaches. We present the various difficulties that arise in such a problem, in particular the proof that such an algorithm always terminate and some efficiency questions.

In this work we ask whether each local-in-time execution of a continuous-time system can be extended to a global-in-time execution. We study this question on the abstract level for a large class of systems (nondeterministic complete Markovian systems). We show that it can be answered using only independent local analysis of system's executions (in a neighborhood of each time moment).

La combinatoire analytique s'intéresse à des famille d'ojets indexés par leur taille. À chaque famille est associée une série génératrice : c'est la série formelle dont le n-ième terme est le nombre d'objets de taille n. Certaines opérations combinatoires sur les familles (comme l'union disjointe et le produit cartésien) correspondent à des opérations sur la série génératrice (comme la somme et le produit). Ainsi, une description combinatoire des familles se traduit par une équation sur leur série génératrice. On extrait ensuite de cette équation l'expression exacte ou asymptotique des coefficients.

Par exemple, notons c_n le nombre d'arbres binaires ayant n noeuds et C(z) la série génératrice correspondante. Comme un arbre binaire est soit un noeud seul, soit un noeud et ses deux fils, qui sont eux-mêmes des arbres binaires, on obtient l'équation combinatoire "arbre binaire = (noeud) OU (noeud ET arbre binaire ET arbre binaire)".

En traduisant "noeud" par "z", "arbre binaire" par "C(z)", "OU" par "+" et "ET" par "*", on en déduit que la série C(z) vérifie l'équation C(z) = z + z * C(z) * C(z).

On peut résoudre cette équation et obtenir l'expression de C(z), puis prendre son développement de Taylor. Les c_n sont les nombres de Catalan dont l'expression est c_n = binom(2n, n) / (n+1).

D'autre part, sans résoudre l'équation, une étude de singularité permet d'obtenir la formule asymptotique c_n ~ 4^n n^{-3/2} / rac(pi).

Pour n'importe quel langage L, nous allons considérer la série génératrice bivariée F(z,u) = \sum_{n\geq 0} \sum_{k=0}^n f(n,k) u^k z^n où f(n,k) est le nombre de mots de longueur n avec k occurrences d'un motif préalablement fixé. À chaque grammaire engendrant L est associée un graphe de dépendance où chaque non terminal devient un sommet qui est relié aux non terminaux qui interviennent dans ses règles de production.

En ce qui concerne les grammaires régulières (i.e., les automates), la série génératrice est rationnelle. Si le graphe de dépendance est fortement connexe, alors le comportement asymptotique des coefficients f(n,k) et la loi limite associée sont connus. Nous allons compléter ces résultats en donnant les lois limites atteignables lorsque le graphe de dépendance est non fortement connexe.

En ce qui concerne les grammaires algébriques, la série génératrice est... algébrique. Si le graphe de dépendance est fortement connexe, alors le théorème de Drmota-Lalley-Woods fournit le comportement asymptotique des coefficients f(n,k) et la loi limite associée. Nous exhibons les comportements asymptotiques atteignables dans le cas d'un graphe de dépendance non fortement connexe.

Il s'agit de réaliser une analyse précise et réaliste de la complexité des principaux algorithmes de texte sur des mots produits aléatoirement par une source. Cette étude fine consiste à étudier le nombre de comparaisons entre symboles réalisées par les algorithmes, les symboles étant les constituants élémentaires des clés (dont les études classiques comptent le nombre de comparaisons, ce qui est plus grossier). L'étude d'une source et des principales structures de données associées repose sur sa série de Dirichlet; en l'occurrence, il est essentiel d'en étudier la discipline, c'est-à-dire de trouver une région à gauche de sa singularité dominante, où elle est analytique et de croissance polynomiale.

La correspondance de Curry-Howard permet d'associer un programme informatique à une preuve mathématique. Ainsi, on peut donner un contenu calculatoire à des preuves qui semblent ne pas en avoir. En outre, les programmes ainsi extraits à partir de preuves sont corrects par construction : ils ne peuvent pas contenir de bugs. Néanmoins, cette correspondance ne traite que les preuves dites constructives, desquelles sont bannis certaines formes de raisonnement comme le raisonnement par l'absurde. La réalisabilité classique permet de dépasser cette limitation mais en introduit une autre : tous les programmes ne donnent plus forcément des réponses correctes. On verra donc comment contourner ce problème et quelles en sont les conséquences sur un exemple concret : les nombres réels.

Les protocoles de populations sont un modèle de calcul distribué modélisant de vastes réseaux de faibles agents. Le modèle classique a une puissance de calcul très limitée, mais il est possible en faisant un peu varier le modèle de l'augmenter considérablement. En limitant les communications, il est possible d'obtenir la puissance de certaines machines de Turing.

Based on our previous research on reconfiguration management for seamless PHY (and other) layer adaptation on heterogeneous platforms (made of GPP, DSP, FPGA), we have derived a management architecture that matches cognitive radio requirements. It can be used indeed for any application, beyond cognitive radio context, that requires real-time auto-adaptivity. We have called the management architecture HDCRAM that stands for Hierarchical and Distributed Cognitive Radio Architecture Management. HDCRAM is a set of blocks and the rules associated to connect these blocks (connections and messages). The goal of using HDCRAM is to benefit from the necessary infrastructure to be added to pure signal processing application (radio signal processing or anything else for other layers) so that the application can be ubiquitously changed whatever the nature of the underlying processing units (e.g. DSP, FPGA, ASIC, GPP, etc.). This set of rules for the management architecture has been formalized in the HDCRAM metamodel.

Dans cet exposé nous présentons le contexte d'utilisation des courbes elliptiques en cryptographie. Nous introduisons ensuite les couplages qui sont des applications bilinéaires définies sur les sous-groupes du groupe des points d'une courbe elliptique. Nous présentons quelques applications des couplages en cryptographie. Nous terminons en présentant nos recents résultats sur un exemple de calcul de couplages sur un modèle special des courbes elliptiques de Jacobi.

Le calcul de la clôture intégrale d'un anneau de nombres (i.e., de l'ordre maximal d'un corps de nombres) est bien connu (cf l'algorithme Round 2 de Zassenhaus ou l'algorithme Round 4). Dans cet exposé, on développera une nouvelle approche de calcul, basée sur l'inversibilité de certains idéaux de l'anneau de nombres en question.

Après avoir défini les surfaces de Kummer, je présenterai les fonctions thêta et plus particulièrement les relations de Riemann. Ces relations permettent d'obtenir des formules efficaces sur les surfaces de Kummer. Nous montrerons comment poser le problème du logarithme discret sur les surfaces de Kummer. Ce qui est une brique fondamentale de la cryptographie asymétrique.

Cet exposé presentera une nouvelle méthode pour trouver des familles de courbes elliptiques adaptées à l'algorithme de factorisation ECM, c'est-à-dire des familles ayant de bonnes propriétés de torsion lorsque l'on réduit les courbes modulo un premier p. Cette méthode sera expliquée sur un exemple concret qui a permis d'obtenir des familles qui offrent des performances comparables, et même meilleurs dans certains cas, à l'implémentation de référence GMP-ECM.

Since 1985, the IEEE 754 standard defines formats, rounding modes and basic operations for floating-point arithmetic. In 2008 the standard has been extended, and recommendations have been added about the rounding of some elementary functions such as trigonometric functions (cosine, sine, tangent and their inverses), exponential, and logarithm. However to guarantee the exact rounding of these functions one has to approximate them with a sufficient precision. Finding this precision is known as the Table Maker's Dilemma. To determine this precision, it is necessary to find the hardest-to-round argument of these functions.

Lefèvre et al. proposed in 1998 an algorithm which improves the exhaustive search by computing a lower bound on the distance between a line segment and a grid. In this presentation, we will provide an improvement of this algorithm and show how to take advantage of massively parallel architectures (especially GPUs) for such computations. This enables a speed up of 52x on a NVIDIA Fermi GPU over one single high-end CPU core.

Les surfaces médiatrices sont des constructions géométriques qui sont très fréquentes dans divers domaines tels que: Tool Path Generation, Voronoï Diagram, Motion Planning, NC-milling, etc.

Pour deux surfaces paramétriques de degré petit, il sera présenté une nouvelle approche pour déterminer une représentation algébrique de leur médiatrice en utilisant la règle généralisée de Cramer et une élimination appropriée. La nouvelle approche introduite permet d'obtenir facilement un paramétrage de la médiatrice dans les cas de : quadrique et plan, quadrique et cylindre et tore et cylindre. La médiatrice est rationnelle dans la plupart des cas. Dans quelques cas le paramétrage implique des racines carrées, ce qui est bien adapté pour les méthodes d'approximation.