DD2552 semteo21 HT21-1 Seminars on Theoretical Computer Science, Programming Languages and Formal Methods

DD2552 semteo21 HT21-1 Seminars on Theoretical Computer Science, Programming Languages and Formal Methods

Short summary of the course

This seminar course covers the basics of formal specification and verification of probabilistic systems. It focuses in particular on verification using probabilistic logics such as PCTL of Markov processes, using model checking tools that use numeric-symbolic and statistical methods.

Examination and grades

The default examination in the course is through solving the set of homework problems in hw.pdf. The handed-in solutions are given a grade of A, B, C, D, E, FX, or F, which is also the student's grade on the course as a whole. Homework solutions must be sent as a PDF file to palmskog@kth.se by January 14, 2022, 23:59 CET, for the results to be reported to LADOK before the beginning of period 3 of the 2021/2022 academic year.

As a special one-time concession due to earlier issues in the course, students can elect to, instead of homework, take a 1-hour oral examination with the course lecturer during the winter exam week, January 10 to January 14. The oral exam will be given a grade of A, B, C, D, E, FX, or F, which is then the grade on the course as a whole. Students must contact palmskog@kth.se by December 22, 23:59 CET to book a time if they want to use this examination option. The oral examination will be about problems similar to the homework problems. 

Re-examination

The re-examination in the course during spring 2022 is by solving a new set of homework problems. The handed-in solutions are given a grade of A, B, C, D, E, FX, or F, which is also the grade on the course as a whole.

The re-examination homework problem set will appear on the course website on March 14, 2022.

The re-examination homework problem solutions must be sent to palmskog@kth.se by April 22, 2022, 23:59 CET, for the results to be reported into LADOK for the 2021/2022 academic year.

Intended learning outcomes and the examination

The intended learning outcomes are that after passing the course, the student shall be able to:

1. discuss advanced concepts within the area of the course
2. attack problems within the area of the course actively, both through own work and through search of relevant information
3. assimilate and present the essential contents of scientific articles within the area of the course.

In the homework problems, the intention is that different numbers of total points correspond to different degrees of outcome 2. Outcome 1 and 3 are also examined by the homework by the choice of problems and by the references to research literature.

Course literature

The main course literature is a survey on statistical model checking

Please contact palmskog@kth.se if you are unable to download a PDF copy of the survey.

Seminars

Weekday Date Content References
Monday Aug 30 CTL, PCTL introduction sem1.pdf
Thursday Sep 2 PCTL semantics & DTMCs sem2.pdf
Monday Sep 6 PCTL decidability, CTMCs sem3.pdf
Thursday Sep 9 CTMCs and CSL sem4.pdf
Monday Sep 13 CSL statistical verification sem5.pdf
Thursday Sep 16 Error control and estimation sem6.pdf
Monday Sep 20 Comparison of verification methods sem7.pdf
Thursday Sep 23 Nondeterministic systems sem8.pdf
Monday Sep 27 Probabilistic timed automata sem9.pdf
Thursday Sep 30 Timed automata tools and hybrid systems sem10.pdf
Monday Oct 4 Bayesian modeling, estimation, and testing sem11.pdf
Thursday Oct 7 Case studies in system verification
Monday Oct 11 Case studies in system verification
Thursday Oct 14 PRISM tool demonstration PRISM