• Summary
• LIFO Members (Directory)
• Research Teams
• CA
• GAMoC
• LMV
• Pamda
• SDS
• Research Actions
• Doctoral Research
• Seminars and Events
• Seminars (french)
• Events at LIFO
• Events out of LIFO
• Publications and Software
• Publications
• Doctoral and Habil. Theses
• Research Reports
• Software
• Technology transfer

• Contacts/Reaching LIFO
• Who's who at LIFO
• Coming to LIFO
• Teaching
• CS Department
• CS Technical Department
• INSA Centre-Val de Loire

Contact

LIFO - Bâtiment IIIA
Rue Léonard de Vinci
B.P. 6759
F-45067 ORLEANS Cedex 2

Email: contact.lifo
Tel: +33 (0)2 38 41 99 29
Fax: +33 (0)2 38 41 71 37

LIFO seminars (french)

08/12/2008 : Vérification symbolique et structures partagées
Duy Tung NGuyen (LIFO) Résumé

26/11/2008 : Extraction d'information et analyse d'opinion pour l'aide à la recommandation.
Poirier Damien (France Telecom Lannion) Résumé
Attention : 10 Heure salle réunion 1

24/11/2008 : Problèmes de satisfaction et d'optimisation de contraintes quantifiées
Jérémie Vautard (LIFO) Résumé

17/11/2008 : Dualité et largeurs de décompositions
Frédéric Mazoit (Labri Bordeaux) Résumé

03/11/2008 : From Philosophical to Industrial Logics
Moshe Y. Vardi (Rice university) Résumé
Attention : AMPHI H

13/10/2008 : Reconstruction de surfaces par LP-Fitting
Thibaut Marzais (LIFO ) Résumé

29/09/2008 : Des types et des effets pour la sécurité C
David Teller (LIFO) Résumé

30/06/2008 : Analyse de la complexité des programmes par interprétation sémantique
Romain Pechoux (LORIA Nancy) Résumé

19/05/2008 : Quatum Computing
Fanming Song (Université de Nanjing) Résumé

30/04/2008 : Authentification biométrique adaptative: Application à la dynamique de frappe et à la signature manuscrite
Sylvain Hocquet (Université François Rabelais de Tours) Résumé
Attention : 14h à l'Ensi de Bourges salle CRI03

