IGFE CSC 7339

MSc

PostGraduate

Master of Science

Anglais/English

2,5

21

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.

Basics in probability, statistics and stochastic models

Fiche mise à jour le 07/09/2015