E0 222 Automata Theory and Computability

Teaching Assistants: P Habeeb and Nabarun Deka.

Meeting schedule:

• 10am on Tue, Thu.
• Google Meet link for the course.
• First class at 10am on Thu 5th August 2021.

• Course Outline
  • Automata and Logic: Buchi's logical characterization of regular languages; Automata-based decision procedures for logics of natural numbers with order (N,<); logic of natural numbers with + (N,+) (Presburger logic); Undecidability of (N,+,x); Algebraic approach to regular languages, the syntactic monoid and relation to the Myhill-Nerode theorem.
  • Pushdown Systems: Parikh's theorem on semi-linearity of CFL's; Reachability in pushdown systems, saturation algorithm for Pre* and Post*; Deterministic PDA's and complementation; Visibly Pushdown Automata; Decidability results for PDA's and subclasses like Counter Automata.
  • Automata on infinite words: Closure properties of omega-regular languages, including closure under complementation; Deterministic Buchi automata; Revisiting Buchi's logical characterization.
  • Automata on Trees: Closure properties, decision procedures, congruences and minimization.

• Lectures
  • 05-08-2021: Course overview. [Recording].
  • 10-08-2021, 12-08-2021: Recap on Finite State Automata. [Recording 10-08-2021], [Recording 12-08-2021].
  • 17-08-2021: Quiz on finite-state automata.
  • 19-08-2021, 24-08-2021, 26-08-2021, 31-08-2021: Buchi's logical characterization of regular languages. [Recording 19-08-2021]. [Recording 24-08-2021.] [Recording 26-08-2021.] [Recording 31-08-2021.]
  • 02-09-2021, 07-09-2021: Automata-based Decision Procedure for Presburger Logic. [Recording 02-09-2021]. [Recording 07-09-2021].
  • 09-09-2021, 14-09-2021: Myhill-Nerode Theorem. [Recording 09-09-2021]. [Recording 14-09-2021].
  • 16-09-2021, 21-09-2021: Algebraic approach to automata by Kamal Lodaya. [Recording 16-09-2021]. [Recording 21-09-2021].
  • 23-09-2021: Tree Automata by Kamal Lodaya. [Recording 23-09-2021].
  • 30-09-2021: Intro to Context-Free Grammars. [Recording].
  • 05-10-2021: Chomsky Normal Form [Recording 04-10-2021].
  • 07-10-2021: Pumping Lemma and ultimate periodicity for regular languages. [Recording].
  • 12-10-2021: Pumping Lemma for CFGs. [Recording].
  • 14-10-2021: Parikh's Theorem. [Recording].
  • 21-10-2021: Intro to PDAs. [Recording].
  • 26-10-2021: Equivalence of PDAs and CFGs. [Recording].
  • 28-10-2021, 29-10-2021: Pushdown Reachability. [Recording 28-10-2021] [Recording].
  • 02-10-2021: Complementing DPDAs. [Recording].
  • 09-11-2021: Visibly Pushdown Languages. [Recording].
  • 11-11-2021: Intro to Turing Machines. [Recording].
  • 16-11-2021: Equivalent models. [Recording].
  • 18-11-2021: Halting Problem [Recording].
  • 19-11-2021: More Undecidable Problems. [Recording].
  • 23-11-2021: Reductions. [Recording].
  • 25-11-2021: Undecidable problems about CFLs. [Recording].
  • 26-11-2021: Godel's Incompleteness Theorem. [Recording].
  • TBA: Decision Procedure for Real Arithmetic (by Kamal Lodaya).

• Books and other material
  1. Dexter Kozen: Automata and Computability. Springer 1999.
  2. Hopcroft J.E. and Ullman J.D.: Introduction to Automata, Languages and Computation. Addison Wesley, 1979.
  3. Melvin Fitting: First-Order Logic and Theorem Proving (See Secs. 5.1, 5.2, and 5.3 for basics of first-order logic).
  4. Wolfgang Thomas: Automata on infinite objects, in Handbook of Theoretical Computer Science, Volume B, Elsevier, 1990.
  5. H. R. Lewis and C. H. Papadimitriou: Elements of the Theory of Computation. Prentice Hall, 1981.
  6. Deepak D'Souza and Priti Shankar (Eds.): Modern Applications of Automata Theory, World Scientific, 2012.
  7. Note on Buchi's MSO characterisation of regular languages.
  8. Wolfgang Thomas: Notes on applied automata theory
  9. Note on regular languages, logic and algebra, by Kamal Lodaya.
  10. Chapter by Comon and Kirschner (see Chapter 2, Section 2.8 on Presburger Logic).
  11. Chapter by Straubing and Weil.
  12. Visibly Pushdown Automata by Alur and Madhusudan.

• Assignments
  • Assignment 1 (MSO and Presburger Logic) due on Fri 10 September 2021.
  • Assignment 2 (Implementing decision procedure for Presburger Logic). Slide on problem. [Recording of discussion on assignment with TAs on 24 Sep 2021.]
  • Assignment 3 due on Mon 04 October 2021.
  • Assignment 4 (Context-Free Grammars) due on Mon 1st November 2021.
  • Assignment 5 (Pushdown Automata) due on Mon 15 November 2021.
  • Assignment 6 due on Mon 06 December 2021.

• Seminar Topics (Link to Schedule Doc)
  • Angluin's algorithm for learning regular languages. Addrija, Dhruv and Mehul, 5th Nov 2021. Slides.
  • Regularity Preserving Relations by Seifras and McNaughton. Saurabh Awinashe and Ankit Kurani 11th Nov 2021. Slides.
  • Buchi Automata. Abhishek, Kawin and Sasanka. Slides.
  • Nested word automata. Harshitha, Jaydeep and Rupashree, 19 Nov 2021.
  • Schutzenberger's aperiodic monoid characterization of star-free languages. Tushar and Umang, 25th Nov. Slides.
  • Primitive Recursive Functions and Computability. Aditya Ravishankar, Moksha Mevada, Ankit Kumar, 26 Nov. Slides.
  • Undecidability of Post's Correspondence Problem. Bodhisattva, Rishav and Sourav, 04 Dec 2021.
  • Concatenation of inputs in a 2-way automaton. Abhilash and Prathamesh, 05 Dec 2021. Slides.
  • Context Sensitive Grammars and Linear Bounded Automata. Rajesh, Mayank, and Himanshu, 06 Dec 2021 Slides.
  • Presburger Logic and Semilinear Sets (Paper by Ginsburg and Spanier, Pacific J. Math, 1966). Chintan, Maitri and Rohit, 07 Dec 2021. Slides.
  • Undecidability of validity problem of First-Order Logic. (see Rob van Glabbeek's notes). Sumanth Prabhu, 13 Dec 2021. Slides.
  • Proof of Shuztenberger-McNaughton-Papert theorem (FO=star-free=counter-free=aperiodic monoid).
  • Direct automaton construction for Parikh's Theorem. Paper by Esparza, Ganty, Kiefer, Luttenberger.

• Weightage for evaluation:
  • Mid-semester Exam: 20%
  • Assignments + Quiz + Seminar: 40%
  • Final Exam: 40%

• Exam Schedule:
  • Mid-semester Exam: 9:30am Tue 28th September 2021.
  • Final Exam: 10am Fri 10th December 2021.