Automata, Games, and Verification Bernd Finkbeiner, Hadar Frenkel

News

15.03.2023

Re-exam on March 28

Dear all, below are the details for the re-exam on March 28:

  • The re-exam will take place on Tuesday, March 28, at 2:15 pm in HS002 (building E1 3). Please try to arrive a few minutes early.
  • You must register via LSF at least a week before the exam. Please... Read more

Dear all, below are the details for the re-exam on March 28:

  • The re-exam will take place on Tuesday, March 28, at 2:15 pm in HS002 (building E1 3). Please try to arrive a few minutes early.
  • You must register via LSF at least a week before the exam. Please let us know immediately if you cannot register for some reason.  
  • The re-exam will have a similar structure and guidelines as the first exam. That is: You will have 120 minutes to complete the exam; The exam is open book and you are allowed to use any written or printed material. 
  • The content of all lectures and all problem sets is relevant to the exam. Material in the lecture notes that we will not have had time to cover during the lectures is not required for the exam.
  • Please bring your student ID and a black or blue non-erasable pen.

Good luck! 

15.02.2023

Exam results

Dear All, The results of the main exam are now available on your personal status page. The exam inspection will take place on Thursday, February 23, 9-11 am in building E1.1, room 1.06. Please bring your student ID. Have a great semester break!

10.02.2023

Extra office hour on Monday

Thanks, everyone, for a great final round of discussion sessions! Here are a few points that came up today:

  1. Extra office hour on Monday: There will be an additional office hour on Monday, Feb 13, 9-11 am. 
  2. The exam on Tuesday: The exam will consist of four... Read more

Thanks, everyone, for a great final round of discussion sessions! Here are a few points that came up today:

  1. Extra office hour on Monday: There will be an additional office hour on Monday, Feb 13, 9-11 am. 
  2. The exam on Tuesday: The exam will consist of four problems; the first problem consists of several true/false questions in the style of our warm-up questions; the other three problems will be in the style of the exercises on the problem sets. 
  3. The co-Büchi condition: Several people noticed that we never formally defined the co-Büchi condition, which is the dual of the Büchi condition. The co-Büchi condition requires that a certain set of states only occurs finitely often. Formally, co-Büchi(F)= {α∈Qω | Inf(α) ∩ F = ∅}.

If any further questions come up, don’t hesitate to send us eMail or to stop by during the extra office hour on Monday. We wish you lots of success in the exam! See you on Tuesday!

07.02.2023

Final discussion sessions on Friday

Dear All, the warm-up questions for Friday are online; there is no problem set this week. See you on Friday for a final round of discussion sessions!

01.02.2023

Exam on February 14

Dear all, here are a few details regarding the exam on February 14. Please don't hesitate to let us know if you have further questions.

  • The exam will take place on Tuesday, February 14, at 2:15 pm in HS002 (building E1 3). Please try to arrive a few minutes... Read more

Dear all, here are a few details regarding the exam on February 14. Please don't hesitate to let us know if you have further questions.

  • The exam will take place on Tuesday, February 14, at 2:15 pm in HS002 (building E1 3). Please try to arrive a few minutes early.
  • You must be registered via LSF at least a week before the exam. Please let us know immediately if you cannot register for some reason.  
  • You will have 120 minutes to complete the exam.
  • The exam is open book, i.e., you are allowed to use any written or printed material.
  • The content of all lectures and all problem sets is relevant for the exam. Material in the lecture notes that we will not have had time to cover during the lectures is not required for the exam (but this is still great stuff, and you are highly encouraged to read the entire lecture notes).
  • Please bring your student ID and a black or blue non-erasable pen.

31.01.2023

No lecture today

Dear All, In a really unfortunate twist, both Hadar and I fell sick this morning. Since neither of us can give the lecture today, we, unfortunately, have to cancel today's lecture. There will also be no discussion sessions this week. The office hour on Thursday will... Read more

Dear All, In a really unfortunate twist, both Hadar and I fell sick this morning. Since neither of us can give the lecture today, we, unfortunately, have to cancel today's lecture. There will also be no discussion sessions this week. The office hour on Thursday will be online only. Next week, everything should be back to normal. We are also planning to have a final discussion session on February 10. 

We suggest you use the extra time this week to review the course materials in preparation for our exam on February 14 and to let us know about any questions that come up. We're happy to answer your questions by email; if there are topics of common interest, we'll also pick them up in the lecture next week. Again, our apologies for cancelling today -- see you soon, stay healthy!

