News
18.09.2018
|
GandALF 2018: International Symposium on Games, Automata, Logics, and Formal VerificationAs mentioned during the last lecture, the conference GandALF (International Symposium on Games, Automata, Logics, and Formal Verification) takes place in Saarbrücken this year, organized by the Reactive Systems Group. The program contains presentations on topics... Read more As mentioned during the last lecture, the conference GandALF (International Symposium on Games, Automata, Logics, and Formal Verification) takes place in Saarbrücken this year, organized by the Reactive Systems Group. The program contains presentations on topics covered by our course, in particular the three invited talks and the sessions on games. |
06.04.2018
|
Grades and Inspection of Re-ExamWe just filed the grades for the re-exam and updated the grades for the course accordingly, they should now be visible to you. If you have any questions or want to inspect your re-exam, please contact us until the end of next week (April 13th). If we have not... Read more We just filed the grades for the re-exam and updated the grades for the course accordingly, they should now be visible to you. If you have any questions or want to inspect your re-exam, please contact us until the end of next week (April 13th). If we have not heard from you until then, we will post the final grades to LSF. |
12.03.2018
|
Re-ExamThe re-exam for Reactive Synthesis will be next week, Tuesday March 20, at 14:15 in Lecture Hall 3 in E1 3 (i.e., our usual lecture hall). Please be there 5 min early, so we can start on time. Last time we checked, more people had "registered" with us by email... Read more The re-exam for Reactive Synthesis will be next week, Tuesday March 20, at 14:15 in Lecture Hall 3 in E1 3 (i.e., our usual lecture hall). Please be there 5 min early, so we can start on time. Last time we checked, more people had "registered" with us by email than were registered in the official LSF. If you want to participate and have not yet registered in LSF, please do so. |
01.02.2018
|
Exam InspectionWe just filed the grades for the exam and the course. You should have received two emails, one with your grade in the exam and one with the grade for the course. If you have not, please contact Swen or Martin.
The exam inspection takes place on Monday,... Read more We just filed the grades for the exam and the course. You should have received two emails, one with your grade in the exam and one with the grade for the course. If you have not, please contact Swen or Martin.
The exam inspection takes place on Monday, February 5th from 10 to 11:30 in Room 1.13 (E 1 1, Swen's and Martin's office).
If you want to take the second exam (20.03.18), please send an email to Martin. |
30.01.2018
|
A note on automataNote that (according to our definition) deterministic automata are always complete, i.e., for every state q and every letter a there is an outgoing a-transition from q.
Please make sure that your deterministic automata are complete in the exam. |
29.01.2018
|
Project GradesA few minutes ago, you should have received an email with your project grades. If you did not get this email or if you want to discuss your grade, please let us know. |
17.01.2018
|
Bug on problem set 7We just uploaded problem set 7. In comparison to the printed version handed out during the lecture, we fixed a bug in the definition of the second property. Thank you for notifying us!
Also, we added a clarification. |
11.01.2018
|
Project - Phase 2Few remarks/reminders for the Project's submission:
Few remarks/reminders for the Project's submission:
Good luck! |
10.01.2018
|
Exam: Conflict with Operating Systems, Part 2Due to our exam being scheduled just after the exam for the lecture "Operating Systems", we offer two options to those that want to take both exams: - Either, you can take part in the written exam, which starts at 14:30 the earliest. - Or you can take an oral... Read more Due to our exam being scheduled just after the exam for the lecture "Operating Systems", we offer two options to those that want to take both exams: - Either, you can take part in the written exam, which starts at 14:30 the earliest. - Or you can take an oral exam. In this case, write an email to Martin Zimmermann to set up a date. Please write the email before January 24th. |
28.12.2017
|
Exam: Conflict with Operating SystemsThere is a scheduling conflict between our exam and the one for the lecture Operating Systems.
If you are affected, please write an email to zimmermann@react.uni-saarland.de. |
15.12.2017
|
Benchmarking framework and latest slides onlineNow available under Materials: - the benchmarking framework, including more benchmarks and tools for checking and evaluating your synthesis tool - the slides from last lecture (regarding the confusion about QBF formulas in algorithms: the formulas were... Read more Now available under Materials: - the benchmarking framework, including more benchmarks and tools for checking and evaluating your synthesis tool - the slides from last lecture (regarding the confusion about QBF formulas in algorithms: the formulas were correct, but the algorithms use a form of generalization that does not negate the whole formula, but only a part of it; I have added a remark to the slides) - the paper by Bloem et al. mentioned in the slides.
|
08.11.2017
|
Problem Set 3Problem Set 3 is now online. The deadline is on the 14th of November before the tutorial. |
08.11.2017
|
APPLY AlgorithmIt was pointed out to me that the APPLY algorithm, as presented in the lecture, did not properly reflect the fact that the current root nodes of the two BDDs could be labeled with different variables. In that case, the recursion only considers the successor nodes in... Read more It was pointed out to me that the APPLY algorithm, as presented in the lecture, did not properly reflect the fact that the current root nodes of the two BDDs could be labeled with different variables. In that case, the recursion only considers the successor nodes in the BDD that is rooted in the maximal variable (and re-uses the current root node for the other BDD). I have already fixed this in the slides, thanks for pointing it out! |
25.10.2017
|
ExamsThe exam dates have been fixed. The first one takes place on January, 31st instead of the last lecture. The lecture has been moved to January, 30th. No exam relevant material will be presented during this last lecture. The re-exam is scheduled for March, 20th, 14:15. |
23.10.2017
|
First TutorialAs determined in the first lecture, the tutorials will be on Tuesdays at 14:15. We will meet for the first time tomorrow in Seminar Room 15, E1.3. See you there! |
18.10.2017
|
Problem Set 1, Exercise 1.1(a)Try your best, but also be bold when you think it is impossible to solve! In any case, argue your claims. |
04.09.2017
|
Registration OpenIf you plan to participate in this course, please register. It helps us in planning the course, and you will get future news and announcements by email. |
31.08.2017
|
First LectureThe first lecture is on Wednesday, October 18th, 2017. The tutorial slot will be determined during the first lecture. |
Reactive Synthesis
Advanced Lecture (6 CP), Winter Term 2017/18
Wednesdays 14:15-16:00, in HS 003, E1.3
Student Profile
This course is aimed at students that are interested in reactive synthesis in its full breadth, ranging from its theoretical formalization as an infinite game to efficient algorithms and data structures to solve the synthesis problem, and in the implementation of state-of-the-art algorithms for practically relevant and challenging problems.
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 that are in constant interaction with their (possibly antagonistic) environment. Over the course of the last fifty years it turned out to be very fruitful to model and analyze such “reactive systems” in a game-theoretic framework, which captures the antagonistic and strategic nature of the interaction between the system and its environment. Despite the prohibitive complexity of these problems in general, in recent years it has been shown that many benchmark problems can be solved automatically by efficient implementations of game-solving algorithms.
In this lecture, we will introduce different types of two-player games of infinite duration, and algorithms to solve them. To obtain efficient implementations, we will also cover automated reasoning methods that can be used as subprocedures in a synthesis algorithm, as well as data structures that can efficiently represent important aspects of infinite games.
During the course, students will implement a synthesis tool using their knowledge acquired during the lecture. At the end of the course, the resulting tools will be compared against each other and state-of-the-art tools on a set of benchmarks from the official Reactive Synthesis Competition.
Topics
- Theoretical Basics: reachability and safety games, Büchi and co-Büchi games, parity games
- Efficient Algorithms and Data Structures: fixpoint algorithms, strategy extraction, BDD representation and operations, incremental algorithms, SAT solving
- Implementation: BDD packages, SAT solvers, existing tools, Reactive Synthesis Competition
Grading
The final grade will be composed of the project grade and the grade from an exam. For admission to the exam, students most solve a certain percentage of exercises during the course.
Teaching Material
For background on infinite games, see the lecture notes from the course Infinite Games. Here, we will cover a subset of the topics of the first three chapters.