• 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)

18/12/2003 : Vers une décomposition modulaire des graphes bipartis.
Jean-Marie Vanherpe (LIFO - Le Mans) Résumé
Attention : Soutenance d'habilitation.

01/12/2003 : Recherche de motifs fréquents pour l'extraction de règles d'association et de caractérisation.
Ansaf Salleb (LIFO) Résumé
Attention : Soutenance de thèse, amphi H.

24/11/2003 : Explications de retraits de valeurs en programmation par contraintes et application au diagnostic déclaratif.
Willy Lesaint (Orléans + Angers) Résumé
Attention : Soutenance de thèse, amphi H.

03/11/2003 : Une introduction au tatouage et aux ondelettes.
Abdelhamid Benhocine (Université de Sétif, Algérie) Résumé

06/10/2003 : Complexité d'un programme universel.
Alain Colmerauer (LIM Marseille et IUF) Résumé
Attention : Le séminaire aura lieu en amphi H.

22/09/2003 : Research at the Faculty of Informatics and Management.
Josef Hynek (Université Hradec Kralové, République Tchèque) Résumé

23/06/2003 : Programmation par contraintes et informatique musicale.
Charlotte Truchet (Paris 6) Résumé

16/06/2003 : Dominating sets and local treewidth.
Fedor Fomin (Bergen, Norvège) Résumé

02/06/2003 : Algorithmes certifiés.
Dieter Kratsch (Metz) Résumé

26/05/2003 : Modèles composables et concurrents pour le temps-réel.
Franck Pommereau (Paris 12) Résumé

12/05/2003 : Exploration interactive de données multimédia par réalité virtuelle.
Gilles Venturini (Tours) Résumé

07/04/2003 : Méthode de génération de tests pour les composants de service. Application aux services de réseau intelligent.
Fatiha Zaidi (INT Evry) Résumé
Attention : Annulé

03/04/2003 : Logiques temporelles pour la vérification : expressivité, complexité, algorithmes.
Nicolas Markey (LIFO) Résumé
Attention : Soutenance de thèse, amphi S, 14h

31/03/2003 : Compositions parallèles et BSML.
Frédéric Loulergue (Paris 12) Résumé

03/03/2003 : Synthesis of Rule-based Constraint Solvers.
Slim Abdennadher (Munich) Résumé

17/02/2003 : Zope pour le développement de portails intranet/extranet.
Nicolas Roméro (Société adp3i) Résumé

13/01/2003 : La loi sur l'innovation et ses implications pour la recherche.
Olivier Jouin, Sébastien Besson, Thierry Gonard (Orléans Technopole) Résumé

Résumés des séminaires

Vers une décomposition modulaire des graphes bipartis. Jean-Marie Vanherpe, LIFO - Le Mans
Dans l'étude de problèmes posés sur des classes particulières de graphes on trouve souvent avantage à les décomposer pour ensuite se ramener à l'étude de parties indécomposables. Dans cette optique nous présenterons des travaux qui concernent une nouvelle méthode de décomposition, nous dévoilerons la structure de certains graphes indécomposables et présenterons quelques applications.