24.01.2023

Course Evaluation, Problem Set 11

Dear All, Warm-up Questions & Problem Set 11 are now online. If you have not yet had a chance to fill out the course evaluation, please be sure to visit the link to the qualis website, which is available in the Materials section: we are excited to hear whether you... Read more

Dear All, Warm-up Questions & Problem Set 11 are now online. If you have not yet had a chance to fill out the course evaluation, please be sure to visit the link to the qualis website, which is available in the Materials section: we are excited to hear whether you liked the course! Thanks a lot for your time and effort, your comments are highly appreciated. See you on Friday!

17.01.2023

Warm-up Questions and Problem Set 10 are online

See you on Friday!

10.01.2023

Warm-up Questions and Problem Set 9

Dear All, The New Year is off to a great start with fresh new Warm-up Questions & Problem Set #9! Note that on Friday, everything is back to normal, i.e., we'll meet in-person or online corresponding to the original type of your discussion session. See you... Read more

Dear All, The New Year is off to a great start with fresh new Warm-up Questions & Problem Set #9! Note that on Friday, everything is back to normal, i.e., we'll meet in-person or online corresponding to the original type of your discussion session. See you then! 

22.12.2022

Zoom recording of Lecture 8

Dear All, We have uploaded the zoom recording of Lecture 8. We wish you Happy Holidays!

20.12.2022

Happy Holidays!

Dear All, The next set of warm-up questions and Problem Set 8 are online. There will be no discussion sessions this week, the next course meeting are the online discussion sessions on January 6. We wish you Happy Holidays and a great start into the New Year 2023!... Read more

Dear All, The next set of warm-up questions and Problem Set 8 are online. There will be no discussion sessions this week, the next course meeting are the online discussion sessions on January 6. We wish you Happy Holidays and a great start into the New Year 2023! See you in January!

16.12.2022

LTL operator precedence rules

Dear All, During the discussion session today, we discovered that the precedence order on the LTL operators defined in the lecture notes does not match what you may know from popular textbooks like Baier/Katoen. We decided to change the precedence rules in the... Read more

Dear All, During the discussion session today, we discovered that the precedence order on the LTL operators defined in the lecture notes does not match what you may know from popular textbooks like Baier/Katoen. We decided to change the precedence rules in the lecture notes so that unary operators bind stronger than binary operators, Until takes precedence over conjunction, and negation and Next bind equally strongly. Sorry for the confusion! Note that this change affects the interpretation of the formulas in Warm-up Question 4 from the current set of questions. The updated lecture notes are available under Materials, together with a list of all changes we made since the beginning of the course. Thanks for the discussions today, have a great weekend!

13.12.2022

Problem Set 7, online course meetings during the weeks before and after the break

Dear All, Warm-up Questions and Problem Set 7 are ready for your enjoyment! Also, please note that we will only have online meetings during the week before and after the break. At today's lecture, we discussed the following schedule for the next few weeks. See you... Read more

Dear All, Warm-up Questions and Problem Set 7 are ready for your enjoyment! Also, please note that we will only have online meetings during the week before and after the break. At today's lecture, we discussed the following schedule for the next few weeks. See you on Friday!

Fri, Dec 16 discussion sessions online and in-person, as usual
Tue, Dec 20 lecture online only (at the usual zoom link)
Fri, Dec 23 no discussion sessions
Dec 26 - 30 break
Tue, Jan 3 no lecture
Fri, Jan 6 all discussion slots online (at the zoom link of the lecture)
Tue, Jan 10 back to normal: lecture in-person and online
07.12.2022

Warm-up Questions and Problem Set 6

... are ready. See you Friday!

01.12.2022

Updates on Problem Set 5

Hi all, As some of you already noticed, Exercise 1.b in Problem Set 5 generates a big automaton. To make it a little less overwhelming, I slightly updated the exercise! Even though the difference is almost invisible (can you find it ? :)) it should make a big... Read more

Hi all, As some of you already noticed, Exercise 1.b in Problem Set 5 generates a big automaton. To make it a little less overwhelming, I slightly updated the exercise! Even though the difference is almost invisible (can you find it ? :)) it should make a big difference in the number of states! Enjoy!

30.11.2022

Warm-up Questions and Problem Set 5

... are available now. Enjoy! 

22.11.2022

Warm-up Questions and Problem Set 4

... are online! Have fun, and see you on Friday!

15.11.2022

Third problem set and warm-up questions

