Automata, Games, and Verification Bernd Finkbeiner

News

08.04.2019

Results: End-of-semester Exam

Dear Students,

the results of the end-of-semester exam are now available in the RCMS. The exam inspection will take place on Friday, 12th of April from 10am to 11am in E1.1 R 1.06.

Kind Regards,

the Automata, Games, and Verification Team

21.02.2019

Time slot shift for the re-exam

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

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

20.02.2019

Results: End-of-term Exam

Dear Students,

the results of the end-of-term exam are now available in the RCMS. The exam inspection will take place on Friday, 8th of March from 10am to 11am in E1.1 R 1.06.

Kind Regards,

the Automata, Games, and Verification Team

01.02.2019

WQ14.2

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

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.

18.12.2018

Bugfix in PS 9.2

Dear Students,

There was a bug on Problem Set 9, Exercise 2 in the semantics definition of t1 < t2. The bug now has been fixed in the current online version.

Kind Regards,

the Automata, Games, and Verification Team

14.12.2018

Solutions for WQ9.3/WQ9.4

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 \varphi by the first-order variable y. Finally, apply the last rule.
Note that, as many... Read more

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 \varphi 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(\varphi ) is the set of all sequences over {∅,{Z}}.
For S1S: L(ψ)=L(\varphi ) - {∅ω}
 

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

06.12.2018

St. Nicholas Day

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

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

30.11.2018

Example for WQ6.6

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*)ω | α=abn0abn1... such that for all i there is a j>i such that nj>ni }.

Have a great... Read more

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*)ω | α=abn0abn1... such that for all i there is a j>i such that nj>ni }.

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

 

22.11.2018

Exam Dates

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

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

26.10.2018

Public Holiday on November 1st

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

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

22.10.2018

Electronic Submission of Problem Set Solutions

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

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

17.10.2018

Group and Discussion Session Assignments

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

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

16.10.2018

Tell us your team members.

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

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.

16.10.2018

Please select your preferred discussion slots till Wednesday 17th, 12:00

https://doodle.com/poll/n6d8pgkbc56p4bav

Show all
 

Advanced Lecture (Vertiefungsvorlesung), Summer Term 2018, 6 CP

Lecture Room: E1 3, HS 001
Lectures: Tuesdays, 14:15-16:00
Office Hours: Thursday, 09:00-11:00 (E1 1, R 1.06)
Exams: EndTerm: 19.02.2019, 14:00-16:00 (E1 3, HS 002)
  Re-Exam: 26.03.2019, 10:00-12:00 (E1 3, HS 002)
 
 

Profile

The theory of automata over infinite objects provides a succinct, expressive, and formal framework for reasoning about reactive systems, such as communication protocols and control systems. Reactive systems are characterized by their nonterminating behaviour and persistent interaction with their environment. In this course we will study the main ingredients of this elegant theory, and its application to automatic verification (model checking) and program synthesis.

The course is addressed to students interested in the theoretical concepts to analyze reactive systems using automata over infinite words, automata over infinite trees, and two-player games. The course continues on the topics of the core lecture “Verification”, the Verification lecture is not, however, a prerequisite for the AG&V course.

Topics

  • Automata over infinite words and trees (omega-automata)
  • Infinite two-player games
  • Logical systems for the specification of nonterminating behavior
  • Transformation of automata according to logical operations

Regulations

  • Every Tuesday, we give out a new problem set and new warm-up questions during the lecture.
  • Every Friday, there are 5-10min discussion sessions from 9:00 until 11:00. Please mark your preferred slots by Wednesday Oct 17th, 12:00 in this doodle: https://doodle.com/poll/n6d8pgkbc56p4bav
  • We will arrange individual discussion sessions for groups of at most three people. To form such a group, choose the same slot preferences in the doodle as your group members and submit a txt-file with the names of all members of the group via your personal status page (at least once by one of the members).
  • Please bring your solutions to the warm-up questions to the discussion sessions. We will discuss them and any questions you may have about the content of the lectures.
  • Attendance to the 5-10min discussion sessions is mandatory. You are allowed to skip at most two sessions in case you cannot make it once or twice. Otherwise, If you encounter any other issus in attending the slot, please contact us as soon as possible.
  • Problem sets can be submitted at the beginning of the next lecture after the one where they were given out.
  • Submitting problem set solutions is not mandatory. We will return the corrected solutions during the next office hour.
  • During the office hours, you can inspect your corrected solutions and ask questions regarding the problem set, your solution, or the lecture.
  • Office hours are every Thursday from 9:00--11:00 in seminar room E1 1, R 1.06 (starting Oct 25). Feel free to come and go whenever you like during these two hours.

References

The course will be based on the following two textbooks, supplemented as necessary by various research papers.

             

Automata, Logics, and Infinite Games:
A Guide to Current Research

Erich Grädel, Wolfgang Thomas,
Thomas Wilke (Eds.)
Springer, 2nd Print (1. November 2005)
LNCS (2500), ISBN 3540003886

Online Version (Access is free of charge if you connect from a department IP. If you encounter any problems, let us know.)
 
             

Automata Theory and its Applications
Bakhadyr Khoussainov, Anil Nerode
Birkhauser Boston
1st edition (February 15, 2001)
ISBN 0817642072


Past Editions

Summer 2015 Winter 2012/2013 Summer 2011 Summer 2008 Winter 2006/2007


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