Probabilistic Model Checking and Applications

Catalogue des cours de Télécom SudParis

Code

CSC 7339

Niveau

PostGraduate (MSc)

Domaine

Informatique

Langue d'enseignement

Anglais

Crédits ECTS

2,5

Heures programmées / Charge de travail

21

Objectif

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.

Contenu

 

Prérequis

Basics in probability, statistics and stochastic models

Mots-clés

 

Evaluation

 

Approches pédagogiques

 

Programme

Master of Science

Fiche mise à jour : 07/09/2015 15:57:40