6937
Comment:
|
67474
|
Deletions are marked like this. | Additions are marked like this. |
Line 6: | Line 6: |
. [[http://www.mpi-sws.org/~rupak/|Rupak Majumdar]] ( rupak@mpi-sws.org ) Room 414, Building 26 (MPI-SWS) | . [[http://www.mpi-sws.org/~rupak/|Dr. Rupak Majumdar]] ( rupak@mpi-sws.org ) Room 414, Building 26 (MPI-SWS) |
Line 8: | Line 8: |
. [[http://www.mpi-sws.org/~neider/|Daniel Neider]] ( neider@mpi-sws.org ) Room 315, Building 26 (MPI-SWS) | . [[http://www.mpi-sws.org/~neider/|Dr. Daniel Neider]] ( neider@mpi-sws.org ) Room 315, Building 26 (MPI-SWS) |
Line 10: | Line 10: |
* '''Teaching assistants''': | * '''Tutorials''': |
Line 21: | Line 21: |
* '''Class website''': https://wiki.mpi-sws.org/wiki/Courses/AdvancedAutomataTheory |
|
Line 45: | Line 47: |
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 |
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 |
Line 61: | Line 61: |
* 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 |
|
Line 64: | Line 69: |
||# ||<style="font-weight:bold; text-align:center">Date ||<style="font-weight:bold;text-align:center">Course topic / lecture ||<style="font-weight:bold; ">Homework ||<style="font-weight:bold;">Additional Materials (lecture notes/papers) || || ||L1 ||<style="text-align:center">April 18 || Introduction to the course. Review of finite automata. Basic constructions. || || || || ||L2 ||<style="text-align:center">April 19 || Constructions on finite automata. || || || || ||L3 ||<style="text-align:center">April 25 || Automata minimization: Myhill-Nerode theorem, non-determinism. || || || || ||L4 ||<style="text-align:center">April 26 || Automata learning: Passive learning, L*. || || || || ||L5 ||<style="text-align:center">May 02 || Antichains and implementations. || || || || ||L6 ||<style="text-align:center">May 03 || Alternating automata. || || || || ||L7 ||<style="text-align:center">May 09 || Applications. Open problems. || || || || ||L8 ||<style="text-align:center">May 10 || (Weak) monadic second order logics on words (WS1S). Buchi-Elgot theorem. || || || || ||L9 ||<style="text-align:center">May 16 || Omega automata: Buchi, co-Buchi, Rabin, Streett. || || || || ||L10 ||<style="text-align:center">May 17 || Conversions between automata. Deterministic and non-deterministic automata. || || || || ||L11 ||<style="text-align:center">May 23 || MSO (S1S) and Buchi's theorem. || || || || ||L12 ||<style="text-align:center">May 24 || Determinization of automata. || || || || ||L13 ||<style="text-align:center">May 30 || Determinization of automata. || || || || ||L14 ||<style="text-align:center">May 31 || Alternating automata. || || || || ||L15 ||<style="text-align:center">June 06 || Linear temporal logic. Automata-theoretic odel checking. || || || || ||L16 ||<style="text-align:center">June 07 || Overflow: Applications, tools, open problems. || || || || ||L17 ||<style="text-align:center">June 13 || Church's problem. Realizability. Games and synthesis. || || || || ||L18 ||<style="text-align:center">June 14 || Safety, reachability, Buchi, parity games. || || || || ||L19 ||<style="text-align:center">June 20 || Parity games: algorithms. || || || || ||L20 ||<style="text-align:center">June 21 || Tree automata and decidability of S2S || || || || ||L21 ||<style="text-align:center">July 04 || Tree automata and decidability of S2S || || || || ||L22 ||<style="text-align:center">July 05 || Beyond regularity: nested word automata. || || || || ||L23 ||<style="text-align:center">July 11 || Context free languages. Parikh's theorem. || || || || ||L24 ||<style="text-align:center">July 12 || TBD. || || || || ||L25 ||<style="text-align:center">July 18 || TBD. || || || || ||L26 ||<style="text-align:center">July 19 || TBD. || || || || |
||# ||<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;font-weight:bold;text-align:center& 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;font-weight:bold;text-align:center& 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;font-weight:bold; & 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;font-weight:bold; & 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;text-align:center& 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;text-align:center& 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;text-align:center& 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;text-align:center& 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;text-align:center& 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;text-align:center& 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;text-align:center& 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. || || || || ||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;text-align:center& 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*. || || || || ||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;text-align:center& 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;text-align:center& 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;text-align:center& 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;text-align:center& 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;text-align:center& 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;text-align:center& 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;text-align:center& 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;text-align:center& 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;text-align:center& 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;text-align:center& 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;text-align:center& 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;text-align:center& 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;text-align:center& 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;text-align:center& 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;text-align:center& 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;text-align:center& 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;text-align:center& 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;text-align:center& 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. || || || || |
Course: Advanced Automata Theory
Summer 2017
Instructor:
Dr. Rupak Majumdar ( rupak@mpi-sws.org ) Room 414, Building 26 (MPI-SWS)
Dr. Daniel Neider ( neider@mpi-sws.org ) Room 315, Building 26 (MPI-SWS)
Tutorials:
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
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):
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. |
|
|
|
L2 |
April 19 |
Further constructions on finite automata. Regular expressions. |
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. |
|
||
L6 |
May 03 |
Myhill-Nerode theorem, non-determinism. |
|
|
|
L7 |
May 09 |
Learning from examples. Passive learning. |
|
|
|
L8 |
May 10 |
L*. |
|
|
|
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. |
|
|
|