MPRI - Techniques avancées de vérification -- M2 (2023--2024)

Equipe enseignante 2023-2024

Benedikt Bollig, Patricia Bouyer et François Laroussinie.

Plan de la première partie:

• Présentation de la logique temporelle
  • Logiques temporelles: LTL, CTL,...
  • Problèmes de vérification
• Méthodes algorithmiques à base d’automates pour les logiques temporelles:
  • automate alternant de mots infinis + application à LTL
  • automates d’arbres + application à CTL
• Complexité
• Expressivité

Actualités

Documents

• Exercices sur LTL et les automates.
• Voir aussi l'exemple de spécification avec LTL dans l'article "Up and down, the temporal way" de Howard Barringer (The Computer Journal, vol. 30, nb 2, 1987) que l'on trouve facilement sur Internet.
• Exercices sur les automates d'arbres.

Email: francoisl[at]irif.fr