Single-Course English 7.5 ECTS

Model Checking

Overall Course Objectives

Model checking is a set of modelling and analysis techniques combining logic, graph-based models of computation (automata, transitions systems, Markov chains,…), probabilities, statistics, constraint solving, artificial intelligence and game theory. Following this course the students will be able to apply model checking techniques for modelling, specification and validation/verification for various classes of systems (distributed/concurrent systems, schedulers, controllers, networks, biological systems, games, etc.). The students will also understand how model checking complements other formal methods techniques and they will understand the connections to other fields such as artificial intelligence.

Learning Objectives

  • explain the characteristic features of a given system;
  • explain the basic concepts of the process oriented approach to modelling, specification and validation/verification of systems;
  • explain the covered modelling formalisms and use them to model systems;
  • explain the covered logical specification formalisms and use them to specify properties related, e.g., to safety, security and performance;
  • operate state-of-the-art verification tools and explain the overall workings of such tools;
  • identify situations where the covered techniques apply;
  • motivate and design a series of experiments using verification tools and interpret the results obtained;
  • achieve the above goals in a group effort while at the same time maintaining individual accountability; and
  • communicate his/her results in a clear and precise manner using a standard form for technical reports.

Course Content

The course covers three main topics:
(1) Methods for modeling systems with features such as non-determinism, probabilistic/stochastic aspects, and multiple agents/objectives: transition systems, Markov models, and games.
(2) Logical formalisms for expressing properties related to the safety, security, and performance of systems.
(3) Validation and verification tools that determine the relationship between models and properties in order to establish strong guarantees related to safety, security, and performance.

Recommended prerequisites

02141, The students are expected to be familiar with finite automata and/or transition systems; this background can be obtained in the course 02141. The students are expected to have a basic knowledge about probability theory. The students must be able to write programs in a programming language.

Teaching Method

Lectures, theoretical exercises, and practical exercises.

See course in the course database.





13 weeks




DTU Lyngby Campus

Course code 02246
Course type Candidate
Semester start Week 35
Semester end Week 48
Days Tues 13-17

11.250,00 DKK