28/04/2008 : Méta-heuristiques pour la résolution de problèmes d'ateliers de production
Geoffrey Vilcot (Laboratoire d'Informatique de Tours) Résumé

21/04/2008 : Graph searching on some graph classes
Rodica Mihai (University of Bergen - Norvège) Résumé

07/04/2008 : Construction algébrique de graphes
Luc Gillibert (LORIA Nancy) Résumé

07/04/2008 : Aspects dynamiques de XML: Évolution des schémas
Mírian Halfeld Ferrari Alves (Université François Rabelais de Tours) Résumé
Attention : 15H

31/03/2008 : Couverture de graphes et complexité algebrique
Laurent Lyaudet (LIFO Orléans) Résumé

17/03/2008 : Apprentissage dans les réseaux sociaux
Emmanuel Viennet (LIPN Paris 13) Résumé

10/03/2008 : Programmation générative & Architecture parallèle : Vers une méthodologie pour la génération systématique d'outils de développement
Joel Falcou (Institut d'Electronique Fondamentale - Université Paris-Sud Orsay) Résumé

03/03/2008 : Algorithmes exacts pour une généralisation du problème de la domination d'un graphe
Mathieu Liedloff (Université Paul Verlaine - Metz) Résumé

25/02/2008 : Automates cellulaires et universalité
Guillaume Theyssier (laboratoire de mathématiques de l'Université de Savoie) Résumé

25/02/2008 : Analyse d'atteignabilite en réécriture pour la vérification de systèmes infinis.
Yohan Boichut (LORIA) Résumé
Attention : 15H

11/02/2008 : Problèmes de décision et d'évaluation en complexité algébrique
Sylvain Perifel (ENS Lyon) Résumé

07/02/2008 : Généralisation aux systèmes multi-patch des méthodes de calcul du taux de reproduction de base pour des modèles épidémiologiques de type SIRS.
Maurice Tchuente (ENS Lyon) Résumé
Attention : C EST UN JEUDI A 10h15

04/02/2008 : Calcul et exploitation de recouvrements acycliques pour la résolution de (V)CSP
Samba Ndojh Ndiaye (LSIS Marseille) Résumé

28/01/2008 : Extraction et formalisation de la sémantique des liens hypertextes dans des documents culturels, scientifiques et techniques.
Moustafa Al Hajj (LIFO Orléans) Résumé

21/01/2008 : Réactivité efficace pour le pi-calcul synchrone.
Frédéric Dabrowski (INRIA) Résumé

14/01/2008 : Abstraction in Representation and Learning
Lorenza Saitta (LIFO Orléans) Résumé

Résumés des séminaires

Vérification symbolique et structures partagées Duy Tung NGuyen, LIFO
Dans les années 90, les industries des composants électroniques, dans leur recherche d'outils pour améliorer le niveau de confiance de leurs produits, ont adopté les diagrammes de décisions binaires (BDD) pour traiter des composants de plus en plus complexes. Les BDD sont des structures codant des fonctions booléennes. Ils peuvent être vus comme des arbres où les états représentent des choix de valeurs de variables booléennes, un ordre total sur les variables garantit l'unicité du codage d'une fonction. Les techniques de partage de structures, combinées à des méthodes de réductions, conduisent à des implémentations extrêmement efficaces en pratique. Ainsi, des vérifications exhaustives ont pu être réalisées sur des systèmes comprenant des milliards d'états. Le pouvoir d'expression des BDD est suffisant pour manipuler une grande classe de systèmes finis. De plus, certains systèmes dynamiques peuvent être pris en compte avec ce type de techniques. Comme le nombre de variables des systèmes étudiés est un facteur critique, de nombreuses structures "à la BDD" ont été proposées. D'autres structures ont plutôt cherché à étendre le domaine d'application de ces techniques. Dans le cadre de projets industriels, nous avons conçu une nouvelle structure à la BDD, les Diagrammes de Décisions de Données (DDD). Notre objectif était de fournir un outil flexible qui peut être autant que possible adapté pour la vérification de tout type de modèles et qui offre des capacités de traitement similaires aux BDD. A la différence des BDD, les opérations sur nos structures ne sont pas prédéfinies, mais une classe d'opérateurs, appelée homomorphismes, est introduite pour permettre à un utilisateur de concevoir ses propres opérations. Dans ce modèle, les variables ne sont pas booléennes ; elles prennent leurs valeurs dans des domaines non nécessairement bornés. Une autre caractéristique intéressante est qu'aucun ordre sur les variables est présupposé dans la définition. De plus, une variable peut apparaître plusieurs fois dans un même chemin. Cette propriété est très utile quand on manipule des structures dynamiques comme les files. Les Diagrammes de Décisions de Données Hiérarchique (Tree Data Decision Diagrams, TDDD) ont les même idées comme DDD mais grâce aux structures hiérarchiques, ils sont plus compacts. Les opérations que nous avons définies ce basent sur la théorie de la récriture de termes pour assurer la terminaison des modèles en certains cas ainsi que pour améliorer l'interface de conception des modèles. Nous avons implémenté sous forme un outil et testé avec le modèle de correction automatique des mots. De plus, nous allons développer des méthodes de transformation automatique d'un système de la récriture de termes vers l'autre plus efficace.

Extraction d'information et analyse d'opinion pour l'aide à la recommandation. Poirier Damien , France Telecom Lannion
Le domaine d'étude est l'extraction d'Information. Le sujet concerne la transformation de données textuelles non structurées en données structurées et exploitables par des systèmes de recommandations. Deux grandes catégories d'informations sont utilisées dans ce type de moteurs : les données de description de contenus comme les acteurs, le réalisateur ou le genre pour les films, et les données d'usage qui peuvent être par exemple des notes sur les produits consommés ou encore des pages internet visitées. Avec l'émmergence du Web 2.0, les internautes sont de plus en plus amenés à partager leurs sentiments, opinions, expèriences sur des produits, personnalités, films, musiques, etc (par exemple sous forme de commentaires). Ces données textuelles produites par les utilisateurs représentent potentiellement des sources d'informations riches qui peuvent être complémentaires aux données exploitées actuellement par les moteurs de recommandation et peuvent donc ouvrir de nouvelles voies d'études dans le domaine de la recommandation en ligne. Notre objectif dans le cadre de la thèse est de produire, à partir des commentaires issus des forums, des matrices d'entrées pertinentes pour les systèmes de recommandations. L'idée sous jacente est de pouvoir enrichir un système de recommandation pour un service débutant, qui possède encore peu d'utilisateurs propres, et donc peu de données d'usage, par des données issues d'autres utilisateurs.

Problèmes de satisfaction et d'optimisation de contraintes quantifiées Jérémie Vautard, LIFO
Les problèmes de satisfaction de contraintes quantifiées (QCSP) sont une extension des problèmes de satisfaction de contraintes dans laquelle certaines des variables peuvent être quantifiées universellement. Un tel formalisme permet de représenter de manière compacte des jeux à deux joueurs ("Existe-t-il un coup tel que pour tout coup de mon adversaire, il existe un coup tel que pour tout coup de mon adversaire ..... tel que je gagne ?") ou, plus généralement, toute une classe de problème dans lesquels certains paramètres ne sont pas contrôlables (par exemple, la réalisation d'un projet en présence d'un ennemi ayant pour objectif de l'empêcher). Après avoir présenté les limitations du formalisme "classique" des QCSP, j'exposerai mes travaux sur deux extensions de ce cadre : d'une part, les QCSP+, permettant de modéliser aisément des problèmes non-triviaux ; et d'autre part la version "optimisation" de ces problèmes : les QCOP+, permettant de représenter et de résoudre des problèmes d'optimisation multi-niveaux non-linéaires.

Dualité et largeurs de décompositions Frédéric Mazoit, Labri Bordeaux
Il existe dans la littérature un grand nombre de décomposition similaire aux décompositions arborescentes des graphes. L'immense majorité d'entre elles sont associées à des obstructions. Ces objets sont des obstructions au sens où il existe une décomposition si et seulement si il n'existe pas d'obstruction. Jusqu'à récemment, chacun de ses théorèmes de « dualité » nécessitait une preuve ad-hoc. Au cours de ce séminaire, J'utiliserai le cas de la dualité entre largeur arborescente et bramble pour présenter un cadre général qui permet de donner une démonstration unifiée de tous les théorèmes ad-hoc de ce type connu à ce jour.

From Philosophical to Industrial Logics Moshe Y. Vardi, Rice university
One of the surprising developments in the area of program verification is how several ideas introduced by logicians in the first part of the 20th century ended up yielding at the start of the 21st century industry-standard property-specification languages called PSL and SVA. This development was enabled by the equally unlikely transformation of the mathematical machinery of automata on infinite words, introduced in the early 1960s for second-order arithmetics, into effective algorithms for industrial model-checking tools. This talk attempts to trace the tangled threads of this development.

Reconstruction de surfaces par LP-Fitting Thibaut Marzais, LIFO
La modélisation est un domaine qui est devenu primordial dans l'informatique graphique de nos jours. On peut modéliser des objets par des nuages de points, des maillages ou des surfaces de type surfaces paramétrées. Je présente aujourd'hui mon travail de thèse, qui regroupe la chaine complète de reconstruction allant du maillage à un ensemble de surfaces paramétrées. Ce processus fait intervenir plusieurs techniques comme la segmentation de maillages, la paramétrisation et le fitting. Nous avons à plusieurs developpé une technique de quadrangulation, mais avec un cadre de travail adapté. Les M-tuiles et les M-pavages permettent d'englober toutes les informations nécessaires lors de la segmentation, lorsqu'on applique des techniques de pavage/découpage sur le maillage. L'algorithme de fitting présenté est nouveau, prenant en compte une norme uniforme en lieu et place de la norme euclidienne dominante, permettant ainsi l'utilisation d'un programme linéaire pour le résoudre. Une étude des critères de recollement de surfaces est faite, avec des contraintes linéaires incluses très facilement au programme linéaire, et une autre étude sur les différents cas possibles de régularité choisie.

Des types et des effets pour la sécurité C David Teller, LIFO
Dans le domaine de la sécurité, l'une des tâches les plus difficiles est de déterminer quels effets l'exécution d'un programme peut avoir sur le système cible. Si de nombreux outils permettent de déterminer ces effets durant l'exécution (analyse dynamique) ou après l'exécution du programme (analyse de traces), l'extraction de ces effets avant l'exécution (analyse statique d'effets) est largement ignorée, en particulier dans les logiciels écrits dans des langages proches du système. Or, le support théorique pour ce genre de choses est là, ou presque. Une petite pincée de types dépendants, deux grosses cuillers de types avec effets, un peu d'interprétation abstraite et un bon effort de modélisation permettent de déterminer statiquement l'ensemble des appels systèmes effectués par un programme -- et surtout de déterminer qui est visé par ces appels. Au cours de l'exposé, nous présenterons brièvement les modèles de sécurité Unix et SELinux, qui nous servent de référence, puis quelques éléments des théories mentionnées, pour conclure par le logiciel sur Extrapol, qui permet d'analyser des fichiers sources C pour en déduire leurs effets sur le système.

Analyse de la complexité des programmes par interprétation sémantique Romain Pechoux, LORIA Nancy
Il existe de nombreuses approches développées par la communauté de la Complexité Implicite permettant d'analyser les ressources nécessaires à la bonne exécution des algorithmes. Nous nous intéressons plus particulièrement au contrôle des ressources à l'aide d'interprétations sémantiques. Après avoir rappelé brièvement la notion de quasi-interprétation ainsi que les différentes propriétés et caractérisations de classes de complexité polynomiales qui en découlent, nous présentons les différentes avancées obtenues dans l'étude de cet outil : nous étudions le problème de la synthèse qui consiste à trouver une quasi-interprétation pour un programme donné, puis, nous abordons la question de la modularité des quasi-interprétations. La modularité permet de diminuer la complexité de la procédure de synthèse et de capturer un plus grand nombre d'algorithmes. Après avoir mentionné différentes extensions des quasi-interprétations à des langages de programmation réactif, bytecode ou d'ordre supérieur, nous introduisons la sup-interprétation. Cette notion généralise la quasi-interprétation et est utilisée dans des critères de contrôle des ressources afin d'étudier la complexité d'un plus grand nombre d'algorithmes dont des algorithmes sur des données infinies ou des algorithmes de type "diviser pour régner". Nous combinons cette notion à différents critères de terminaison comme les ordres RPO, les paires de dépendance ou le size-change principle et nous la comparons à la notion de quasi-interprétation. En outre, après avoir caractérisé des petites classes de complexité parallèles, nous donnons quelques heuristiques permettant de synthétiser des sup-interprétations sans la propriété sous-terme, c'est à dire des sup-interprétations qui ne sont pas des quasi-interprétations. Enfin, nous adaptons les sup-interprétations à des langages orientés-objet, obtenant ainsi différents critères pour contrôler les ressources d'un programme objet et de ses méthodes.

Quatum Computing Fanming Song, Université de Nanjing

Authentification biométrique adaptative: Application à la dynamique de frappe et à la signature manuscrite Sylvain Hocquet, Université François Rabelais de Tours
Depuis le 11 septembre 2001, le monde connaît une demande toujours plus importante en termes de sécurité. Au départ, cette demande s’exprimait à l’échelle des états : contrôle aux frontières, lutte anti-terroriste, contrôle de l’immigration… Mais, cette exigence de sécurité s’est vite étendue à la vie de tous les jours. La protection des données personnelles informatiques est d’ailleurs une problématique critique pour l’avenir du développement d’Internet, que ce soit pour le commerce électronique, les courriels ou les autres applications en ligne... Mais, malgré cette importante nécessité de sécurité, beaucoup d’entreprises ou de particuliers ne sont pas prêts à investir tant sur le plan financier que sur celui de l’effort à fournir pour assurer cette sécurité. Pour répondre à ces nouveaux besoins, la biométrie semble être une solution pratique, efficace et dont les coûts en effort et en argent sont en constante diminution, mais restent conséquents. Une branche de la biométrie : la biométrie comportementale permet de limiter ces contraintes. Elle comporte néanmoins de nombreux inconvénients : la résolution de problèmes à une classe, l’évolution des caractéristiques des utilisateurs au cours du temps et une très grande variabilité entre les comportements des utilisateurs. Nos propositions consistent à faire en sorte que le système s’adapte au maximum et automatiquement à chaque utilisateur notamment par la détermination de paramètres personnalisés. Nous avons appliqué nos propositions à l’analyse de la dynamique de frappe au clavier et à l’analyse des signatures manuscrites. La première application a été proposée par la société CAPMONETIQUE et a aboutit à la création d’un logiciel. La dynamique de frappe est une méthode biométrique qui connaît un développement important actuellement. Cette méthode étudie l’interaction des utilisateurs avec leur clavier afin de les authentifier. Cette partie, ainsi que les expérimentations effectuées sur l’authentification de signatures manuscrites, démontrent l’intérêt de nos préconisations et valident leur généricité puisque, dans les deux cas, les performances des systèmes biométriques comportementaux augmentent par rapport à leurs version basique.

Méta-heuristiques pour la résolution de problèmes d'ateliers de production Geoffrey Vilcot, Laboratoire d'Informatique de Tours
Dans les industries se trouve de nombreuses problématiques et en particulier des problèmes d'ordonnancement. Pour la très grande majorité, les problèmes appartiennent à la classe de complexité NP-Difficile, on ne peut donc obtenir de solutions optimales en un temps raisonnable, surtout pour les instances industrielles qui sont souvent de grande taille. Pour les résoudre on utilise des méthodes approchées qui trouvent des solutions de bonne qualité en un temps de calcul acceptable. J'ai proposé lors de mes recherches des méta-heuristiques basées sur le principe de la recherche tabou et sur celui des algorithmes génétiques. Ces méthodes, qui s'appuient notamment sur la théorie des graphes, ont été implémentées avec succès dans un logiciel commercial.

Graph searching on some graph classes Rodica Mihai, University of Bergen - Norvège
In the graph searching problem, a team of searchers (pursuers) is trying to catch a fugitive moving along the edges of a graph. The problem is to find the minimum number of searchers that can guarantee the capture of the fugitive in the worst case scenario for the searchers (assuming that fugitive is very fast, invisible, and knows the strategy of the searchers). The minimum number of the searchers sufficient to perform searching and ensure capture for each of the models of graph searching are respectively the edge, node, and mixed search numbers, and computations of these are all NP-hard for general graphs. We will look at some graph classes where we can compute the forementioned search numbers in polynomial time.

Construction algébrique de graphes Luc Gillibert, LORIA Nancy
Les liens qu'on peut établir entre les groupes et les graphes on déjà été abordés plusieurs fois au cours de ces deux derniers siècles. Ainsi les graphes de Cayley sont utilisés dans de nombreux domaines de la science moderne. Dans cet exposé sera présenté un nouveau graphe associé à un groupe : le G-graphe. Après une présentation formel de ces graphes, différents problèmes qu'ils induisent où qu'ils résolvent seront abordés. En particulier la construction de graphes symétriques et semisymétriques, la construction de graphes optimalement connectés et la construction de graphes de grandes mailles.

Aspects dynamiques de XML: Évolution des schémas Mírian Halfeld Ferrari Alves, Université François Rabelais de Tours
La mise à jour des documents XML nous permet de replacer plusieurs questions concernant la maintenance de la cohérence d'une base de données vis à vis des contraintes. En effet, les contextes d'utilisation de XML sont habituellement très dynamiques et le type (ou schéma) peut être vu d'une manière plus flexible que celle adoptée dans le modèle relationnel. Le schéma XML est fréquemment sujet à des transformations pour s'adapter à de nouvelles demandes et de nouvelles fonctionnalités. Nous abordons la mise à jour et le maintien de la cohérence d'une base de données XML de différentes manières. Tout d'abord, nous proposons une procédure de validation incrémentale par rapport aux contraintes. Quand la validation incrémentale par rapport au type échoue, c'est-à-dire quand une mise à jour viole le type, deux propositions de traitement sont faites : 1. une routine de correction est activée pour adapter le document XML au type tout en prenant en compte la mise à jour. La mise à jour a donc une priorité par rapport aux données déjà stockées. 2. une routine propose une adaptation du type du document, de façon à accepter le document mis à jour en préservant la validité des autres documents originalement valides et non soumis à la mise à jour. Dans ce cas, la mise à jour est prioritaire et les contraintes peuvent être modifiées. Dans cet exposé nous allons présenter la 2ème approche, en regardant comment faire évoluer le schéma type DTD d'un document XML. Différentes perspectives s'ouvrent sur ce sujet et son application dans le contexte des services web est possible.

Couverture de graphes et complexité algebrique Laurent Lyaudet, LIFO Orléans
Dans le cadre de la complexité algébrique et plus précisément du modèle de Valiant, on s'attache à déterminer la complexité de suites de polynômes. Les plus connus de ces polynômes sont le déterminant, le Pfaffien, le permanent et l'hamiltonien. Ces polynômes ont des interprétations combinatoires bien connues en termes de couvertures de graphes. L'objet de l'exposé sera de présenter des résultats sur la complexité algébrique de ces couvertures quand on se restreint à certaines familles de graphes. Ces résultats et leur démonstration permettent de montrer l'égalité entre la complexité algébrique de classes de circuits ou de polynômes. Nous montrerons notamment que le Pfaffien et le déterminant ont la même complexité algébrique.

Apprentissage dans les réseaux sociaux Emmanuel Viennet, LIPN Paris 13
Dans cet exposé, nous résumons nos travaux de recherche menés au LIPN sur la fouille de données structurées. Après avoir rappelé la problématique de l'apprentissage numérique et présenté les méthodes à noyaux, nous montrons comment ces dernières peuvent s'appliquer efficacement au traitement de textes structurés. Nous décrivons ensuite les problématiques principales de l'apprentissage dans les réseaux sociaux et discutons différents problèmes: recherche et identification de communautés, catégorisation de noeuds, définition de noyaux adapté aux traitement de ces données. Nous concluons l'exposé par une brève description de deux projets de recherche ANR qui explorent l'apport des informations portées par les réseaux sociaux dans différentes applications.

Programmation générative & Architecture parallèle : Vers une méthodologie pour la génération systématique d'outils de développement Joel Falcou, Institut d'Electronique Fondamentale - Université Paris-Sud Orsay
Les besoins croissants en puissance de calcul exprimés par de nombreux domaines scientifiques exercent une pression très forte sur les architectures émergentes, les rendant toujours plus performantes mais toujours plus complexes à maîtriser. Dans ce cadre, le développement d'outils tirant partie des spécificités de ces architectures ( quadri et bientôt octo-coeurs, processeur Cell ou GPU par exemple) devient une gageure car allier expressivité et efficacité devient une tâche ardue. De nombreux travaux visant à utiliser des techniques comme la programmation générative en général et la métaprogrammation en particulier ont démontré leur pertinence mais peu de méthodologie claire n'en émerge. Nous nous proposons ici de définir une telle méthodologie et de montrer comment elle a permis le développement d'outils de parallélisation automatique dans le domaine du traitement d'image et du signal pour des architectures aussi variées que les machines multi-coeurs, les clusters ou le processeur Cell.

Algorithmes exacts pour une généralisation du problème de la domination d'un graphe Mathieu Liedloff, Université Paul Verlaine - Metz
Etant donné un graphe, le problème fondamental de la domination demande de déterminer un plus petit sous-ensemble de sommets de sorte que chaque sommet n'appartenant pas à l'ensemble ait un voisin qui y soit. Le problème est NP-complet et seul un algorithme exponentiel peut calculer une solution exacte pour une entrée quelconque, sauf si P=NP. Depuis 2004, plusieurs algorithmes ont été publiés pour le résoudre dans un temps plus rapide que O(poly(n) 2^n). Dans cet exposé, nous considérerons une généralisation du problème: la (sigma,rho)-domination. Ce cadre très général permet de représenter de nombreux problèmes de type domination. Etant donné deux ensembles sigma et rho d'entiers positifs, un ensemble S est dit (sigma,rho)-dominant si (i) pour tout sommet v de S, le nombre de ses voisins dans S est un entier de sigma; (ii) pour tout sommet v de V-S, le nombre de ses voisins dans S est un entier de rho. Nous donnerons un algorithme exponentiel pour énumérer tous les ensembles (sigma,rho)-dominants d'un graphe en temps O(c^n), pour une certaine constante c<2, si l'ensemble sigma ne contient pas deux entiers consécutifs et si, soit sigma et rho sont finis, soit l'un d'eux est fini et leur intersection est vide. Nous regarderons également d'autres ensembles sigma et rho pour lesquels le problème peut être résolu en temps O(poly(n) 2^(n/2)).

Automates cellulaires et universalité Guillaume Theyssier, laboratoire de mathématiques de l'Université de Savoie
Les automates cellulaires sont des systèmes dynamiques discrets définis par une règle locale qui agit uniformément et de manière synchrone sur un réseau de cellules. Dès la naissance du modèle, sa proximité avec les machines de Turing était comprise et des automates "Turing-universels" ont été construits. En revanche, ce n'est que plus récemment et progressivement que des notions d'universalité "intrinsèque" ont été dégagées, indissociables des notions de simulation correspondantes : un automate est intrinsèquement universel s'il est capable de simuler tout les automates cellulaires. Cette approche a le double intérêt de fournir une notion d'universalité rigoureusement formalisée et adaptée aux automates cellulaires, mais également un outil de classification très fin à travers la notion de simulation. L'objectif de cet exposé est d'abord de présenter le formalisme "algébrique" de J. Mazoyer, I. Rapaport et N. Ollinger (basé sur des opérations de changement d'échelle), ainsi que de nombreux résultats sur la notion d'universalité et le pré-ordre de simulation associés. Dans un formalisme plus général issu de la dynamique symbolique, nous introduirons ensuite toute une famille de notions de simulation entre automates cellulaires. L'objectif est de comprendre en quoi les ingrédients introduits dans chaque notion de simulation influent ou n'influent pas sur le pré-ordre associé, et en particulier sur la notion d'universalité qui en découle.

Analyse d'atteignabilite en réécriture pour la vérification de systèmes infinis. Yohan Boichut, LORIA
Le problème de la vérification de systèmes infinis est en général indécidable. Une possibilité de traiter le sujet est de considérer la vérification de tels systèmes comme un problème d'atteignabilité en réécriture. Sans surprise, le problème d'atteignabilité en réécriture est également indécidable en général. Cependant, par le biais d'approximations, il est possible de calculer un sur-ensemble des termes atteignables afin de vérifier qu'un terme n'est pas accessible par réécriture. La technique de réécriture [Genet98] développe cette idée. L'objet de cet exposé est de décrire comment nous avons appliqué, avec succès, cette technique pour la vérification de protocoles de sécurité dans un premier temps et de programmes Java dans un second temps. Je présenterai également de récents travaux menés avec Thomas Genet (IRISA) et Pierre-Etienne Moreau (Loria) qui ont débouché sur un prototype plus performant que Timbuk

Problèmes de décision et d'évaluation en complexité algébrique Sylvain Perifel, ENS Lyon
En complexité algébrique on manipule directement des nombres réels ou complexes, ce qui permet d'analyser plus aisément des problèmes algébriques. Deux types de problèmes sont alors étudiés : les problèmes de décision, d'une part, où il s'agit de vérifier une propriété (réponse oui ou non) et les problèmes d'évaluation, d'autre part, où il s'agit de calculer un résultat. Nous étudierons les liens entre ces deux types de problèmes du point de vue de la théorie de la complexité, en utilisant le modèle de Blum, Shub et Smale pour les premiers (BSS, opérations +, -, * et tests d'égalité pour décider des langages), et celui de Valiant pour les seconds (calcul de polynômes grâces aux opérations +, - et *). Nous parlerons en particulier des analogues algébriques de P et NP dans ces deux contextes, et montrerons que séparer des classes de complexité dans le modèle BSS (problèmes de décision) implique leur séparation dans le modèle de Valiant (problèmes d'évaluation).

Généralisation aux systèmes multi-patch des méthodes de calcul du taux de reproduction de base pour des modèles épidémiologiques de type SIRS. Maurice Tchuente, ENS Lyon
On s?intéresse à la généralisation aux environnements hétérogènes, des modèles épidémiologiques de type SIRS où les individus, hôtes ou vecteurs, sont répartis dans trois compartiments : les sains ou susceptibles (S), les infectés (I) et les retirés (R). Pour ce faire on considère un système multi-patch, avec des migrations entre les patchs. On montre que, lorsque les migrations sont rapides, le passage à un système multi-patch pour les modèles sans vecteur, fait baisser le taux de reproduction de base. On propose ensuite, pour les modèles à vecteur de type Ross-Macdonald, une formulation matricielle qui permet de calculer, dans le cas où les taux de migration sont les mêmes pour tous les compartiments épidémiologiques, le taux de reproduction de base.

Calcul et exploitation de recouvrements acycliques pour la résolution de (V)CSP Samba Ndojh Ndiaye, LSIS Marseille
Le formalisme CSP (problème de satisfaction de contraintes) est un cadre très puissant de représentation de problèmes par un ensemble de variables, associées chacune à un domaine de valeurs de taille finie et par un ensemble de contraintes qui mettent en relation les variables et dénissent des combinaisons de valeurs compatibles. Une solution est une affectation de l'ensemble des variables qui respecte toutes les contraintes. Le problème de décision associé à un CSP, qui consiste à déterminer l'existence ou non d'une solution, est NP-complet. La méthode de résolution de base est le Backtrack standard (noté BT) qui se révèle totalement inefficace en pratique à cause du grand nombre de redondances inhérentes à cette technique. Plusieurs voies ont été proposées pour l'améliorer. Notamment, les techniques de filtrage, de retour en arrière non chronologique, de consistance avant et d'apprentissage, ont conduit à des méthodes telles que FC et MAC qui sont bien plus efficaces en pratique, mais dont la complexité théorique demeure en O(m.d^n) (notée O(exp(n))), où m est le nombre de contraintes, d la taille maximale des domaines et n le nombre de variables. De meilleures bornes de complexité sont l'oeuvre de méthodes basées sur la décomposition du problème qui permet de proter des indépendances entre diérentes parties. L'une des meilleures bornes est en O(exp(w + 1)), où w est la treewidth de la décomposition arborescente du problème. En effet, elle peut considérablement améliorer la complexité de base, à savoir O(exp(n)) avec w < n, et parfois w << n. Généralement, on observe une inadéquation entre les excellentes bornes de complexité théorique et les résultats médiocres voire inexistants des méthodes structurelles. Notre objectif est donc de rendre opérationnelles ces méthodes par la dénition de stratégies de décomposition et d'exploitation de qualité pour une résolution efficace en pratique. Cette étude est ensuite étendue au formalisme CSP valués (VCSP) qui est une extension du formalisme CSP permettant de prendre en compte la notion de préférence sur les solutions. Contrairement au formalisme CSP, il autorise l'utilisation de contraintes faisant référence à des possibilités, préférences, souhaits qu'il faut satisfaire si possible. Le problème VCSP consiste donc à trouver une affectation totale de coût optimum suivant un critère exprimé par les contraintes. Le problème VCSP est NP-dicile. En général, les méthodes de résolution de VCSP sont des adaptations de celles du cadre CSP. On retrouve ainsi la même inadéquation entre les bonnes complexités temporelles des méthodes structurelles et leurs performances médiocres en pratique. Les méthodes structurelles imposent généralement une grande rigidité dans l'ordre d'aectation des variables. Or, les ordres statiques obtiennent généralement des résultats catastrophiques par rapport aux heuristiques dynamiques. Nous proposons ainsi une généralisation des méthodes structurelles BTD (CSP) et BTD-val (VCSP) qui offrent parmi les meilleures résultats pratiques avec une complexité en O(exp(w+1)). Ces nouvelles méthodes, BDH et BDH-val, s'aranchissent de cette rigidité par une exploitation dynamique de la structure du problème grâce à la notion de recouvrement acyclique de graphes qui est un peu plus générale que celle de décomposition arborescente. Elles réalisent un compromis primordial entre la liberté laissée aux heuristiques de choix de variables et l'exploitation de la structure du problème, pour obtenir d'excellentes performances tout en gardant des garanties théoriques intéressantes.

Extraction et formalisation de la sémantique des liens hypertextes dans des documents culturels, scientifiques et techniques. Moustafa Al Hajj, LIFO Orléans
L'utilisation des liens hypertextes sur Internet rend les sites plus attractifs et plus faciles à lire et permet l'enrichissement des sites par des informations provenant d'autres sites. Cependant, ces mêmes liens entraînent des difficultés pour les lecteurs et les moteurs de recherche. Les liens hypertextes sont porteurs d'informations sémantiques qui, si elles étaient complètement formalisées, seraient exploitables par des programmes pour améliorer la navigation et la recherche d'information, et prendraient leur place dans l'émergence du web sémantique. Nous présenterons une méthodologie originale d'extraction formelle de la sémantique des liens hypertextes. La méthode proposée a été testée sur les liens d'un corpus. Le formalisme RDF est utilisé pour représenter la sémantique des liens. Une ontologie pour les liens spécifiques au domaine des biographies de personnages célèbres a été constituée à partir de la sémantique extraite des liens. Celle-ci a été représentée en RD FS. Des outils d'apprentissage supervisé et de caractérisation des pages web par des mots clés sont utilisés pour aider à l'extraction formelle de la sémantique.

Réactivité efficace pour le pi-calcul synchrone. Frédéric Dabrowski, INRIA
La réactivité est une propriété essentielle des programmes synchrones. Intuitivement, celle-ci assure que, à chaque instant, le programme réagit aux entrées du système en produisant une sortie. Dans cet exposé, nous considérerons une propriété plus forte, la réactivité efficace. En plus de la réactivité, cette propriété assure que, à chaque instant, la taille du programme et le temps de réaction sont bornés par par un polynome de la taille du programme et de la taille des entrées du système. Nous présenterons une méthode d'annotation des programmes, associée à une analyse statique permettant d'assurer la propriété de réactivité efficace pour les programmes du pi-calcul synchrone (une version synchrone du pi-calcul basée sur une relaxation du modèle synchrone). Nous évoquerons également l'utilisation d'une version affaiblie de cette analyse statique dans le cadre de l'implémentation d'un langage expérimental adapté à l'utilisation des architectures multi-cores.

Abstraction in Representation and Learning Lorenza Saitta, LIFO Orléans
Computational complexity is often a major obstacle to the application of AI techniques, most notably relational learning, to significant real-world problems. Efforts are then required to understand the sources of this complexity, in order to tame it without introducing too strong simplifications that make either the problem or the technique useless. It is well known that representation is a key issue to facilitate solving a problem, even though there is clearly no hope of turning, by a representation change, an intractable class of problems into a tractable one. However, computational characterization of problem classes is based on worst-case analysis, and, hence, not every problem instance in the class is equally hard to solve. Representation change has been tackled, in Machine Learning, via feature selection and feature construction. These representation changes are both instances of abstraction, i.e., of representation changes aimed at simplifying the representation of both examples and hypotheses. In the literature, several definitions of abstraction have been proposed. In this talk the effects of some of these definitions on the task of learning (relations) will be described. Both the computational complexity reduction (if any), and the impact on the quality of the learned knowledge will be discussed.