Reactive Synthesis Swen Jacobs

News

31.03.2020

Material

Dear students,

I have updated the material by adding photos of the whiteboard proofs from the first lecture, as well as fixing a typo on the bottom of slide 37 in lecture 3.

30.03.2020

Exam

Dear students,

I noticed that some of you that are working on projects are not registered for the exam in the LSF and/or have not written to me regarding their preferences.

If you want to take the exam:

- to still register in LSF, write an email to Evelyn... Read more

Dear students,

I noticed that some of you that are working on projects are not registered for the exam in the LSF and/or have not written to me regarding their preferences.

If you want to take the exam:

- to still register in LSF, write an email to Evelyn Kraska (kraska@cs.uni-saarland.de). She has agreed to manually register you for the exam in our exceptional situation.

- write me an email regarding whether an oral exam on Friday is OK for you or if you'd prefer to have a written exam at some later date.

24.03.2020

Exam and Project

Dear students,

here are some news regarding exam and project.

Regarding the exam: since we will not be able to take a written exam on the scheduled date of April 3, you will have two options:

1. take an *oral* exam on April 3 via videoconference, or

2.... Read more

Dear students,

here are some news regarding exam and project.

Regarding the exam: since we will not be able to take a written exam on the scheduled date of April 3, you will have two options:

1. take an *oral* exam on April 3 via videoconference, or

2. take a written exam *at some later time* that is not determined yet. We will try to figure out something asap.

Please let me know until Sunday which one you prefer.

 

Regarding the project, here are some clarifications:

1. Some of the benchmark examples do not use all identifiers or all colors in the given range (i.e., the highest id is n but some id smaller than n is not used, or similarly for colors). Please make sure that your implementation supports such examples.

2. Some benchmark examples also give a start vertex. You do not have to support these.

23.03.2020

Project Meetings: Last Chance

Dear students,

some of you still have not booked your time slot for the project meeting. In order to finish the project, you have to book a slot for a meeting tomorrow until today 23:59.

Also, once you have booked the meeting, please let us know how we can get... Read more

Dear students,

some of you still have not booked your time slot for the project meeting. In order to finish the project, you have to book a slot for a meeting tomorrow until today 23:59.

Also, once you have booked the meeting, please let us know how we can get access to your code, such that we can have a look at it before the meeting.

18.03.2020

Project Meetings: Doodle Poll

Dear students,

here is the Doodle poll for the project meeting time slots:

https://doodle.com/poll/5vd7rn9cvxg8hc9y

Please enter either the names of both team members, or "Team n", where n is your team id.

You can only choose one option (per team), and... Read more

Dear students,

here is the Doodle poll for the project meeting time slots:

https://doodle.com/poll/5vd7rn9cvxg8hc9y

Please enter either the names of both team members, or "Team n", where n is your team id.

You can only choose one option (per team), and it is first come, first served. When choosing, please keep in mind: if you choose a late time (say on Tue), you will not have much time to work with our feedback before the checkpoint submission.

If for some reason none of the times work for you, please let us know.

 

17.03.2020

Project: Submission of Your Program and Documentation

Regarding submission of your program and documentation, we recommend that you set up your own (private) GitHub or BitBucket repository and give us access. We need access to your code before our meetings, such that we can have a look at your code beforehand.

As an... Read more

Regarding submission of your program and documentation, we recommend that you set up your own (private) GitHub or BitBucket repository and give us access. We need access to your code before our meetings, such that we can have a look at your code beforehand.

As an alternative, you will also be be able to upload your code into the CMS.

17.03.2020

Project Materials, Changes to Schedule and Organization

Dear students,

the project files are now all online:
- the PGSolver files and benchmark library
- a Python BDD package
- a code example for attractor computation
- basic parser files in Python and Java
- a file that defines the output format for strategies,... Read more

Dear students,

