Probabilistic Model Checking and Applications

Catalogue des cours de Télécom SudParis

Code

IGFE CSC 7339

Niveau

MSc

Graduate

PostGraduate

Domaine

Informatique

Programme

Master of Science

Langue

Anglais/English

Crédits ECTS

2,5

Heures programmées

21

Acquis d'apprentissage

In this course we are going to learn the basic principles of probabilistic model checking, a well-established technique for the verification/analysis of probabilistic models. The course will contain an introductory part on stochastic processes (Discrete/Continuous Time Markov chains) as well
as an introductory part on probabilistic temporal logics (PCTL, CSL), i.e. the formal languages for specifying properties of stochastic models which probabilistic model checking is based upon.
The course will then present the algorithms for verifying temporal logic properties against probabilistic models.
The course will contain also a number of tutorials where the students will be asked to develop complete models and to analyse by means of
standard probabilistic model checking tools such as the PRISM model checker. The analysis of standard communication protocols such as, for example the IEEE 802.11 family of distributed coordination functions will be proposed as a case-study to the participants.

Prérequis

Basics in probability, statistics and stochastic models

Fiche mise à jour le 07/09/2015