Quantitative logics
New website for 2014
Starting 2014, this course will use OpenCourseware. Please surf to http://www.ocw.cs.ru.nl/NWI-IMC033.
Introduction
More complex systems require more complete methods to check whether they satisfy their requirements. It becomes too risky to provide systems to customers based on only a few test runs.
This course introduces several variants of model checking, a fully automated method to verify whether a model of (computer) system behaviour satisfies its requirements, expressed in a suitable logic. In particular, we will look at probabilistic logics and other quantitative logics. The models used are variants of Markov chains. Quantitative logics have the advantage that they do not just provide the answer “true” or “false”; a typical outcome is a (real) number that gives more exact information about the degree of satisfaction. As model checking is fully automatic, requiring no complex knowledge of proof strategies or biases of simulation tools, it is the method of choice for industry-scale verification. While the basics of model checking are about 25 years old, we will reach the forefront of research in discussing the newest extensions.
Objectives
- Ability to express requirements and create models of (computer) system behaviour, as far as it fits in the taught formalisms.
- Know the possibilities and limitations of model checking for quantitative models.
- Know examples of model checking algorithms for quantitative models.
- You know about a variety of quantitative logics and their model checking algorithms. In particular, temporal logic; probabilistic logic; stochastic logic; discounting. (Depending on time, I may also include a real-time logic and a logic with rewards.)
- You can demonstrate that you could write (the mathematical logic part of) a simple model checker.
It is not a goal of this course to introduce you to the several optimisation methods like BDDs or symbolic model checking, that are used in practice to handle large models. Nor is it a goal of the course to solve the linear equation systems etc. because you should have learnt that already in your Linear Algebra course.
Schedule
| Wk | Date | Time | Topic | Slides | Literature |
|---|---|---|---|---|---|
| 6 | Tue, Feb 5 | 13.45 | Global overview; refreshers in probability theory, labelled transition systems, CTL model checking | 2013 | Clarke, Emerson, Sistla 1986 |
| Wed, Feb 6 | 15.45 | exercises | 2013 | ||
| 7 | Wed, Feb 13 | 15.45 | Discrete-time Markov chains | 2013 | Hansson, Jonsson 1994 |
| 8 | Tue, Feb 19 | 13.45 | exercises | 2013 | |
| Wed, Feb 20 | 15.45 | Probabilistic CTL | 2013 | ||
| 9 | Tue, Feb 26 | 13.45 | exercises | 2013 | |
| Wed, Feb 27 | 15.45 | PCTL model checking on Markov chains | 2013 | ||
| 10 | Tue, Mar 5 | 13.45 | exercises | 2013 | |
| Wed, Mar 6 | 15.45 | MRMC, the Markov reward model checker | 2013 | ||
| 11 | Tue, Mar 12 | 13.45 | exercises on MRMC. I would be happy if some of you could install it on their laptops. | ||
| Wed, Mar 13 | 15.45 | Markov decision processes | 2013 | Baier, Kwiatkowska 1998 | |
| 12 | Tue, Mar 19 | 13.45 | exercises | 2013 | |
| Wed, Mar 20 | Lecture cancelled—I am ill | ||||
| 13 | Tue, Mar 26 | 13.45 | PCTL model checking on MDPs | 2013 | |
| Wed, Mar 27 | 15.45 | ||||
| 16 | Tue, Apr 16 | 13.45 | exercises on the model checker PRISM. I would be happy if some of you can install it on their laptop. | ||
| Wed, Apr 17 | 15.45 | Continuous-time Markov chains | 2013 | ||
| 17 | Tue, Apr 23 | 13.45 | exercises | 2013 | |
| Wed, Apr 24 | 15.45 | CTMCs, continued, and Continuous Stochastic Logic (including multiple until) | 2013 | Baier, Haverkort, Hermanns, Katoen 2003 | |
| 19 | Tue, May 7 | 10.45 | exercises | 2013 | |
| Wed, May 8 | No lecture—I am absent | ||||
| 20 | Tue, May 14 | 13.45 | repetition? | ||
| Wed, May 15 | 15.45 | CSL model checking (without multiple until) | 2013 | ||
| 21 | Tue, May 21 | 13.45 | exercises | 2013 | |
| Wed, May 22 | 15.45 | MRMC as a model checker for CTMCs | 2013 | ||
| 22 | Tue, May 28 | 13.45 | exercises | Problems 2 and 3 from last week | |
| Wed, May 29 | 15.45 | Discounted CTL | 2012 | Alfaro, Faella, Henzinger, Majumdar, Stoelinga 2005 | |
| 23 | Tue, June 4 | 13.45 | exercises | 2013 | |
| Wed, June 5 | 15.45 | DCTL model checking | (p. 161sq. of the article) | ||
| 24 | Tue, June 11 | 13.45 | exercises | ||
| Wed, June 12 | 15.45 | Outlook into bisimulation | 2013 | Derisavi, Hermanns, Sanders 2003 | |
| 25 | Tue, June 18 | 13.45 | exercises | 2013 | |
| Wed, June 19 | 15.45 | Recapitulation, questions | |||
| 27 | Tue, July 2 | 10.30 |
Examination | ||
Evaluation
Written exam on July 2.
Extra information
Students are encouraged to express their own interest, so that the programme can be adapted.
