- Module IN2340
- Lecture: Tuesday 12:30 - 14 in MI 03.09.014 (starting on Oct 18)
- Tutorials: Thursday 10 - 12 in MI 03.09.014 (given by Pranav Ashok)
- Language: English
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.
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.
Here you can find another course on quantitative verification, focusing on probabilistic systems.