Quantitative Verification (IN2340)




  • The first three lectures (We 10-12) and the first two tutorials (Th 10-12) are online, after this initial period 19.10.-3.11 the teaching in presence will still be reachable also online at bbb for those of you who cannot come.



  • 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.