the project files are now all online:
- the PGSolver files and benchmark library
- a Python BDD package
- a code example for attractor computation
- basic parser files in Python and Java
- a file that defines the output format for strategies, should you decide to implement strategy extraction

The parser files include a basic ANTLR grammar that can parse multiple lines of the PGSolver format. You have to extend it yourself to make it read a full PGSolver input file and match your intended functionality in your program. We recommend you extend the basic parser based on ANTLR that we provide, but if you prefer to implement a parser in a different way then that's also fine.

We have also included a version in Java that includes some additional example code that takes the resulting parse tree and prints it in a LISP-style human-readable format. Please have a look at the readme files and let us know if something does not work for you.

Moreover, as already announced yesterday, we have to make some on-the-fly adjustments to the organization of the rest of the course. Since there was a delay in getting all the project material online from our side, we will extend both the checkpoint and the final submission of the project by a couple of days:

- the checkpoint date is Tuesday, March 24
- final submission is Tuesday, March 31

Finally, all meetings will only be virtual (using Skype or a similar video conferencing software), we will write a separate news item with a link that lets you sign up for time slots.

16.03.2020

Changes due to Coronavirus Situation

Dear Students,

as you have certainly noticed, a lot has changed since we last met on Thursday. What was a possibility is now a certainty: University is shutting down for the next few weeks, and we will not be able to have the exam on the planned date.

We also... Read more

Dear Students,

as you have certainly noticed, a lot has changed since we last met on Thursday. What was a possibility is now a certainty: University is shutting down for the next few weeks, and we will not be able to have the exam on the planned date.

We also had some delay regarding the project - most of the promised material is available for download, but the parser is still missing.

We will update you tomorrow regarding the project, and as soon as possible regarding the exam!

10.03.2020

Project Teams

Dear students,

for managing project teams, there is now a new option "Teams" in the menu. Please gather in teams of 2 as soon as possible (latest: until the end of the week).

You can then submit your engineering notebooks as a team.

05.03.2020

No Lecture tomorrow, fixed slide from yesterday

Dear students,

as mentioned in the lecture today, there will be no lecture tomorrow. We will meet again on Monday at the usual time.

Moreover, I have fixed the last slide from yesterday's lecture by adding the inputs of the respective functions. The meaning... Read more

Dear students,

as mentioned in the lecture today, there will be no lecture tomorrow. We will meet again on Monday at the usual time.

Moreover, I have fixed the last slide from yesterday's lecture by adding the inputs of the respective functions. The meaning should be much clearer now, please let me know if you have any questions.

See you on Monday!

28.02.2020

Time and Place for Lectures and Tutorials

Dear students,

I have now added information on time and place of lectures and tutorials to the general information page.

Looking forward to seeing you on Monday!

17.02.2020

Schedule

Dear students,

I have updated the information on the course with a rough schedule. More information will be added in the next days.
 

Show all
 

Reactive Synthesis

Advanced Lecture (6 CP), Winter Term 2019/20

Block course in semester break:

Lectures every weekday from March 2 to March 13, from 10:15 to 12:30 (with a 15 min break).
Lecture hall: 0.06 in CISPA building (Stuhlsatzenhaus 5)

Tutorials every weekday from March 2 to March 13, from 14:15 to 16:00.
Seminar room: 1.06 or 2.06 in E1.1.

Project: starts in the second week of lectures, to be submitted until March 27.

Exam: tbd (tentative date: April 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 today's 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
  • Implementation: BDD packages, existing tools, Reactive Synthesis Competition

Schedule

The course will start on March 2nd, with lectures of 2x60min, from 10:15 to 12:30 (incl. 15 min break) every weekday until March 13th. In the second week, we will introduce the project, and after the lectures students will have 2 more weeks  to work (in groups of two) on the project, until March 27th. In addition to the project, we will have an exam on April 3rd.

Grading

The final grade will be composed in equal parts of the project grade and the grade from the exam. For passing the course you need a passing grade in both the project and the exam.

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.



Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators