IST Austria Courses
IST Austria logo

Advanced topics in Formal Methods

Instructor: Krish Chatterjee

Teaching Assistant: Mirco Giacobbe, Przemyslaw Daca



In this course we will study some advanced topics in formal methods. In particular we will study various classes of graph games and probabilistic systems. Graph games arise in the synthesis problems, and probabilistic systems arise in analysis of randomized protocols, as well as systems that interact with nature. In this course we will study the basic properties of these models, and algorithms to solve them. We will also study the different complexity classes where the computational problems for these models lie, and discuss most important open questions in this area.


The attendee will be required to solve weekly homeworks and to give a paper presentation at the end of the course. Homeworks are handed out on Wednesday.




Final Grade

 50% weekly homeworks, 50% final presentation


Mon 8:45 - 10:00, Mondi 3.

Wed 8:45 - 10:00, Mondi 3.

Starts on Mon 4 May.

Ends on Wed 1 Jul.


Some useful lecture notes can be found here.



Date Topic Videos Blackboards Slides
May 04 Graph games [part1]    
May 06 Reachability objectives [part1] [part2] [part3]    
May 11 Büchi objectives [part1] [part2] [part3] [11] [12] [13] [21] [22]  
May 13 O(n²) algorithm for Büchi [part1] [part2] [part3] [11] [12] [13] [21] [22]  
May 18 Parity games [part1] [part2] [part3] [11] [12] [13] [21] [22]  
May 20 Algorithms for parity [part1] [part2] [part3] [part4] [11] [12] [13] [21] [22]  
May 27 Subexponential parity + MDPs [part1] [part2] [part3] [11] [12] [13] [21] [22] [23]  
June 1 MDPs + concurrent games [part1] [part2] [11] [12] [13] [21] [concgames]
June 3 Stochastic games [part1] [part2] [part3]    
June 8 Quantitative objectives in MDPs [part1] [part2] [part3]   [qobj] [qobj+notes]


File Due Date
[hw1.pdf] May 13
[hw2.pdf] May 20 May 27
[hw3.pdf] May 28
[hw4.pdf] Jun 3
[hw5.pdf] Jun 10 Jun 17