Quantitative Verification (IN2340)


  • Module IN2340
  • Lectures: Tuesday 12-14 in MI HS2 or online (starting on Nov 3)
  • Tutorials: Wednesday 10-12 in MI HS2 or online
  • Language: English


  • Feb 5: Exercise sheet 11 is available now.
  • Feb 1: Exercise sheet 10 is available now.
  • Jan 25: Exercise sheet 9 is available now.
  • Jan 19: Exercise sheet 8 is available now.
  • Jan 9: Exercise sheet 7 is available now.
  • Dec 21: Exercise sheet 6 is available now.
  • Dec 16: Exercise sheet 5 is available now.
  • Lecture and tutorial have been swapped for the next week i.e. the tutorial is on Tuesday, 8th Dec and the lecture is on Wednesday, 9th Dec.
  • Dec 3: Exercise sheet 4 is available now.
  • No lecture or tutorial on 02.12.2020.
  • Nov 22: Exercise sheet 3 is now available.
  • Nov 12: Exercise Sheet 2 is available now.
  • Nov 9: The first tutorial will be on 11.11.2020 from 10:05 to 11:35. This tutorial will be on UPPAAL model checker. You can find the link to the BBB room for tutorials above, there's no access code required for now. Note that it is different from the BBB room for lectures.
  • Nov 1: The first week, we have a lecture in both slots. Besides, due to the higher number of registred participants, the lectures will be held ONLINE until further notice (decrease of participants, change in regulations or TUM recommendations).


  • This course is concerned with modelling, specification and analysis of hardware and software systems, focusing on the fundamental aspects of time, probability, cost, and their combinations. We provide a way to ask and automatically answer questions on dependability and performance, such as "Is it possible that the system will crash within 30 seconds?", "What is the probability of a system failure in the next 24 hours?", or "How to schedule tasks in a business process at a minimum cost?"
  • The main topics are
    • timed automata and timed logics,
    • Markov chains, Markov decision processes, probabilistic logics, optimization criteria and algorithms,
    • continuous-time stochastic systems and hybrid systems.
  • The previous knowledge from the model-checking course may be advantageous, but is not required. Similarly, the knowledge from the automata course may be advantageous since the systems dealt with are essesntially automata with time and/or probabilities. However, the course is self-contained.
  • The first part of the lecture will cover topics of Chapters 9 and 10 of the book Principles of model cheking by Christel Baier and Joost-Pieter Katoen. The second part will focus on some recent research development. Many thanks go to people who provided (parts of) their slides on the concerned topics, namely Patricia Bouyer-Decitre, Tomas Brazdil, Holger Hermanns, Jan Krcal, Kim G. Larsen, Jeremy Sproston and others.