Reactive Synthesis Swen Jacobs, Martin Zimmermann

News

06.04.2018

Grades and Inspection of Re-Exam

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... 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-Exam

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... 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 Inspection

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,... 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 automata

Note 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 Grades

A 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 7

We 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 2

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... Read more

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!

10.01.2018

Exam: Conflict with Operating Systems, Part 2

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... 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 Systems

There 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 online

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... 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 3

Problem Set 3 is now online. The deadline is on the 14th of November before the tutorial.

08.11.2017

APPLY Algorithm

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... 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

Exams

The 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 Tutorial

As 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 Open

If 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 Lecture

The first lecture is on Wednesday, October 18th, 2017. The tutorial slot will be determined during the first lecture.

Show all
 

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.



If you encounter technical problems, please contact the administrators