Swedish web site
Theory and Application of Probabilistic Model Checking2015HT
|
|
Course plan
Lectures
8 lectures, reading assignments and an examination seminar
Recommended for
PhD students curious about probabilistic based methods to formally reason about properties of runs of transition systems.
The course was last given
This course is a quite different specialisation of the "introduction to automatic verification" course last given in VT2014.
Goals
After the course, the students will be able to:
* model computer algorithms, protocols, components or systems as probabilistic
transition systems
* specify correctness criteria using examples of probabilistic temporal logics
* understand what it means for a model to verify a correctness property
* apply an existing tool for modelling and analysing a probabilistic transition
systems
Prerequisites
Basic notions in probabilities, automata theory and logic.
Organization
Lectures, reading assignments and examination seminar
Contents
Introduction to probabilistic model checking. Probabilistic temporal logics. Model checking discrete-time Markov chains, Markov decision processes, continuous time Markov chains, verification techniques and applications.
Literature
* Lecture material
* Distributed papers
Lecturers
Ahmed Rezine
Examiner
Ahmed Rezine
Examination
One of two (depending on students interest):
* Modelling and verification of a case study, preferably from the student
research
* Detailed reading of recent research paper proposed by the examiner
A presentation by the student in a seminar session will take place in both
cases.
Credit
6pt
Page responsible: Director of Graduate Studies
