- Module IN2340
- Lecture: Tuesday 14:05 - 15:35 in MI 03.09.014 (starting on Oct 17)
- Tutorials: Thursday 10:15 - 11:45 in MI 03.09.014 (given by Pranav Ashok)
- Language: English
- The following irregularitites during the semester are to be noted:
- Nov 5: Please bring your laptops on Tuesday, we will actively use Uppaal.
- Oct 28: The Lego robot model has been updated.
- Oct 24: The lectures-exercises schedule has been updated.
- Oct 17: In the first lecture, we discussed a few motivational case studies. We shall start with the technical content only in the next lecture. Therefore, everyone who missed the first lecture is still very welcome to join for Thursday exercises or next week for the second lecture.
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.
Here you can find another course on quantitative verification, focusing on probabilistic systems.