Recherche de motifs fréquents pour l'extraction de règles d'association et de caractérisation. Ansaf Salleb, LIFO
La fouille de données est un domaine de recherche en plein essor visant à extraire des connaissances à partir de grandes quantités de données. Dans cette thèse, nous nous intéressons à l'extraction de motifs fréquents dans les bases de données. Cette étape à la fois importante et coûteuse, est commune à plusieurs tâches de fouille de données. Parmi celles-ci, nous avons étudié la recherche de règles d'association et la recherche de règles de caractérisation, fondées l'une comme l'autre sur la recherche de motifs fréquents. D'une part, nous nous sommes intéressés à l'extraction de motifs fréquents dans des bases dites transactionnelles. Ces bases se présentent comme des multi-ensembles de transactions, où chaque transaction est constituée d'un ensemble d'items, appelé itemset. Nous proposons dans ce cadre une approche booléenne pour la recherche des itemsets fréquents. L'idée est de représenter une base de transactions par une fonction à variables booléennes et à valeurs entières. L'étude menée a non seulement montré l'efficacité de l'approche pour représenter et charger les bases de transactions denses en mémoire, mais aussi l'intérêt de l'utilisation de ce format condensé pour l'extraction des itemsets fréquents maximaux. D'autre part, l'extraction des motifs fréquents dans des bases de données représentant des objets et leurs relations, comme par exemple les bases de données relationnelles et géographiques, est un problème non trivial, étant donné la complexité de l'espace de recherche. Ceci nous a poussé à orienter nos recherches vers d'autres types de règles plus ciblées telles que les règles de caractérisation. Nous proposons un cadre général pour la caractérisation d'un ensemble d'objets, appelé ensemble 'cible', en nous basant non seulement sur leurs propriétés propres mais aussi sur les propriétés de tous les objets qui leur sont liés directement ou indirectement. Ce cadre original est basé sur des notions nouvelles, telles que la notion de chemin quantifié, qui nous permet de considérer des données relationnelles sans recourir à l'aplatissement des relations. Enfin, nous avons effectué des expérimentations sur une base de données géographiques, issue du domaine de la prospection minière, qui nous a été fournie par le BRGM. Elles ont porté sur la recherche de règles d'association et de caractérisation, ce qui nous a permis d'appliquer nos approches à des bases de données réelles.

Explications de retraits de valeurs en programmation par contraintes et application au diagnostic déclaratif. Willy Lesaint, Orléans + Angers
Non communiqué.

Une introduction au tatouage et aux ondelettes. Abdelhamid Benhocine, Université de Sétif, Algérie
Par tatouage, on entend insertion d'une information (ou marque) cachée dans un média comme une image, un objet, une séquence vidéo,... . Les objectifs du tatouage sont nombreux ; on peut citer la protection du copyright et la copie illégale. Les problèmes informatiques sont également nombreux : positionner la marque, ne pas altérer la perception du média, garder la marque aussi longtemps que possible dans le média, empêcher toute tentative d'effacement ou de modification de la marque, extraire la marque. Les méthodes de tatouage sont diverses et plus ou moins robustes : la robustesse est la qualité d'un algorithme capable de rendre difficile sinon impossible toute tentative deffacement de la marque, ce qui permettrait sinon au pirate de s'approprier l'oeuvre. La technique des ondelettes discrètes permet la décomposition d'un signal en une partie définissant son approximation à différentes résolutions et une partie appelée détail. Une telle technique s'adapte au problème du tatouage, le signal à décomposer étant une suite de valeurs discrètes comme les coordonnées de points, les couleurs des pixels,... , paramètres du média susceptibles de varier lors du tatouage.

Complexité d'un programme universel. Alain Colmerauer, LIM Marseille et IUF
Le grand public l'a compris : à l'achat d'un ordinateur les caractéristiques techniques importent peu, ce qui compte ce sont les logiciels fournis. Eux seuls décident des utilisations possibles de la boite en tôle, avec son clavier et son écran. L'intelligence de la machine réside dans le logiciel, c'est-à-dire, le programme $P$, qu'elle exécute pour produire un résultat à partir d'une donnée $x$. Mais alors, quel est le programme qui la rend vraiment intelligente ? Réponse : un programme universel $U$ qui, à partir d'une donnée formée d'un programme quelconque $P$ suivi de sa donnée $x$, produit le même résultat que celui que produit l'exécution de $P$ sur $x$. Bref, un programme universel donne à la machine la possibilité de considérer les programmes comme des données et de calculer le résultat de leurs exécutions : dans les données figure le mode d'emploi pour les utiliser! L'objet de cet exposé est la complexité d'un tel programme universel $U$. Bien entendu le programme universel est d'autant plus complexe que les instructions qui le composent sont primitives, et nous le verrons sur des exemples. Mais il s'agit là d'un résultat qualitatif. Pour passer à un résultat quantitatif il faut mesurer la complexité d'un programme universel par un nombre. Comme mesure on peut prendre la taille du programme qui le constitue, mais fidèle à une tradition algorithmique, nous préférons mesurer une valeur $c$ dépendant d'un nombre d'instructions exécutées. Pour définir $c$ on fait la remarque suivante : un programme universel $U$ étant un cas particulier de programme $P$, on peut considérer une donnée quelconque $x$ pour $U$. Si on exécute $U$ sur la donnée formée de $U$ suivi de $x$, d'après la définition de l'universalité, on obtient le même résultat que si on exécute directement $U$ sur $x$, mais en exécutant un nombre d'instructions plus grand. Plus généralement si on exécute $U$ sur $U$, répété $n$ fois, suivi de $x$, on obtient le même résultat qu'en exécutant $U$ directement sur $x$, mais en exécutant un nombre $f(n,x)$ d'instructions considérablement plus grand. Il est alors naturel de définir la complexité de $U$ comme la limite $c$ du rapport $f(n+1,x)/f(n,x)$ quand $n$ devient infiniment grand. Ce nombre $c$ est en quelque sorte le nombre moyen d'instructions qu'exécute $U$ pour simuler l'exécution d'une de ses propres instructions. Le fait de faire tendre $n$ vers l'infini augmente les chances que $c$ ne dépende pas de $x$. Nous présentons un programme universel de complexité $c$: * de l'ordre de 10, pour une machine qui idéalise le fonctionnemment de nos ordinateurs actuels, (un nombre infini de mémoires, chacune contenant un entier non borné), * moins de 4000, pour une machine de Turing à quatre symboles (le symbole blanc compris) avec un seul ruban bi-infini, la machine de Turing étant une des machines idéalisées les plus simples. Nous terminons par quelques éclaircissements sur la façon de calculer $c$ et de justifier son existence.

