Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Automates d'arbres et applications (24h de cours – 3 ECTS)

Responsable : Hubert Comon-Lundh

Horaires des cours

Les cours ont lieu de de 10h15 à 11h45 les lundi matin sur le site Chevaleret, en 0C2.

Les cours seront en anglais si quelqu'un en fait la demande.

Intervenants prévus pour 2005-2006

Objectifs

Il s'agit de donner quelques algorithmes de base sur les automates d'arbre (par exemple: le vide est un problème typique de la classe PTIME), mais surtout l'objectif est de montrer comment utiliser les automates d'arbres dans plusieurs domaines d'application.

Ce cours doit donc permettre d'acquérir quelques notions de base qui permettent d'utiliser l'outil automates d'arbres (aa dans la suite) chaque fois que le problème posé s'y prête. C'est notamment le cas pour toute une série de questions qui se posent naturellement en logique monadique de second ordre, comme la recherche de stratégies optimales de réduction, mais aussi pour d'autres problèmes plus exotiques: contraintes ensemblistes, unification rigide, réductibilité close, déductibilité par un intrus, langages de requêtes, etc...

Nous verrons plusieurs variantes des automates d'arbres: automates alternants, automates avec contraintes, automates sur les arbres dont les fils ne sont pas ordonnés.

Plan du cours

1- Les notions de base: propriétés de clôture, déterminisme, décision

du vide et du plein et leurs complexités, pompage: sous forme d'exercices puisque c'est normalement connu.

2- logique monadique de second ordre (faible) à deux successeurs; théorème de

Thatcher et Wright (cas finis); théorème de Rabin (cas infini).

3- Exemples d'application en réécriture: la  théorie de la réductibilité,

l'unification rigide.

4-  Résultats de préservation de la reconnaissabilité. Applications:

vérification de propriétés d'accessibilité dans les systèmes complexes, stratégies décidables en réécriture.

																																					
5-  Automates à contraintes égalitaires et diségalitaires. Résultats de

décision. Applications: théorie de la réduction.

																																					
6-  Automates d'arbres avec symboles variadiques.

hedges-automates et automates modulo AC. Counting MSO. Liens avec les bases de données (La frontière exacte de cette partie doit être fixée en accord avec le cours de fondements des bases de données).

																																				  
8- Automates bidirectionnels et alternants. Théorèmes d'expressivité.

Un exemple d'application avec la théorie de l'intrus de Dolev-Yao. Les classes H1-H3.

																																					
9-  Automates à mémoire. Lien avec les contraintes ensemblistes.

(Peut faire l'objet d'un devoir, par exemple)

																																					
10- Automates modulo les théories équationnelles et applications.

Résultats de clôture, de décision. Automates bidirectionnels alternants modulo...

Exercices

Le matériel pédagogique est disponible depuis le serveur de liste du cours http://list.mpri.master.univ-paris7.fr/wws/d_read/cours-2-28-1/.

Dates et contenu des cours (2006)

Prévisions

Date Intervenant Contenu
18 sep H. Comon-Lundh Automates d'arbres fins et infinis: définition et propriétés élémentaires
25 sep H. Comon-Lundh Automates d'arbres fins et infinis: définition et propriétés élémentaires
2 oct H. Comon-Lundh Automates de tuples d'arbres: 3 notions de reconnaissabilité. Propriétés de cloture et comparaison des 3 notions
9 oct H. Comon-Lundh Cloture des GTT par itération et par composition.
16 oct H. Comon-Lundh Définition de (W)SkS.
23 oct H. Comon-Lundh Correspondance entre automates d'arbres et (W)SkS. Théoreme de Thatcher et Wright. Théorème de Rabin.
30 oct F. Jacquemard Automates a contraintes égalitaires et diségalitaires (indécidabilité).
6 nov F. Jacquemard Automates a contraintes égalitaires et diségalitaires (décidabilité).
13 nov Partiel
20 nov PAS DE COURS
27 nov F. Jacquemard Théorie de la réduction
F. Jacquemard Automates de multiarbres, hedge automata
F. Jacquemard Contraintes de Presbuger
F. Jacquemard Automates de multiarbres, sheave automata and logic
F. Jacquemard Automates modulo théories équationnelles
22 jan H. Comon-Lundh Automates alternants et bidirectionnels
29 Jan PAS DE COURS
5 fev H. Comon-Lundh Automates alternants et bidirectionnels
12 fev Examen

Pré-requis

Les prérequis généraux du M2 (notions de complexité, automates de mots: propriétés de clôture et de décision, automates d'arbres: définitions et propriétés de clôture).

Bibliographie

Le document de référence est: Comon, Dauchet, Gilleron, Jacquemard, Lugiez, Tison, Tommasi: Tree Automata Techniques and Applications.

Liste de diffusion

Les années précédentes

Année 2006-2007


  • Set ALLOWTOPICCHANGE = %MAINWEB%.WebMastersGroup, %MAINWEB%.HubertComonLundh, %MAINWEB%.FlorentJacquemard
 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA