Differences between revisions 2 and 45 (spanning 43 versions)
Revision 2 as of 2017-04-17 11:35:22
Size: 10098
Editor: rupak
Comment:
Revision 45 as of 2017-05-08 12:26:34
Size: 90461
Editor: neider
Comment:
Deletions are marked like this. Additions are marked like this.
Line 2: Line 2:
Line 4: Line 3:
Line 8: Line 6:
  [[http://www.mpi-sws.org/~rupak/|Rupak Majumdar]] ([[mailto:rupak@mpi-sws.org|rupak@mpi-sws.org]])<<BR>>
 
Room 414, Building 26 (MPI-SWS)
  [[http://www.mpi-sws.org/~neider/|Daniel Neider]] ([[mailto:neider@mpi-sws.org|neider@mpi-sws.org]])<<BR>>
 
Room 315, Building 26 (MPI-SWS)
 * '''Teaching assistants''':
  [[http://www.mpi-sws.org/~burcu/|Dr. Burcu Ozkan]] ([[mailto:burcu@mpi-sws.org|burcu@mpi-sws.org]])<<BR>>
 
[[http://www.mpi-sws.org/~akschmuck/|Dr. Anne-Kathrin Schmuck]] ([[mailto:akschmuck@mpi-sws.org|akschmuck@mpi-sws.org]])<<BR>>
  . [[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 315, 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 )
Line 16: Line 16:
  Tuesdays 08:15-09:45 48-210 and Wednesdays 13:45-15:15 46-280<<BR>>
 * '''Tutorial''': Tuesday 10:00-11:30<<BR>>
  . Tuesdays 08:15-09:45 48-210 and Wednesdays 13:45-15:15 46-280

 * '''Tutorial''': Tuesday 10:00-11:30
Line 19: Line 21:

 * '''Class website''': https://wiki.mpi-sws.org/wiki/Courses/AdvancedAutomataTheory
Line 21: Line 26:
== Introduction ==
 * '''Syllabus and contents.'''
Line 22: Line 29:
== Introduction == We shall study automata on finite/infinite words and trees and their relationship to logic and computer-aided verification of systems.
Line 24: Line 31:
  * '''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.'''
Line 28: Line 33:
  * '''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.
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.
Line 35: Line 35:
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.
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 b. '''Erich Graedel, Wolfgang Thomas, Thomas Wilke''', '' [[https://link.springer.com/book/10.1007/3-540-36387-4|Automata, Logics, and Infinite Games]]'', Springer c. '''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.

== Announcements ==
 * The first lecture is on April 18, 2017.
 * The '''written final exam''' will be held on '''July 28, 2017''' morning. (Exact time TBD.)
 * Homeworks are due in class!

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

== Schedule ==
This schedule is preliminary and subject to change.
||# ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;font-weight:bold;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">Date ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;font-weight:bold;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">Course topic / lecture ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;font-weight:bold; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">Homework ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;font-weight:bold; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">Additional Materials (lecture notes/papers) || ||
||L1 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">April 18 ||Introduction to the course. Review of finite automata. Basic constructions. || ||http://www.jflap.org/ || ||
||L2 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">April 19 ||Further constructions on finite automata. Regular expressions. ||[[attachment:hw1.pdf|HW1]] ||Reading: Sipser || ||
||L3 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">April 25 ||Review of complexity classes, decision problems on automata || || || ||
||L4 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">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 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">May 02 ||Automata minimization: Homomorphisms. ||[[attachment:hw2.pdf|HW2]] ||[[attachment:lecture05_slides.pdf]] || ||
||L6 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">May 03 ||Myhill-Nerode theorem, non-determinism. || || || ||
||L7 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">May 09 ||Learning from examples. Passive learning. || ||[[attachment:RPNI Algorithm]] || ||
||L8 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">May 10 ||L*. || ||[[attachment:Angluin's Algorithm]] || ||
||L9 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">May 16 ||Applications of finite automata and learning. libalf. || || || ||
||L10 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">May 17 ||Spill slot. || || || ||
|| || || || || || ||
||L11 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">May 23 ||Omega automata: Buchi, co-Buchi, Rabin, Streett. || || || ||
||L12 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">May 24 ||Conversions between automata. Deterministic and non-deterministic automata. || || || ||
||L13 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">May 30 ||MSO (S1S) and Buchi's theorem. || || || ||
||L14 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">May 31 ||Determinization of automata. || || || ||
||L15 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">June 06 ||Determinization of automata. || || || ||
||L16 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">June 07 ||Alternating omega-automata: Miyano and Hayashi's construction. || || || ||
||L17 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">June 13 ||Linear temporal logic. Automata-theoretic model checking. || || || ||
||L18 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">June 14 ||Overflow: Applications, tools, open problems. || || || ||
|| || || || || || ||
||L19 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">June 20 ||Church's problem. Realizability. Games and synthesis. || || || ||
||L20 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">June 21 ||Safety, reachability, Buchi, parity games. || || || ||
||L21 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">July 04 ||Parity games and mu-calculus. || || || ||
||L22 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">July 05 ||Bounded synthesis. || || || ||
||L23 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">July 11 ||Tree automata and decidability of S2S || || || ||
||L24 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">July 12 ||Beyond regularity: nested word automata. || || || ||
|| || || || || || ||
||L25 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">July 18 ||Context free languages. Parikh's theorem. || || || ||
||L26 ||<style="&quot; &amp; quot; &amp; amp; quot; &amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot;text-align:center&amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; amp; quot; &amp; amp; amp; amp; quot; &amp; amp; amp; quot; &amp; amp; quot; &amp; quot; &quot;">July 19 ||Timed automata. || || || ||
Line 40: Line 102:

  * '''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.
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.

 * '''Textbook''':
  Class notes and research papers will be handed out.

The text book
Michael Sipser, Introduction to the theory of computation,
contains the material we will cover in the first few weeks as well as the required background for the class.



 * '''Teamwork''':
  Students may collaborate on homeworks, but each student needs to individually write up a solution set and be prepared to present it in class on the due date.
 * '''Logistics of Homework:'''
  Homework exercises will be handed out every two weeks (weekday TBA). Your answers must be handed in until the day specified in the homework, at the end of the lecture. Answers can be handed in personally to any of the teaching assistants.

== Exam ==

 * The first exam will take place on July 28th, at 9:00am, in rooms 56-206 and 56-207.
 * The exam is an open-book exam: You may bring any notes and literature that you like.

== Schedule ==

||<: 2% rowbgcolor="#B7AFA3" style="font-weight: bold;"> # ||<: 4% style="font-weight: bold;"> Date ||<: 30% style="font-weight: bold;"> Course topic / lecture ||<20% style="font-weight: bold;"> Homework ||<35% style="font-weight: bold;"> Materials ||<9% style="font-weight: bold;"> Video ||
||<: rowbgcolor="#F5FAFA"> L1 ||<:> April 23 ||<:> Introduction to formal verification || || [[attachment:Lecture1.ppt|Lecture slides]]<<BR>>[[attachment:demillo.pdf|De Millo, Lipton, and Perlis. Social processes and proofs of programs.]] || ||
||<: rowbgcolor="#C1DAD6"> - ||<:> April 25 || || || || ||
||<: rowbgcolor="#F5FAFA"> L2 ||<:> April 28 ||<:> Preliminaries: graph algorithms, automata theory || [[attachment:hw1.pdf|Homework 1.]] Need not be turned in. || [[attachment:Lecture2.pdf|Lecture notes]] || ||
||<: rowbgcolor="#F5FAFA"> L3 ||<:> April 30 ||<:> Preliminaries: propositional logic || || [[attachment:Lecture3.pdf|Lecture notes]]<<BR>>[[http://ipsc.ksp.sk/2013/real/problems/l.html|Problem L (Labyrinth).]] [[https://github.com/fniksic/labyrinth|Solution]].<<BR>>[[http://try.ocamlpro.com|Try OCaml]], [[http://ocaml.org/learn/|Learn OCaml]], [[https://realworldocaml.org|Real World OCaml]] || ||
||<: rowbgcolor="#C1DAD6"> T1 ||<:> May 2 ||<:> Solutions to Homework 1. || || || ||
||<: rowbgcolor="#F5FAFA"> L4 ||<:> May 5 ||<:> The invariant verification problem. Enumerative invariant verification. Depth first search. Spin. || || Notes from an unpublished text book by Rajeev Alur and Tom Henzinger: <<BR>> [[attachment:CavBook-1.pdf|The Reactive modules modeling language.]]<<BR>>[[attachment:CavBook-2.pdf|Invariant verification.]]<<BR>>[[http://spinroot.com/|SPIN]] web page. || ||
||<: rowbgcolor="#F5FAFA"> L5 ||<:> May 7 ||<:> Peterson's protocol. Heuristics for enumerative invariant verification. Symbolic invariant verification. Symbolic reachability. || || [[attachment:CavBook-3.pdf|Alur and Henzinger. Symbolic graph representation.]] || [[http://www.mpi-sws.org/seminars/vrs/2014-05-07_vrs.mpg|MPG (660 MB)]] ||
||<: rowbgcolor="#C1DAD6"> T2 ||<:> May 9 ||<:> Q & A || || || ||
||<: rowbgcolor="#F5FAFA"> L6 ||<:> May 12 ||<:> Symbolic model checking with SAT || || [[attachment:Sharad Malik MOD Chapter.pdf|Malik and Weissenbacher. Boolean satisfiability solvers: Techniques and extensions.]]<<BR>>[[attachment:NieOT-JACM-06.pdf|Nieuwenhuis, Oliveras, and Tinelli. Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T).]] || [[http://www.mpi-sws.org/seminars/vrs/2014-05-12_vrs.mpg|MPG (678 MB)]] ||
||<: rowbgcolor="#F5FAFA"> L7 ||<:> May 14 ||<:> Implementing a SAT Solver. BDDs. || [[attachment:hw2.pdf|Homework 2.]] Due May 28, 2014. || || [[http://www.mpi-sws.org/seminars/vrs/2014-05-14_vrs.mp4|MP4 (529 MB)]] ||
||<: rowbgcolor="#C1DAD6"> T3 ||<:> May 16 ||<:> Q & A || || || ||
||<: rowbgcolor="#F5FAFA"> L8 ||<:> May 19 ||<:> BDDs. || || [[attachment:ieeetc86.pdf|Bryant. Graph-based algorithms for Boolean function manipulation. (The BDD paper.)]] || [[http://www.mpi-sws.org/seminars/vrs/2014-05-19_vrs.mp4|MP4 (434 MB)]] ||
||<: rowbgcolor="#F5FAFA"> L9 ||<:> May 21 ||<:> SMT. Timed automata and difference constraints. || || [[attachment:Projects.pdf|Project suggestions.]]<<BR>>[[attachment:Timed Automata.pdf|Alur, Parthasarathy. Decision problems for timed automata: A survey.]] || ||
||<: rowbgcolor="#C1DAD6"> T4 ||<:> May 23 ||<:> Q & A || || || [[http://www.mpi-sws.org/seminars/vrs/2014-05-23_vrs.mp4|MP4 (313 MB)]] ||
||<: rowbgcolor="#F5FAFA"> L10 ||<:> May 26 ||<:> Symbolic execution. || || [[attachment:cacm13.pdf|Cadar, Sen. Symbolic execution for software testing: Three decades later.]] || ||
||<: rowbgcolor="#F5FAFA"> L11 ||<:> May 28 ||<:> Inductive invariants. Abstraction. || || || ||
||<: rowbgcolor="#C1DAD6"> T5 ||<:> May 30 ||<:> Solutions to Homework 2. || || || ||
||<: rowbgcolor="#F5FAFA"> L12 ||<:> June 2 ||<:> Predicate abstraction and CEGAR. || || [[attachment:SoftwareModelChecking.pdf|Survey on software model checking.]] || ||
||<: rowbgcolor="#F5FAFA"> L13 ||<:> June 4 ||<:> IC3. || [[attachment:hw3.pdf|Homework 3.]] Due June 18, 2014. || [[attachment:ic3_bradley.pdf|Bradley. SAT-based model checking without unrolling. (The IC3 paper.)]]<<BR>>[[attachment:ic3_tut.pdf|Somenzi, Bradley. IC3: Where monolithic and incremental meet. (The IC3 tutorial.)]] || ||
||<: rowbgcolor="#C1DAD6"> T6 ||<:> June 6 ||<:> Q & A || || || ||
||<: rowbgcolor="#F5FAFA"> - ||<:> June 9 ||<:>Holiday (No lecture) || || || ||
||<: rowbgcolor="#F5FAFA"> L14 ||<:> June 11 ||<:> Interpolation-based model checking || || [[attachment:McMillan-Interpolation.pdf|McMillan. Interpolation and SAT-based model checking.]] || ||
||<: rowbgcolor="#C1DAD6"> T7 ||<:> June 13 ||<:> Discussing projects || || || ||
||<: rowbgcolor="#F5FAFA"> L15 ||<:> June 16 ||<:> Simulation and Bisimulation || || [[attachment:partition.pdf|Partition refinement]] || ||
||<: rowbgcolor="#F5FAFA"> L16 ||<:> June 18 ||<:> Simulation and Bisimulation || || || ||
||<: rowbgcolor="#C1DAD6"> T8 ||<:> June 20 ||<:> Solutions to Homework 3. || || || ||
||<: rowbgcolor="#F5FAFA"> L17 ||<:> June 23 ||<:> Well-structured Transition Systems || || [[attachment:marktoberdorf-notes.pdf|Majumdar. Marktoberdorf 2013 lecture notes.]] || ||
||<: rowbgcolor="#F5FAFA"> - ||<:> June 25 ||<:> Cancelled. || || || ||
||<: rowbgcolor="#C1DAD6"> T9 ||<:> June 27 ||<:> Q & A || || || ||
||<: rowbgcolor="#F5FAFA"> L18 ||<:> June 30 ||<:> Example: Concurrent programs || || || ||
||<: rowbgcolor="#F5FAFA"> L19 ||<:> July 2 ||<:> Safe Temporal Logic (STL) || [[attachment:hw4.pdf|Homework 4.]] Due July 9/July 16, 2014. || [[attachment:stl.pdf|Notes on STL]] || ||
||<: rowbgcolor="#C1DAD6"> T10 ||<:> July 4 ||<:> Q & A || || || ||
||<: rowbgcolor="#F5FAFA"> L20 ||<:> July 7 ||<:> Model checking STL || || || ||
||<: rowbgcolor="#F5FAFA"> L21 ||<:> July 9 ||<:> Safety vs liveness || [[attachment:Endterm.pdf|Practice exam]] || [[attachment:safetyvsliveness.pdf|Safety and liveness]] (We did not cover all the material) || ||
||<: rowbgcolor="#C1DAD6"> - ||<:> July 11 ||<:> Cancelled || || || ||
||<: rowbgcolor="#F5FAFA"> L22 ||<:> July 14 ||<:> CTL || || [[attachment:CTL.pdf|CTL]] (For reading about linear time logics and automata: [[attachment:automata.pdf|Automata-theoretic verification]] || ||
||<: rowbgcolor="#F5FAFA"> L23 ||<:> July 16 ||<:> Model checking CTL || [[attachment:exam-solutions.pdf|Solutions to the Practice Exam]] || || ||
||<: rowbgcolor="#C1DAD6"> T11 ||<:> July 18 ||<:> Solutions to Homework 4. '''Moved to 10:00 am!''' || || || ||
||<: rowbgcolor="#F5FAFA"> - ||<:> July 21 ||<:> No lecture (preperation time for project presentations) || || || ||
||<: rowbgcolor="#F5FAFA"> L24 ||<:> July 23 ||<:> Project presentations || || || ||
||<: rowbgcolor="#C1DAD6"> T12 ||<:> July 25 ||<:> Preparation for exam || [[attachment:hw5.pdf|Homework 5.]] (No due date) || || ||

Course: Advanced Automata Theory

Summer 2017

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):

  1. Michael Sipser, Introduction to the theory of computation, MIT Press b. Erich Graedel, Wolfgang Thomas, Thomas Wilke, Automata, Logics, and Infinite Games, Springer c. 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.

Announcements

  • The first lecture is on April 18, 2017.
  • The written final exam will be held on July 28, 2017 morning. (Exact time TBD.)

  • Homeworks are due in class!

Lecture Notes

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

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

lecture05_slides.pdf

L6

May 03

Myhill-Nerode theorem, non-determinism.

L7

May 09

Learning from examples. Passive learning.

RPNI Algorithm

L8

May 10

L*.

Angluin's Algorithm

L9

May 16

Applications of finite automata and learning. libalf.

L10

May 17

Spill slot.

L11

May 23

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

L12

May 24

Conversions between automata. Deterministic and non-deterministic automata.

L13

May 30

MSO (S1S) and Buchi's theorem.

L14

May 31

Determinization of automata.

L15

June 06

Determinization of automata.

L16

June 07

Alternating omega-automata: Miyano and Hayashi's construction.

L17

June 13

Linear temporal logic. Automata-theoretic model checking.

L18

June 14

Overflow: Applications, tools, open problems.

L19

June 20

Church's problem. Realizability. Games and synthesis.

L20

June 21

Safety, reachability, Buchi, parity games.

L21

July 04

Parity games and mu-calculus.

L22

July 05

Bounded synthesis.

L23

July 11

Tree automata and decidability of S2S

L24

July 12

Beyond regularity: nested word automata.

L25

July 18

Context free languages. Parikh's theorem.

L26

July 19

Timed automata.

Courses/AdvancedAutomataTheory-SS2017 (last edited 2018-03-29 06:38:49 by neider)