Model Checking

This course provides an introduction to model checking, a formal verification technique used to ensure that systems behave as intended. In the first part, students learn the foundations of classical model checking, including how to model systems as Kripke structures, express properties in temporal logics (CTL, LTL), and apply core model checking algorithms. The second part introduces probabilistic model checking, covering discrete-time Markov chains, probabilistic temporal logics (pCTL), and model checking algorithms based on linear programming and value iteration. The course concludes with applications to decision-making under uncertainty, particularly in reinforcement learning and runtime safety enforcement, using modern probabilistic model checkers, such as Prism or Storm.

At the end of the course, students will be able to:

- Model system behaviour using Kripke structures and probabilistic transition systems.
- Specify correctness properties using temporal logics such as CTL, LTL, and pCTL.
- Explain the semantics and expressiveness of classical and probabilistic temporal logics.
- Apply model checking algorithms to verify CTL and LTL specifications.
- Explain probabilistic model checking techniques for Markov chains and MDPs.
- Use probabilistic model checking tools such as Prism and Storm to model and verify simple properties.

Target group: This course is intended for students with an interest in computer science, particularly those who wish to learn about formal verification and the use of mathematical methods to ensure system correctness.

Prerequisites: Students are expected to have a basic background in discrete mathematics (sets, relations, graphs). Familiarity with automata theory, formal languages, and probability theory is helpful but not required. Programming experience is beneficial for practical exercises, though no specific language is required.

Evaluation: Students will complete several assignments during the course. In addition to submitting their solutions, they are expected to present them during recitations once or twice, depending on class size. Alternatively, students may choose to be graded based on a single comprehensive final exam.

Teaching format: Lectures

ECTS: 3 Year: 2025

Track segment(s):
Elective

Teacher(s):
Filip Cano Cordoba

Teaching assistant(s):
Ehsan Kafshdar Goharshadi