Grading (inspiration)
The final grade is the weighted sum 2/3 * oral exam + 1/3 * homework. The oral exam and homework are graded in the range 2–5.
There are 10 questions for the oral exam. It is possible to choose a subset of questions, as follows:
- grade 5: choose 9 questions
- grade 4: choose 6 questions
- grade 3: choose 4 questions
Homework
Please send me your solutions in PDF format.
- First set of homeworks, deadline 2026/04/22.
Calendar
| week | date | lecture | tutorial | note |
|---|---|---|---|---|
| 0 | 23.02 | lecture 01 | XXXXXX | lecture by Piotrek Hofman |
| 1 | 02.03 | lecture 02 | tutorial 02 | LTL and ABA |
| 2 | 09.03 | lecture 03 | tutorial 03 | ABA, NBA, CTL |
| 3 | 16.03 | lecture 04 | tutorial 04 | PDS and LCS |
| 4 | 23.03 | lecture 05 | tutorial 05 | (bi)simulations for NBA |
| 5 | 30.03 | XXXXXX | XXXXXX | monday := friday |
| 6 | 06.04 | XXXXXX | XXXXXX | Easter monday |
| 7 | 13.04 | lecture 06 | tutorial 06 | timed automata |
| 8 | 20.04 | XXXXXX | XXXXXX | cancelled |
| 9 | 27.04 | lecture 07 | tutorial 07 | more timed automata |
| 10 | 04.05 | XXXXXX | XXXXXX | dzień rektorski |
| 11 | 11.05 | lecture 08 | tutorial 08 | size-change termination |
| 12 | 18.05 | lecture 09 | tutorial 09 | Büchi-Landweber theorem |
| 13 | 25.05 | lecture 10 | tutorial 10 | bilinear control systems |
| 14 | 01.06 | lecture 11 | tutorial 11 | probabilistic verification |
| 15 | 08.06 | lecture 12 | XXXXXX | lecture by Piotrek Hofman |
Original plan (14 lectures)
- verification for finite-state systems (2 lectures)
- temporal logics: LTL, CTL, CTL*
- translation from logics to automata
- verification for infinite-state systems (4 lectures)
- pushdown automata
- lossy channel systems
- timed and hybrid automata
- verification of stochastic models (4 lectures)
- discrete and continuous-time finite Markov chains
- recursive Markov chains / probabilistic pushdown automata
- Markov decision processes
- synthesis of finite-state programs (1 lecture)
- Church’s problem
- Büchi-Landweber’s theorem
- control of discrete event systems (1 lecture)
- Ramadge-Wonham problem
- proving termination of programs with the size-change principle (1 lecture)
- computing invariants in polynomial dynamical systems (1 lecture)