Magistère STIC , deuxième année

Notes de cours, exercices, logique et automates, premier semestre 2003

• Bibliographie (liste complète)
• Bibliographie (liens vers les principales sources)
• Cours du 20 octobre:
  • Introduction
  • La logique LTL: définitions
  • La logique monadique de second ordre à un successeur
  • Les automates de Büchi alternants
  • Exercices pour le 24 octobre: 1 (page 3)
• Cours du 24 octobre
  • Automates alternants et logique LTL: passage en temps linéaire des formules de LTL aux automates; la satisfaisabilité et la vérification en LTL sont PSPACE-complets .
  • Automates alternants faibles avec condition de parité.
  • Exercices pour le 3 novembre: 13, 14, 15 (page 26), 19, 20 (page 28)
• Cours du 3 novembre:
  • Passage des automates de Büchi aux automates alternants faibles avec condition de parité.
  • Jeux à parité: définition et déterminisme des jeux à parité faible.
  • Exercices pour le 7 novembre: 22 page 28
• Cours du 7 novembre :
  • Jeux à parité: stratégies sans mémoire et lien avec les automates alternants
  • Une autre preuve du théorème de Buchi
• Cours du 10 novembre:
  • Jeux à parité: recherche de stratégies gagnantes; questions de complexité
  • Solution de quelques exercices du chapitre 7 en particulier, déterminisme des jeux à parité finis.
  • Ensemble du chapitre 7
• Cours du 14 novembre:
  • Logique monadique du second ordre à k successeurs: définition et exemples. Le vide des automates d'arbres à parité est dans co-NP.
  • Les logiques CTL et CTL*;
• Cours du 17 novembre:
  • Traduction de CTL et CTL* en SkS (dans le cas de modèles à branchement borné)
  • Automates d'arbres alternants: définition et exemples
  • Automates d'arbres alternants: passage de CTL aux automates alternants faibles en temps linéaire
  • Les notes de cours du 17 novembre
• Cours du 21 novembre (prévisions):
  • Applications: la vérification est PTIME-complète pour CTL (condition simple de victoire dans un jeu à parité faible).
  • La satisfaisabilité est DEXPTIME-complete
  • Notes de cours: satisfaisabilité et vérification en CTL
  • Automates d'arbres alternants hésitants; les modèles d'une formule de CTL* sont reconnus par un automate hésitant.
• Cours du 24 novembre (prévisions):
  • La vérification de modèles en CTL*: une question de jeux.
  • introduction au mu-calcul; liens avec SkS.
• Cours du 28 novembre (prévisions):
  • quelques résultats simples sur les ordinaux et les calculs de point fixe
  • Automates d'arbres alternants et mu-calcul
• Cours du 1 Décembre (prévisions):
  • Conséquence pour la vérification de modèles en mu-calcul
• Au mois de janvier (prévisions): retour sur le théorème de Rabin; une preuve fondée sur les jeux.