====== Méthodes formelles approche probabiliste ======


===== Description =====

Dans ce cours, nous présentons des méthodes de vérification automatique pour des systèmes probabilistes. Nous expliquons ainsi comment représenter formellement un système par un modèle et une spécification par un langage mathématique ou une formule et nous intéressons principalement aux modèles ayant des aspects probabilistes comme les chaînes de Markov et les processus de décision Markovien. Nous décrivons de plus des algorithmes de model-checking sur ces modèles. Nous utilisons également l'outil de vérification PRISM qui implémente ces algorithmes de vérification. 


===== Syllabus =====
==== Sujets centraux ====

  - Spécifications temporelles linéaires
    * Propriété de sûreté et de vivacité
    * La logique temporel linéaire LTL
    * Les automates de Büchi
  - Algorithmes de vérification sur les structures de Kripke
  - Vérification de chaînes de Markov à temps discret
    * Définition du modèle
    * Définition de propriétés qualitatives
    * Définitionn de propriétés quantitatives
  - Vérification de processus de décision markovien
    * Définition du modèle
    * Définition des ordonnanceurs
    * Vérification de propriétés d'accessibilité

===== Pré-requis =====
  - Logique
  - Automates
  - Algorithmes dans les graphes
  - Avoir suivi un cours du premier semestre tel que [[modspec9|Modélisation et Spécification]] ou [[mfv9|Méthodes formelles de vérification]] est un plus