Course: Advanced Automata Theory

Summer 2017

Introduction

We shall study automata on finite/infinite words and trees and their relationship to logic and computer-aided verification of systems.

Computer science or math students with background in logic and theory of computation. (Familiarity with basic algorithms, logic, and theory of computation will be assumed). Talk to the instructor if you are not sure if you have the background. We shall try to keep the class self-contained, please attend the initial lecture for background material.

Further, I expect you (1) have "mathematical maturity" (e.g., you should be comfortable with proofs and abstract reasoning); (2) are interested in the material; and (3) are willing to spend time outside of class in order to better understand the material presented in lectures.

Grading will be based on a written, open-notes, final exam. Open notes means that you are free to bring your notes to the exam. However, you may not use internet access on any device during an exam.

In order to appear for the exam, you have to turn in homework problems (to be assigned approximately biweekly), write up lecture notes for two lectures, and present a result to the class.

The following text books cover most of the material (and much more):

  1. Michael Sipser, Introduction to the theory of computation, MIT Press

  2. Javier Esparza, Automata Theory Lecture Notes

  3. Erich Graedel, Wolfgang Thomas, Thomas Wilke, Automata, Logics, and Infinite Games, Springer

  4. Jeffrey Shallit, A Second Course in Formal Languages and Automata Theory, Cambridge University Press

In addition, we shall provide lecture notes, surveys, or research papers for topics not covered in these books.

Homework exercises will be handed out approximately every two weeks (weekday TBA). Your answers must be handed in until the day specified in the homework, at the beginning of the lecture.

Students may collaborate on homework assignments, but each student needs to individually write up a solution set and be prepared to present it in class on the due date. The work you submit in this course must be the result of your individual effort. You may discuss homework problems and general proof strategies or algorithms with other students in the course, but you must not collaborate in the detailed development or actual writing of problem sets. This implies that one student should never have in his or her possession a copy of all or part of another student's homework. It is your responsibility to protect your work from unauthorized access. In writing up your homework you are allowed to use any book, paper, or published material. However, you are not allowed to ask others for specific solutions, either in person or by using electronic forums such as newsgroups. Of course, during the administration of exams any form of cooperation or help is forbidden. Academic dishonesty has no place in a university; it wastes our time and yours, and it is unfair to the majority of students. Any dishonest behavior will be severely penalized and may lead to failure in the course.

Announcements

Lecture Notes

We hope to collaboratively create Wiki-like lecture notes at https://sandstorm.init.mpg.de/shared/fE1Q2Y28_shn-nE9vet1m_xlHI2hUKjdbzlSrYEpX9c

You can find a LaTeX tutorial online, which explains basics and first steps of writing LaTeX documents. Please also consult l2tabu, which is a list of do's and don't for writing LaTeX documents. The comprehensive LaTeX symbol list and the detexify website are useful, too (please contact me prior to importing or changing fonts to make particular symbol work).

Schedule

This schedule is preliminary and subject to change.

#

Date

Course topic / lecture

Homework

Additional Materials (lecture notes/papers)

L1

April 18

Introduction to the course. Review of finite automata. Basic constructions.

http://www.jflap.org/

L2

April 19

Further constructions on finite automata. Regular expressions.

HW1

Reading: Sipser

L3

April 25

Review of complexity classes, decision problems on automata

L4

April 26

(Weak) monadic second order logics on words (WS1S). Buchi-Elgot theorem.

Reading: MukundNotes Advanced Reading: Graedel-Thomas-Wilke Ch 12

L5

May 02

Automata minimization: Homomorphisms.

HW2

Partition refinement algorithm / Marking algorithm

L6

May 03

Myhill-Nerode theorem.

L7

May 09

Minimization of DFAs.

L8

May 10

Bisimulation. Reduction of NFAs.

L9

May 16

Learning from examples. Passive learning.

HW3

RPNI Algorithm

L10

May 17

Angluin's Algorithm (L*). libalf.

Angluin's Algorithm

L11

May 23

Omega automata: Buchi, co-Buchi, Rabin, Streett.

Reading: BuchiAutomata

L12

May 24

Conversions between automata. Deterministic and non-deterministic automata.

L13

May 30

Omega-regular languages: properties

HW4

L14

May 31

Combinatorial results: Konig's lemma, Ramsey's theorem

L15

June 06

Complementation using Ramsey's theorem

L16

June 07

Towards determinization: marked subset construction

L17

June 13

Safra's construction

HW5 (updated 26/6/17,4pm)

L18

June 14

Linear temporal logic. Automata-theoretic model checking.

L19

June 20

Linear temporal logic.

L20

June 21

Church's problem. Fundamental definitions of infinite games.

Reading: Automata, Logics, and Infinite Games

L21

June 27

Safety and reachability games.

HW6

attractor_computation.pdf

L22

June 28

Büchi games.

L23

July 04

Parity games.

L24

July 05

Strategy automata and game reductions.

L25

July 11

Muller games.

LAR_example.pdf

L26

July 12

Nondeterminacy of infinite games.

L27

July 18

Recap of the course.

List of topic covered in the course

L28

July 19

Recent results in automata theory.