The third problem set and the warm-up questions for Friday are available for download. This week's in-person discussion sessions will be in rooms 1.11 and 1.14 (building E1 1), online sessions at the usual zoom link. As usual, please let us know in case you cannot... Read more

The third problem set and the warm-up questions for Friday are available for download. This week's in-person discussion sessions will be in rooms 1.11 and 1.14 (building E1 1), online sessions at the usual zoom link. As usual, please let us know in case you cannot make it. See you on Friday! 

15.11.2022

AG&V exam dates: February 14 and March 28

Dear All, please note that the dates of the AG&V exam and re-exam have been set to February 14, 2023 (2-5 pm) and March 28, 2023 (2-5 pm). In case you cannot participate on those dates, please let us know. 

09.11.2022

Second problem set and warm-up questions

The second problem set and the warm-up questions for Friday are available for download. The in-person discussion sessions this week will be in room 1.11 (building E1 1), online sessions at the usual zoom link. As usual, please let us know in case you cannot make... Read more

The second problem set and the warm-up questions for Friday are available for download. The in-person discussion sessions this week will be in room 1.11 (building E1 1), online sessions at the usual zoom link. As usual, please let us know in case you cannot make it. See you on Friday!  

08.11.2022

Problems with zoom today

Dear All, Our lecture hall seems to have network problems today; this may affect the zoom meeting of the lecture. We'll try to make it work, but, to be safe, we'll record the lecture and make the recording available later today. Thanks for your patience!

02.11.2022

Discussion sessions start this Friday

Dear All, You should now see your assigned discussion session on your personal status page. Please check and let us know if your assignment is missing or if the time slot does not work for you. We start this Friday (Nov 4th). In-person sessions will meet this week... Read more

Dear All, You should now see your assigned discussion session on your personal status page. Please check and let us know if your assignment is missing or if the time slot does not work for you. We start this Friday (Nov 4th). In-person sessions will meet this week in building E1 1, room 1.14; to join an online session, please use the standard zoom link from the lecture (Information/Zoom Meeting). Please answer the warm-up questions before the session and bring your answers with you. See you on Friday!

25.10.2022

Please book your discussion session!

Dear All, Thanks for a great first course meeting today! The first set of warm-up questions and the first problem set are now available in the "Materials" section. Also, please book the time slot for your discussion session at ... Read more

Dear All, Thanks for a great first course meeting today! The first set of warm-up questions and the first problem set are now available in the "Materials" section. Also, please book the time slot for your discussion session at terminplaner6.dfn.de/b/0763239517732f0714f54c6493283ccc-48879. Please make your choice by the end of the week (31.10.2022, 00:00). 

If none of the offered time slots work for you, or if you run into any other problems, let us know. (If you previously entered your preferences on your personal status page, please make your choice again via the DFN link. Unfortunately, there was a glitch in the system, which did not show you all options.)  

The first discussion sessions will take place on Nov 4. The first office hour is already on Oct 27. Because of the holiday next week, the next lecture will be on Nov 8. See you soon!
 

24.10.2022

Welcome!

Welcome to Automata, Games, and Verification! The first course meeting is on Tuesday, Oct 25, 2022, at 2:15 pm. You can participate in-person (E1.3/HS003) or remotely (zoom link under "Information" while logged in). See you then!

Show all
 

Automata, Games, and Verification

Lectures: Tuesdays, 14:15-16:00 in building E1.3, room HS003, starting on 25/10/22 
Discussion sessions: Fridays, in building E1.1, rooms 1.11 and 1.14, starting on 04/11/22
Office hours: Thursdays, 9:00-11:00 in building E1.1, room 1.06, starting on 27/10/22
Both in-person and online participation via Zoom is possible. 
 

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

Organization

  • Every Tuesday, we publish a new problem set and new set of "warm-up" (multiple-choice) questions.
  • Every Friday, there are 5-10min discussion sessions. 
  • We will arrange individual discussion sessions for groups of at most three people. Both in-person and online options will be available.
  • 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 issues 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
  • Office hours are every Thursday from 9:00-11:00 in seminar room E1 1, R 1.06 (starting Oct 27). Feel free to come and go whenever you like during these two hours.
  • During the office hours, you can inspect your corrected solutions and ask questions regarding the problem set, your solution, or the lecture.
  • Grade: The grade will be determined only by the grade of the exam. Participation in the weekly discussion sessions is a requirement for admission to the exam. 
  • Exams: The dates of the exam and the re-exam are February 14, 2023 (2-5 pm) and March 28, 2023 (2-5 pm).

 



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