Research at the Faculty of Informatics and Management. Josef Hynek, Université Hradec Kralové, République Tchèque
The aim of this presentation is to introduce the University of Hradec Kralove and its Faculty of Informatics and Management. The main focus will be given on various research teams that are currently active at this school, to outline their interests and results achieved and to discuss the possibilities of mutual research co-operation.

Programmation par contraintes et informatique musicale. Charlotte Truchet, Paris 6
Le travail que nous présenterons se situe à la croisée de deux thèmes informatiques. Premièrement, la programmation par contraintes. Très grossièrement, il s?agit de programmer non pas en construisant un résultat (via un algorithme), mais en décrivant un résultat à atteindre, avec des variables (les inconnues du problème), sur lesquelles sont posées des contraintes, prédicats qui restreignent les valeurs que les variables peuvent prendre. Le problème ainsi modélisé forme un CSP (Constraint Satisfaction Problem). Il existe aujourd?hui de nombreuses techniques de résolution de CSP pour résoudre des problèmes fortement combinatoires, avec de multiples applications académiques ou industrielles. Nous en présenterons une application un peu inhabituelle, l?informatique musicale. Il s?agit de rendre l?ordinateur accessible à des musiciens, des compositeurs contemporains dans notre cas. Nous décrirons le logiciel OpenMusic, qui est un langage de programmation visuel, fonctionnel et objet adapté à la musique. La programmation par contraintes trouve une place très naturelle en musique : les anciens traités d?harmonie par exemple ne donnent pas de méthode constructive pour écrire de la « belle musique », mais donnent un ensemble de règles que la « belle musique » doit respecter (pas de quintes parallèles, voix soprano et basse en mouvements contraires, etc). C?est également le cas pour les compositeurs contemporains, avec lesquels nous avons identifié et résolu une quinzaine de CSPs musicaux. Cette étude a servi à choisir un algorithme de résolution par recherche locale, implémenté dans OpenMusic.

Dominating sets and local treewidth. Fedor Fomin, Bergen, Norvège
It is known that the treewidth of a planar graph with a dominating set of size $d$ is $O(\sqrt{d})$ and this fact is used as the basis for several fixed parameter algorithms on planar graphs. An interesting question motivating our study is if similar bounds can be obtained for larger minor closed graph families. We say that a graph family $\mathcal{F}$ has the {domination-treewidth property} if there is some function $f(d)$ such that every graph $G\in\mathcal{F}$ with dominating set of size $\le d$ has treewidth $ \le f(d)$. We show that a minor-closed graph family $\mathcal{F}$ has the domination-treewidth property if and only if $\mathcal{F}$ has bounded local treewidth. This result has important algorithmic consequences.

