Automata, Games, and Verification Bernd Finkbeiner

News

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

 

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: TBA
  Re-Exam: TBA
 
 

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