OBJECTIFS :
Présentation de modèles probabilistes et introduction à la vérification de modèles probabilistes avec la logique PCTL.
CONTENU DÉTAILLÉ DE L’ENSEIGNEMENT :
- Chaines de Markov
- Files d’attente (M/M/1, M/M/m, M/G/1, etc)
- Probabilités transitoires et stationnaires
- Réseaux de files d’attentes
- Réseaux à forme produit (réseaux de Jackson, réseaux BCMP, etc)
- Vérification sur les chaines de Markov et MDP avec la logique PCTL