Previous Next Contents

8   Année 1997-98

Groupe de travail géré par par D. Janin

   


* 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
   


Previous Next Contents