Advanced Lecture (Vertiefungsvorlesung), Summer Term 2016, 6 CP
| People: |
Martin Zimmermann, Alexander Weinert |
| Contact: |
infinitegames16@react.uni-saarland.de |
| Lecture Room: |
E1 3, HS 003 |
| Lectures: |
Tuesdays, 10:15-12:00 |
| Tutorials: |
Mondays, 14:00-16:00, E1 3, Room 016 |
| Exams: |
End of Term: Mon, Aug 1st, 2016, 10 am |
| |
End of Semester: Tue, Sep 20th, 2016, 10 am |
| Exam room: |
E1 3, HS 003 |
News
- Tue, Jul 26th: The lecture notes have been updated to the final version and the recap slides have been uploaded.
- Mon, Jul 25th: Figure 4.2 in the lecture notes has been updated to present a finite-state strategy with a non-trivial initialisation function.
- Tue, Jul 19th: The lecture notes have been updated to include the proof of Rabin’s theorem. Also, we included a chapter about infinite games in infinite arenas that we did not cover this year. This chapter is not relevant for the exams. If you find bugs in the lecture notes, please inform us. We will fix them and announce them here.
- Thu, Jul 14th: The last regular lecture is on Tuesday, July 19th. On Tuesday, July 26th, we present a recap and an outlook on further aspects of infinite games not covered during the course.
- Thu, Jul 14th: In preparation of the exam, on Monday, July 25th we offer a question-and-answer session instead of the problem class.
- Tue, Jul 12th: There was a typo in the announcement of the day of the second exam: It will be held on Tuesday, September 20th, not on the August 20th.
- Tue, Jul 12th: The thirteenth problem set is now available and the lecture notes have been updated to include the proof of closure of parity tree automata under complementation.
- Tue, Jul 5th: The twelfth problem set is now available and the lecture notes have been updated to include an introduction to parity tree automata.
- Tue, Jun 28th: The eleventh problem set is now available and the lecture notes have been updated to include an introduction to S2S.
- Tue, Jun 21st: The tenth problem set is now available and the lecture notes have been updated to include an undetermined game.
- Tue, Jun 14th: The ninth problem set is now available and the lecture notes have been updated to include the Borel hierarchy and Wadge reductions.
- Tue, Jun 7th: The eighth problem set is now available and the lecture notes have been updated to include Muller games.
- Tue, May 31st: The seventh problem set is now available and the lecture notes have been updated to include finite-memory strategies.
- Tue, May 24th: The sixth problem set is now available and the lecture notes have been updated to include the progress measure algorithm.
- Tue, May 17th: The fifth problem set is now available and the lecture notes have been updated with an appendix on posets and complete lattices. Also, we added exercisees to the lecture notes.
- Tue, May 10th: The fourth problem set is now available and the lecture notes have been updated to include Parity games.
- Tue, May 3rd: The third problem set is now available and the lecture notes have been updated to include Büchi- and Co-Büchi games.
- Tue, Apr 26th: The second problem set is now available and the lecture notes have been updated to include reachability- and safety games.
- Tue, Apr 19th: The first problem set is now available.
- Tue, Apr 19th: The lecture notes are now available.
- Fri, Jan 8th: The first lecture is on Tuesday, April 19th, 2016. The tutorial slot will be determined during the first lecture.
Student Profile
This course is aimed at mathematically interested students that enjoy beautiful proofs that capture intuitive descriptions of strategies, appreciate deep connections to logics, and value an occasional hard open problem. Also, you should like to play games: we plan to have a tournament where students will submit games to a pool that can be be solved in order to earn points towards exam admission. Besides this, we will have regular problem sets as well.
Syllabus
Many of todays problems in computer science are no longer concerned with programs that transform data and then terminate, but with non-terminating systems which have to interact with a possibly antagonistic environment. The emergence of so-called “reactive systems” requires new approaches to verification and synthesis. Over the course of the last fifty years it turned out to be very fruitful to model and analyze reactive systems in a game-theoretic framework, which captures the antagonistic and strategic nature of the interaction between the system and its environment.
In this lecture, we will study different types of two-player games of infinite duration: typical questions we will answer are “how hard is it to determine the winner of a given game?”, “what kind of strategy does the winner need to win the game?”, and “does every game have a winner?”. Also, we discuss applications of infinite games in logics by proving Rabin’s theorem, sometimes called the “mother of all decidability results”.
Topics
- Introduction: reachability and safety games, Büchi and co-Büchi games, parity games.
- Memory: finite-state strategies, reductions, Muller games, limits of reductions, and non-determined games.
- Application: tree automata, MSO over trees, Rabin’s theorem.
Lecture Notes
- We will follow the lecture notes from the winter term 2013-14, which will be updated during the term: lecture-notes.pdf
