|
|
* 13 Octobre | Bertrand Lesaec |
Géneration de Tests | |
|
|
* 20 Octobre | David Janin |
Problèmes ouverts I | |
|
|
* 27 Octobre | André Raspaud (1/2h) -- Bruno Courcelle (1/2h) |
Problèmes ouverts II | |
|
|
* 3 Novembre | Nicole Bidoit |
Extension des langages temporels aux bases de données non structurées | |
|
|
* 10 Novembre | Yves Métivier |
Coverings and the power of local computations in graphs knowing the size or the topology | |
|
|
* 17 Novembre | Géraud Senizergues |
G(A) ~ G(B) ? | |
|
|
* 24 Novembre | Mourad Ykhlef |
Langages de requètes pour bases de données semi-structurées | |
|
|
* 5 janvier | Mike Robson |
Une conjecture sur les arbres binaires de recherche | |
|
|
* 19 janvier | Olivier Ly |
Le problème de l'homéomorphisme de surfaces équationnelles sans bord est décidable | |
|
|
* 26 janvier | Denis Lugiez (LIM - Marseille) |
Quelques sortes d'automates d'arbres a contraintes et leur utilisation en Preuve automatique | |
Résumé : Les outils automatiques de preuves permettent de realiser des preuves par induction en utilisant des techniques a base de reecriture. Dans ce cadre les fonctions sont definies par des regles de reecriture. Pour assurer de bonnes proprietes a la procedure de preuve, il faut pouvoir decider que ces definitions sont completes et savoir construire des ensembles-tests. On montre dans cet expose comment l'utilisation de nouvelles classes d'automates d'arbres a contraintes permet de resoudre ces questions dans de nombreux cas utiles, notamment lorsque des constructeurs associatifs-commutatifs sont utilises. Nous montrerons que la classe d'automate utilisee possede de bonnes proprietes en combinant des techniques arithmetiques et des techniques de pompage. Nous terminerons en discutant les possibilites d'extension de la classe d'automates consideree. | |
|
|
* 26 janvier | Nicolas Magnier |
Validation des transactions dans les bases de données : Classes décidables et vérification automatique | |
|
|
* 2 février | Pierre-André Wacrenier |
|
|
* 9 février | Khanh Hoang (Paris I) |
Une approche basée sur le non-déterminisme au problème de la recherche d'un langage pour PTIME | |
Résumé : Un problème central dans la théorie des modèles finis, la théorie des bases de données et la théorie de la complexité descriptive est la quête d'une logique pour PTIME. Nous présentons une approche basée sur le non-déterminisme pour aborder ce problème : elle permet d'obtenir un langage de requêtes dont le pouvoir d'expression est strictement plus grande que celui des langages connus . | |
|
|
* 23 février | Mohamed Mosbah |
Les graphes de cliques | |
|
|
* 23 mars | Bruno Courcelle |
Representation logique des dessins de graphes avec croisements d'arcs (11h-12h) | |
|
|
* 23 mars | Luc Ségoufin (INRIA Rocquencourt) |
Interrogation des bases de donnees topographiques (14h-15) | |
|
|
* 30 mars | Sofian Maabout (Anvers) |
Une sémantique trivaluée pour rêgles de mise à jour | |
Résumé : Bien que l'introduction de rêgles du type ECA (Evénement, Condition,
Action) -en anglais, trigger- dans les bases de données ait des applications
potentielles trés diverses, il a été demontré que certaines proprietés
fondamentales comme la terminaison et la confluence sont indecidables.
Ainsi, l'utilisation de cet outil est rendu difficile. Nous proposons d'utiliser la sémantique bien fondée [van Gelder et. al. 89] comme support pour la sémantique de rêgles dont l'évenement et l'action sont des mises a jour. Nous montrons l'applicabilité de l'approche en considerant le cas du maintien des contraintes d'intégrité. L'avantage de cette approche sont la complexite polynomiale de la sémantique, la terminaison et la confluence sont garanties. le problème est qu'on utilise une sémantique trivaluée. Nous montrons comment garantir des bases bivaluées pour une certaine classe de contraintes. |
|
|
|
* 27 avril | David Simplot (Lille) |
Itération de transductions préservant les longueurs | |
Résumé : Un grand nombre d'outils et de modèles de calculs (systèmes de réécriture finis, automates cellulaires, machine de Turing, etc...) peuvent être simulés par l'itération d'une transduction rationnelle (fonction sur les mots réalisée par un automate fini avec fonction de sortie). Nous limitons notre étude aux transductions préservant les longueurs et plus particulièrement aux transductions construites à partir de transductions rationnelles (ou de fonctions rationnelles) préservant les longueurs avec les opérations d'union, composition et itération. Nous montrons que l'utilisation de transductions ou de fonctions rationnelles amène à la même classe et nous donnons plusieurs théorèmes de représentation à l'aide de différents outils (bimorphisme, langages de figures, automates cellulaires). | |
|
|
* 4 mai | Bruno Courcelle |
D'aprés Robertson et Seymour (Mineurs de graphes n°23) | |
|
|
* 11 mai | Teodore Knapik (la Réunion) |
Un aller-retour entre les semi-systèmes de Thue et les graphes infinis | |
Résumé : L'exposé donne une approche de spécifications et vérifications
de systèmes infinis. Cette approche, appelée spécifications de
Thue, est basée sur les systèmes de Thue (i.e. équations entre
mots). On s'intéresse à la version "orientée" des systèmes de
Thue, i.e. systèmes de réécriture de mots. Une spécification de Thue est un triplet (S,L,u) où S est un semi-système de Thue, L est un langage ne comportant que des mots irreductibles par rapport à S et u est un mot de S. Le modèle d'une spécification de Thue est un graphe orienté simple ayant une racine et vérifiant certaines conditions. (Il s'agit d'une sorte de "graphe de Cayley".) Au cours de l'exposé on s'attachera principalement à dégager une classe de spécifications dont les modèles ont une théorie monadique du second ordre décidable. Les modèles de cette classe forment une famille de graphes observationnellement equivalents aux graphes des machines à pile. |
|
|
|
* 25 mai | Igor Walukiewicz (Varsovie) |
A fixpoint logic for languages traces | |
|
|
* 15 juin | Giacomo Lenzi (Pise) |
Un prototype de systèmes d'axiomes pour la logique temporelle CTL* | |
|
|
* juin | Philippe Narbel |