Cours/TD/Tp Méthodes formelles - Vérification probabiliste
M2 Informatique 2021-2022

• Jeudi 8h30-11h30. Salle 1001 Sophie Germain

• Responsable du cours : Arnaud Sangnier

• Systèmes de transitions
• Propriétés temporelles linéaires
• Propriétés de sûreté régulières
• Propriétés temporelles linéaires régulières
• La logique LTL
• Chaînes de Markov et propriétés
• Accessibilité dans les Chaînes de Markov
• Vérification qualitative dans les Chaînes de Markov
• Vérification de Processus de Décision Marovien

• Td1
• Td2
• Tp1
• Tp2
• Td3
• Td4

• Examen 2021
• Examen 2020
• Examen 2019

Le devoir est à rendre par mail à sangnier@irif.fr au plus tard le vendredi 18 mars 2022 à 23h59. Les modalités de rendu sont précisées dans l'énoncé.

• Enoncé

• Site du model-checker PRISM
• "Principles of Model-Checking" : M. Christel Baier and Joost-Pieter Katoen. MIT Press, 2008.