Algorithmes certifiés. Dieter Kratsch, Metz
Un algorithme de reconnaissance est un algorithme qui decide si une entree (graphe, objet geometrique, image, mot, etc.) possede une certaine propriete. Un tel algorithme accepte l'entree si elle a la propriete, et il rejete l'entree si ce n'est pas le cas. Un algorithme certifie pour un probleme de decision est un algorithme qui donne avec chaque reponse un certificat demontrant que la reponse est correcte. Une version certifiee d'un algorithme de reconnaissance est fortement souhaitable en pratique. Regardons un algorithme qui decide si un graphe est planaire, qui donne un dessin dans le plan lorsque le graphe est planaire, et sinon declare simplement que le graphe n'est pas planaire. Meme si l'algorithme etait demontre correct, une implantation de l'algorithme peut avoir des bugs. Donc si l'implantation declare le graphe non-planaire il n'y a aucun moyen de savoir si la reponse est correcte ou fausse. D'abord on discute les algorithmes certifies et quelques exemples faciles. Puis on presente un algorithme certifie et lineaire pour la reconnaissance de graphes d'intervalles.

Modèles composables et concurrents pour le temps-réel. Franck Pommereau, Paris 12
Cet exposé porte sur des modèles explicitant la concurrence qui s'appliquent au domaine du temps-réel. Le point de départ est un modèle basé sur des réseaux de Petri colorés composables à la manière des termes dans les algèbres de processus. Nous montrons comment introduire dans ce cadre une représentation du temps, appelée « temps causal », dont l'originalité consiste à utiliser l'expressivité du modèle pour représenter explicitement une horloge dans les systèmes à temporiser. Cette approche se révèle souple et agréable à utiliser ; de plus, les résultats pratiques sont prometteurs puisqu'il a été possible de vérifier automatiquement des systèmes ainsi modélisés avec de meilleures performances que des méthodes réputées (les automates temporisés avec les outils UPPAAL et Kronos). La seconde partie de l'exposé présente les bases formelles sur lesquelles s'appuient les travaux ci-dessus. Il s'agit d'algèbres de processus dotées de la structure suivante : une algèbre de termes est munie d'une sémantique opérationnelle au moyen de règles SOS ; une algèbre de réseaux de Petri permet de donner aux termes une sémantiques dénotationnelle ; ces deux sémantiques sont prouvées cohérentes (elles définissent les mêmes évolutions).

Exploration interactive de données multimédia par réalité virtuelle. Gilles Venturini, Tours
Nous presentons une nouvelle methode interactive de visualisation 3D de donnees multimedia (numeriques, symboliques, sons, images, videos, sites Web) en realite virtuelle. Nous utilisons un affichage 3D stereoscopique permettant de representer les donnees numeriques. Nous ajoutons a cet affichage l'apparition de textes contextuels, l'utilisation de la synthese vocale, la lecture de sons, l'affichage d'imagettes ainsi que l'affichage de grandes images, de videos ou de sites web sur une deuxieme machine. La navigation au sein des visualisations est effectuee grace a l'utilisation d'un capteur 3D a six degres de liberte qui simule une camera virtuelle. Des requetes interactives peuvent etre posees a la machine par l'utilisation d'un gant de donnees reconnaissant les gestes. Nous montrons comment cet outil est applique sur un cas reel concernant l'etude de la peau humaine saine.

