| 12 septembre 2011 | Introduction
aux classes de complexité Transparents présentation du cours Transparents motivation complexité I) Machine de Turing a) Définitions
II) Classes de complexité en tempsb) Exécutions a) Encodage d'une
machine de Turing dans un pavage
III) Classes de complexité en espaceTransparents pavages et machines de Turing Magnets pour le pavage à imprimer b) le problème TILING est NP-complet c) SAT est NP-complet Démo SAToulouse (interface graphique pour un solveur SAT) a) CORRIDOR TILING
est NPSPACE-hard
b) QBF-SAT est NPSPACE-hard et.... dans PSPACE ! |
TD1 |
| 19 septembre 2011 | IV) Conclusion a) Bilan : P inclus
NP inclus (PSPACE = NPSPACE)
b) Exemple : jeu de géographie et jeu de Go Transparents réduction QBF dans le jeu de géographie et jeu de Go La logique modale K Transparents "l'histoire de la logique modale" I) Syntaxe II) Axiomatique III) Sémantique de Kripke IV) Complétude Transparents qui explique la construction du modèle canonique et la complétude |
TD2 |
| 26 septembre 2011 | V) Expressivité a) Bounded morphism
et bissimulations
VI) Le problème de satisfiabilitéb) Traduction standard de la logique modale en premier ordre. Enoncé du théorème de Van Benthem Idée de la preuve du théorème de Van Benthem (pas montré) a) Algorithme PSPACE
utilisant les ensembles de Hintikka
b) Aperçu de la méthode de tableau Logiciel LotrecScheme pour résoudre le problème SAT pour la logique modale K |
TD3 |
| 3 octobre 2011 | Correspondance
sur les cadres Transparents introduction à la correspondance entre formule modale et propriété du 1er ordre 1) Définissabilité 2) Propriétés du premier et du second ordre 3) Des formules modales récalcitrantes a) Formule de Löb
4) Propriétés du premier ordre non définissablesb) Formule de Mc Kinsey 5) Vers un algorithme pour trouver une formule du premier ordre correspondante à une formule modale a) Un fragment
stupide
b) Les formules uniformes |
TD4 |
| 10 octobre 2011 |
c) Formules de
Sahlqvist (forme simple dans "Modal logic" de Blackburn and cie)
6) Théorème de complétude de SahlqvistDéfinition du fragment de Sahlqvist. Exemple de la réflexivité et de la confluence. Transparents sur l'algorithme pour trouver l'équivalent 1er ordre sur les cadres Logiciel Sqema pour trouver la correspondance d'une formule modale Trois techniques pour montrer la décidabilité/complexité de certains problèmes SAT Transparents introductifs 1) La plus "simple" des logiques modales : le système S5 (TD) |
TD5 |
| 17 octobre 2011 | 2) Méthode de tableau revisité a) Variantes KT, KD
et le problème S4
3) FiltrationsLogiciel LotrecScheme pour résoudre le problème SAT pour pleins de variantes b) S4 et test de boucle Algorithme pour le problème de satisfiabilité de S4 |
TD6 |
| 24 octobre 2011 | Logiques
temporelles Motivation Poly (avec des fautes) 1) Présentation de CTL* et de ses fragments LTL et CTL 2) LTL : logique temporelle linéaire a) Un peu
d'expressivité
b) Satisfiabilité Transparents LTL SAT Lien vers le papier de Sitla et Clarke c) Model-checking Transparents réduction de CORRIDOR-TILING dans le model-checking de LTL |
TD7 |
| 31 octobre 2011 | VACANCES | |
| 7 novembre 2011 | 3) Retour à la logique temporelle branchée Motivation a) Model-checking 4) Expressivité- de CTL* - de CTL a) Comparaison entre LTL, CTL, CTL* b) Comparaison entre CTL, K et S4 c) Bissimulations |
No TD |
| 14 novembre 2011 | Demain, toujours... et le problème de satisfiabilité est EXPTIME-complet Transparents Poly (avec des fautes) 1) Musée a) PDL : Propositional Dynamic Logic 2) Vers un problème EXPTIME-hard intéressant : machines de Turing alternantesb) Logique épistémique et connaissance commune c) Conséquence globale a) Définition
b) Calculs c) Comparaison des classes de complexités - AP = PSPACE - APSPACE = EXPTIME |
TD9 |
| 21 novembre 2011 | Conception de programmes 1) Généralités a) Introduction b) Programmation objet = programmation "sociale" c) Diagrammes de classes d) Exemple du vol illustrant... |
TD10 |
| 28 novembre 2011 | 2) Patrons de conception (recettes de cuisine) Transparents - patrons de créations - patrons de structures - patrons de comportements |
TD11 |
| 5 décembre 2011 | Retour sur "demain, toujours..." d) Application à PDL 3) Comment avoir un algorithme EXPTIME pour PDL ? - Lien entre compacité, modèles (non) standards, modèle canonique filtré |
TD12 |