Quantitative Verification (IN2340)
Instructors
- Lectures: Prof. Jan Kretinsky
- Tutorials: Alexandros Evangelidis and Kush Grover
Overview
- Module IN2340
- Lectures: Wednesday 10-12 in 03.13.010, Seminarraum(5613.03.010) or online (starting on Oct 20)
- Tutorials: Thursday 10-12 online (starting on Oct 21)
- Language: English
News
- 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.
Content
- 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.