## page was renamed from Courses/AdvancedAutomataTheory #acl rupak,neider,burcu,akschmuck:read,write,delete,revert,admin All:read = Course: Advanced Automata Theory = '''Summer 2017''' * '''Instructor''': . [[http://www.mpi-sws.org/~rupak/|Dr. Rupak Majumdar]] ( rupak@mpi-sws.org ) Room 414, Building 26 (MPI-SWS) . [[http://www.mpi-sws.org/~neider/|Dr. Daniel Neider]] ( neider@mpi-sws.org ) Room 316, Building 26 (MPI-SWS) * '''Tutorials''': . [[http://www.mpi-sws.org/~burcu/|Dr. Burcu Ozkan]] ( burcu@mpi-sws.org ) . [[http://www.mpi-sws.org/~akschmuck/|Dr. Anne-Kathrin Schmuck]] ( akschmuck@mpi-sws.org ) * '''Lectures''': . Tuesdays 08:15-09:45 48-210 and Wednesdays 13:45-15:15 46-280 * '''Tutorial''': Tuesday 10:00-11:30 * '''Office hours''': By appointment * '''Class website''': https://wiki.mpi-sws.org/wiki/Courses/AdvancedAutomataTheory * '''Mailing list''': TBD == Announcements == * The first lecture is on April 18, 2017. * The written final exam will be held on July 28, 2017 in Room 48-208 between 8:30 and 10:30am. You can bring any books or lecture notes you want to the exam. However, you are not allowed to connect to the internet on any device. * Here is a''' [[attachment:practice-final.pdf|practice exam]].''' * The room''' [[http://www.kis.uni-kl.de/campus/all/event.asp?gguid=0x3183BFF7EF31B348ADB7CE0A7D982A27&tguid=0x934C4C0145A8BB458AB4E80C9169EDA9|48-438]] '''is reserved for exam preparation from Monday, July 24, to Thursday, July 28. * A''' [[attachment:topics.pdf|list of all topics]] '''covered in the course is available. * Safra's construction: you should have a broad understanding of Safra's construction, including the underlying ideas, its main steps, and it's complexity. However, we will __not__ ask to construct Safra trees in the exam. * '''The [[attachment:results_exam1.pdf|results of the first exam]] are available. Please spread this information to your fellow students.''' * '''Einsicht will take place in Room 207, Building 26 (MPI-SWS) on Thursday, August 17, at 2pm (moved from 11am). Please contact one of the instructors if this time and date does not work for you.<
>''' * The second written exam will be held on March 29, 2018 in Room 42-110 between 9:00 and 11:00am. You can bring any books or lecture notes you want to the exam. However, you are not allowed to connect to the internet on any device. == Introduction == * '''Syllabus and contents.''' We shall study automata on finite/infinite words and trees and their relationship to logic and computer-aided verification of systems. * '''Intended Audience.''' 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''' 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. * '''Text book''' The following text books cover most of the material (and much more): a. '''Michael Sipser''', ''Introduction to the theory of computation'', MIT Press a. '''Javier Esparza''', [[https://www7.in.tum.de/~esparza/autoskript.pdf|Automata Theory Lecture Notes]] a. '''Erich Graedel, Wolfgang Thomas, Thomas Wilke''', '' [[https://link.springer.com/book/10.1007/3-540-36387-4|Automata, Logics, and Infinite Games]]'', Springer a. '''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:''' 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. * '''Teamwork and Academic Honesty''': 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. == 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 [[https://www.latex-tutorial.com/|LaTeX tutorial]] online, which explains basics and first steps of writing LaTeX documents. Please also consult [[http://mirrors.ctan.org/info/l2tabu/english/l2tabuen.pdf|l2tabu]], which is a list of do's and don't for writing LaTeX documents. The [[http://tug.ctan.org/info/symbols/comprehensive/symbols-a4.pdf|comprehensive LaTeX symbol list]] and the [[http://detexify.kirelabs.org/classify.html|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. ||[[attachment:hw1.pdf|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: [[attachment:MukundNotesAutomataMSO.pdf|MukundNotes]] Advanced Reading: [[GraedelThomasWilke|Graedel-Thomas-Wilke]] Ch 12 || || || || || || || || || ||L5 ||May 02 ||Automata minimization: Homomorphisms. ||[[attachment:hw2.pdf|HW2]] ||[[attachment:lecture05_slides.pdf|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. ||[[attachment:hw3.pdf|HW3]] ||[[attachment:RPNI.pdf|RPNI Algorithm]] || || ||L10 ||May 17 ||Angluin's Algorithm (L*). libalf. || ||[[attachment:Angluin.pdf|Angluin's Algorithm]] || || || || || || || || || ||L11 ||May 23 ||Omega automata: Buchi, co-Buchi, Rabin, Streett. || ||Reading: [[attachment:MukundNotesBuchiAutomata.pdf|BuchiAutomata]] || || ||L12 ||May 24 ||Conversions between automata. Deterministic and non-deterministic automata. || || || || ||L13 ||May 30 ||Omega-regular languages: properties ||[[attachment:hw4.pdf|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 ||[[attachment:hw5.pdf|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:'' [[https://link.springer.com/book/10.1007/3-540-36387-4|Automata, Logics, and Infinite Games]]'' || || ||L21 ||June 27 ||Safety and reachability games. ||[[attachment:hw6.pdf|HW6]] ||[[attachment: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. || ||[[attachment:LAR_example.pdf]] || || ||L26 ||July 12 ||Nondeterminacy of infinite games. || || || || || || || || || || || ||L27 ||July 18 ||Recap of the course. || ||[[attachment:topics.pdf|List of topic covered in the course]] || || ||L28 ||July 19 ||Recent results in automata theory. || || || || ----