Méthode de génération de tests pour les composants de service. Application aux services de réseau intelligent. Fatiha Zaidi, INT Evry
Le test de conformité est une activité cruciale dans le développement d'une application. Il a pour but de s'assurer que le produit fini correspond bien à la spécification de départ. Devant la complexité croissante des systèmes de télécommunications, il est devenu nécessaire d'assister les différentes phases de développement des systèmes par des méthodes et des outils. Ainsi, les méthodes formelles ont permis l'émergence de méthodes de génération automatique de tests et ainsi la possibilité de soulever un grand nombre d'ambiguïtés dans l'expression de ce que doit réaliser le système. Or, le test exhaustif de ces systèmes n'est pas toujours possible pour des cas réels, en raison du problème bien connu d'explosion combinatoire du nombre d'états. Nous proposons une méthode de génération de tests pour les composants de services dans une architecture de réseau intelligent afin d'éviter la génération de tests redondants et le problème d'explosion susmentionnée. La présentation porte sur la définition d'algorithmes de génération de tests à partir de spécifications exprimées sous formes de machines à états finis étendues et plus particulièrement sur leur application au test de composants imbriqués dans le cadre du domaine des services en télécommunication. Nous abordons ces problèmatiques sous les angles théoriques et pratiques liés à la définition et la mise en oeuvre de ses algorithmes adaptés ainsi qu`à la confrontation avec des études de cas réalistes et de tailles conséquentes. Nous étendons également le champ de l'applicabilité de la méthode proposée pour le test imbriqué au test d'interopérabilité. Intuitivement, l'optique choisie est de considérer tout échange de messages entre les deux implantations comme composante d'un automate intermédiaire, modélisant l'interfonctionnement des deux systèmes. Cet automate est ensuite tout simplement vu comme une spécification imbriquée qu'il s'agit de tester en vue de vérifier l'interopérabilité.

Logiques temporelles pour la vérification : expressivité, complexité, algorithmes. Nicolas Markey, LIFO
Ce travail s'inscrit dans le cadre de la vérification formelle de programmes: le model checking est une technique qui permet de s'assurer qu'une propriété, exprimée en logique temporelle, est vérifiée par le modèle d'un système. Cette thèse étudie plusieurs logiques temporelles, du point de vue de l'expressivité et de la complexité. Nous étudions trois grands types de logiques temporelles : - concernant la logique temporelle du temps linéaire, nous prouvons que l'ajout de modalités du passé permet de simplifier l'écriture des formules sans augmenter la complexité des problèmes de model checking. Nous étudions également l'impact de l'ajout de la modalité Now ; - concernant la logique temporelle du temps arborescent, nous établissons la complexité du model checking pour plusieurs extensions classiques de CTL ; - enfin, nous montrons qu'il est possible, sous certaines conditions, de vérifier efficacement des propriétés quantitatives sur la durée séparant deux évènements.

Compositions parallèles et BSML. Frédéric Loulergue, Paris 12
La bibliothèque BSMLlib est une bibliothèque pour la programmation parallèle BSP en Objective Caml. Elle est basée sur une extension du lambda-calcul par des opérations parallèles sur une structure de données parallèle appelée vecteur parallèle, qui est donné par intention. Ces opérations sont "plates" et permettent la programmation BSP en "mode direct" mais il est impossible d'exprimer directement des algorithmes diviser-pour-règner. De nouvelles constructions pour la bibliothèque BSMLlib seront présentées. Elle permettent d'exprimer des algorithmes diviser-pour-règner. Elles s'appellent respectivement juxtaposition parallèle et la superposition parallèle. Des modèles de coût dérivés du modèle de coût BSP seront également présentés.

Synthesis of Rule-based Constraint Solvers. Slim Abdennadher, Munich
Program synthesis research aims at maximally automating the passage from specifications to programs. In the field of constraint solving, several methods have been proposed to automatically generate solvers for constraints given their logical specification. A general approach to implement the propagation and simplification of constraints consists of applying rules over these constraints. In this talk, we present a variety of methods for generating propagation and simplification rules for constraints defined extensionally or intesionally. Furthermore, we show that these methods perform well on various examples, including Boolean constraints, multi-valued logic, and Allen's qualitative approach to temporal logic.

Zope pour le développement de portails intranet/extranet. Nicolas Roméro, Société adp3i
La société adp3i a bâti une offre de portails intranet/extranet basée sur des logiciels Opensource : Linux, Apache, OpenLDAP et Zope. Nous présenterons plus particulièrement Zope, qui est un serveur d'application orienté gestion de contenu qui étend le paradigme objet de façon très originale, avec les notions de publication objet et d'acquisition. Nous montrerons ensuite comment nous avons utilisé les mécanismes de Zope pour construire notre portail. A l'issue du séminaire, une démonstration "en ligne" aura lieu pour les personnes intéressées.

La loi sur l'innovation et ses implications pour la recherche. Olivier Jouin, Sébastien Besson, Thierry Gonard, Orléans Technopole