M.Tech.(CS) Year II
ISI Kolkata, 2021-2022 Session

Semester: First
Instructors: Ansuman Banerjee and Sujata Ghosh
Meeting Times : Tuesdays and Thursdays: 6:00 - 7:45 pm
First Class: Thursday, October 7, 2021
Location: Online


[Teaching staff | Course overview | References | Grading | Lecture schedule | Homeworks/Handouts]



Teaching staff

Instructors

Ansuman Banerjee
Email: ansuman AT isical DOT ac DOT in
Office Hours: By Arrangement (please send an e-mail)
Office: ACMU, 5th Floor, Platinum Jubilee Academic (PJA) Building

Sujata Ghosh
Email: sujata AT isichennai DOT res DOT in
Office Hours: By Arrangement (please send an e-mail)
Office: Working from Home (Chennai)


Course overview


Course Description: As the name suggests, this course revolves around some advanced topics in logic and automata theory. One focus will be on exploring the logic-automata connection. Algebraic semantics will also form an integral part of the course. Towards the end we will introduce you to some recent methods on formal verification. The complete syllabus of the course can be found here.

Pre-requisites: Automata Theory, Languages and Computation; Discrete Mathematics; Logic for Computer Science


Go to top



References


Background: The following books are good resources.

  • - An introductory textbook on logic for computer science. Michael Huth and Mark Ryan (2004). Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press.

  • - An introductory textbook on automata theory. Michael Sipser (2013). Introduction to the Theory of Computation (Third Edition), CENGAGE Learning.

  • - A comprehensive book on model checking. Christel Baier and Joost-Pieter Katoen (2008). Principles of Model Checking, The MIT Press.

  • - A comprehensive book on dynamic logics. David Harel, Dexter Kozen and Jerzy Tiuryn (2000). Dynamic Logic, The MIT Press.

  • - An advanced textbook on modal logic. Patrick Blackburn, Maarten de Rijke and Yde Venema (2001). Modal Logic, Cambridge University Press.

  • - A book on modal logic aimed at researchers. Patrick Blackburn, Johan van Benthem and Frank Wolter, editors (2007). Handbook of Modal Logic, Elsevier.



Reading materials: A list of some general papers, surveys and textbooks covering topics we will discuss during the semester. This list will be updated regularly throughout the semester.

Algebraic Semantics

  • - An SEP entry. Algebraic Propositional Logic.

  • - A textbook on algebraic logic. Josep Maria Font (2016). Abstract Algebraic Logic, College Publications.

  • - A book on universal algebra. Stanley Burris and H. P. Sankappanavar (1981). A Course in Universal Algebra, Springer (Millenium edition can be found online).

  • - An article on the connections between algebra, category theory and computer science: M. Gehrke (2016). Duality in Computer Science, Invited talk at LICS 2016.

More on Automata Theory

  • - A lecture note on topics in automata theory. Wolfgang Thomas (2003). Automata and Reactive Systems.

  • - An article on automata over infinite words. Madhavan Mukund (2012). Finite-state Automata on Infinite Inputs, In Modern Applications of Automata Theory, World Scientific.

  • - A survey on automata over infinite words. Berndt Farwer (2002). ω-Automata, In LNCS 2500, Springer.

  • - Lecture slides of P. Dasgupta (IIT KGP), R. Iosif (UGA), J.P. Katoen (RWTH Aachen), and B. Srivathsan (CMI). They have been used in the class as well.

Modal mu-calculus

  • - A book chapter on topics in modal mu-calculus. Julian Bradfield and Igor Walukiewicz (2018). The mu-calculus and model checking, In Handbook of Model Checking, Springer.

  • - An book chapter on modal mu-calculus. Julian Bradfield and Colin Stirling (2007). Modal mu-calculi, In Handbook of Modal Logic, Springer.



Go to top



Grading


Grades are based on mid-semester examination (20%), home assignments (10%), project (20%) and end-semester examination (50%). The home assignments would include those problems which are given in the course of teaching and those sets of problems which will be uploaded here at regular intervals, and algorithmic questions. The projects would be decided along the way depending upon the interests, and the deadline for submission will be one week after the end-semester examination.

Any test would be closed-book; no notes are permitted.


Go to top



Lecture schedule

07.10.2021 An historical introduction to the topic (R. Ramanujam) (Class slides)
21.10.2021 Logic and algebra: A joint perspective (Class notes)
26.10.2021 Algebraizing classical propositional logic (Class notes)
28.10.2021 Algebraizing classical propositional logic (contd.) (Class notes)
29.10.2021 Algebraizing basic modal logic (Class notes)
02.11.2021 Finite automata on finite words: A recap (Class slides)
05.11.2021 Finite automata on infinite words (Class slides)
09.11.2021 Büchi Automata (Class slides)
11.11.2021 Büchi Automata and ω-regular languages (Class slides)
16.11.2021 Model checking (Class slides)
18.11.2021 Model checking (contd.) (Class slides)
23.11.2021 Linear temporal logic (Class slides)
25.11.2021 Automata-based LTL model-checking (Class slides)
07.12.2021 Dynamic and temporal logics (Class notes)
09.12.2021 Modal mu-calculus: An introduction (Class notes)
10.12.2021 Algebraic semantics (Class notes)
14.12.2021 On syntax (Class notes)
16.12.2021 Game-theoretic semantics: Basic modal logic (Class notes)
17.12.2021 Game-theoretic semantics: Modal mu-calculus (Class notes)
21.12.2021 Game-theoretic semantics: Modal mu-calculus (contd.) (Class notes)
23.12.2021 Relating algebraic and game-theoretic semantics (Class notes)
28.12.2021 CTL, CTL*: Model-checking (Class slides)
01.01.2022 PSPACE-completeness of LTL model-checking (Class slides)
04.01.2022 Timed automata (Class slides)
06.01.2022 Hybrid automata (Class slides)
10.01.2022 Automata on infinite words: Selected topics (Class slides)
11.01.2022 Finite tree automata (Kamal Lodaya) (Class slides)
13.01.2022 Infinite tree automata (Kamal Lodaya) (Class slides)


Go to top



Homeworks/Assignments


On Logic

  • Homework 1
    Deadline for submission: November 16, 2021.


On Automata


Go to top