Automata, Games, and Verification Bernd Finkbeiner

Dear Students,

The current date and time of the re-exam is set to march 26th, from 2pm to 4pm. However, the time slot collides with another appointment of us, which is why we plan to shift it to an earlier time.

Our new proposed time slot for the re-exam will be from 10am to 12am, still on march 26th.

If this causes a probem for you, please inform us as soon as possible (the latest till the 8th of march).

Kind Regards,
the Automata, Games, and Verification Team

The correct answer for warm-up question 14.2 is that deterministic Muller tree automata are closed under intersection, but not under union or complement. The issue is that the language of {0, 1}-labeled trees that have (at least) one 1-labeled node is not recognizable by a deterministic Muller tree automaton (see also PS13.2), but its complement is recognizable.

Questions 9.3 and 9.4.1 in today's warm-up questions were a little tricky. Here are the solutions:

WQ9.3:

First, interpret x as a second-order variable. Then, replace each x in by the first-order variable y. Finally, apply the last rule.
Note that, as many of you pointed out, the rule that replaces t=S(x) with S(t)∈x is not sound.

WQ9.4.1 (the formula on the top left)
The two languages are not the same.
For WS1S: L() is the set of all sequences over {∅,{Z}}.
For S1S: L(ψ)=L() - {∅^ω}
 

Have a great weekend,
the Automata, Games, and Verification Team

The 6th of December is on its way

and we wish you a blessed St. Nicholas Day.

And if he thinks you all behaved well,

six little stories he may have to tell.

Just try to find some in front of your door,

or in our case the AGV materials store.

 

Wishing you a happy and blessed St. Nicholas Day,

the Automata, Games, and Verification Team

Regarding today's warm-up questions, if you were wondering about an example for a non-counting language that is not Büchi-recognizable (Question 6), here is one: L = { α∈(ab*)^ω | α=ab^n₀ab^n₁... such that for all i there is a j>i such that n_j>n_i }.

Have a great weekend,
the Automata, Games, and Verification Team

 

Dear Students,

we determined the dates and times for the exams at the end of the semester as follows:

EndTerm: 19.02.2019, 14:00-16:00 (E1 3, HS 002)

Re-Exam: 26.03.2019, 14:00-16:00 (E1 3, HS 002)

Both exams will be open book, meaning you can bring any written or printed material to the exam you want. In case you have any issues with one of the given slotes above, please let us know as soon as possible.

Kind Regards,

the Automata, Games, and Verification Team

Dear Students,

next week on Thursday, November 1st, there won't be a Tutorial/Office Hour due to the public holiday "Allerheiligen". The tutorial instead will be held on Friday, November 2nd, from 11:00-13:00 in seminar room 1.06, building E1 1.

Kind Regards,

The Automata, Games, and Verification Team

Dear Students,

we opened a new submission in rCMS, which you can use to submit your solution to the current problem set, if you prefer to submit solutions in a purly digital fashion. Electronic submissions are accepted either as PDF or TXT. There is, however, no requirement to use this form of submission. You still can submit all your solutions in printed or handwritten form at the beginning of the next lecture. For the upcomming problem sets we will also open similar submissions in the future.

Kind Regards,

the Automata, Games, and Verification Team

Dear Students,

we finished your overall assigments to the discussion slots on Friday. Fortunately, we had ben able to respect all your chosen preferences regarding times and groups.

You can find your assigned discussion session slot on your personal page in rcms. Everybody who requested to be in the same group should have been assigned the same "Tutorial" number. Note that your group will be identified by this number from now on. If there had been any choices that cause problems for you or your group, please contact us as soon as possible.

We then will meet at the discussion sessions on Friday. They are placed in the office rooms of the Reactive Systems chair in E1 1, first floor. The exact room will be determined by an information sheet that will appear at the entrance to the chair on Friday morning.

Until then, we wish eveybody a lot of fun with the warm-up questions.

We see each other on Friday,

the Automata, Games, and Verification Team

We recommend you to participate in the discussion sessions in groups of at most three people. To this end at least one member of the group needs to submit a text file containing the names of all members of the group. Furthermore, also make sure, that all members of the group have a nonempty intersection with respect to their chosen discussion slot preferences.

There is a open submission to upload the group member list.