Reactive Synthesis Swen Jacobs, Martin Zimmermann

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. 

You are cordially invited to participate in the scientific program. As long as there is space in the room (001 in E1 7),  just drop by for the talks you are interested in. Please find the program and more information on our web page

https://www.react.uni-saarland.de/gandalf2018/program.html

This conference is an excellent opportunity to learn about current research on automata theory, logics, and verification. In particular, the three invited speakers are leading experts in these areas you give exciting presentations.

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.

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.

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.

Few remarks/reminders for the Project's submission:

• Provide a clear command to run your tool
• If possible, external libraries should be included in compiled form
• Do not forget to submit your engineering notebook
• Two projects with identical code will not pass

Good luck!

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.

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.

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!