Automata, Games, and Verification Bernd Finkbeiner, Hadar Frenkel

News

01.12.2022

Updates on Problem Set 5

Hi all,

As some of you already noticed, the 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... Read more

Hi all,

As some of you already noticed, the 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