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)
Homeworks
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 | |
| 2 | 09.03 | lecture 03 | tutorial 03 | |
| 3 | 16.03 | lecture 04 | tutorial 04 | |
| 4 | 23.03 | lecture 05 | tutorial 05 | |
| 5 | 30.03 | XXXXXX | XXXXXX | monday := friday |
| 6 | 06.04 | XXXXXX | XXXXXX | Easter monday |
| 7 | 13.04 | lecture 06 | tutorial 06 | |
| 8 | 20.04 | XXXXXX | XXXXXX | cancelled |
| 9 | 27.04 | lecture 07 | tutorial 07 | |
| 10 | 04.05 | XXXXXX | XXXXXX | dzień rektorski |
| 11 | 11.05 | |||
| 12 | 18.05 | |||
| 13 | 25.05 | |||
| 14 | 01.06 | |||
| 15 | 08.06 |