Topics: Finite state automata for infinite words, temporal logics, games of infinite duration
Prerequisite: A pass in ToC
Course slots: Monday 10:30, Tuesday 10:30, LH 801
Instructors: Aiswarya (first half), Praveen (Second half)
Teaching Assistant: Ekanshdeep Gupta
Grading: Each half will contribute 50% to the final grades. For the first half, there will definitely be the mid-sem exams. We may also have a quiz, but this will be decided later.
Course references:
[1] Lecture notes of the course "Automata and Reactive Systems" by Prof. Dr. Wolfgang Thomas.
[2] Lectures notes on Linear-Time Temporal Logic and Büchi Automata by Prof. Madhavan Mukund.
[3] Chapter on Finite-state Automata on Infinite Inputs by Prof. Madhavan Mukund.
[4] Lecture notes on Büchi Automata by Prof. K. Narayan Kumar.
[5] Chapter on Automata over Infinite Objects by Prof. Wolfgang Thomas. In the Handbook of Theoretical Computer Science Vol B
[6] Chapter on Languages, Automata and Logic by Prof. Wolfgang Thomas. In the Handbook of Formal Languages. Vol 3
Additional references:
[7] Chapter on Temporal Logics by Stephane Demri and Paul Gastin
[8] The book Principles of Model Checking by Christel Baier and Joost-Pieter Katoen
[9] Lecture notes
on determinizing BŸchi Automata by Prof. K. Narayan Kumar.
[10] RenŽ Mazala, Infinite Games. In Automata Logics, and Infinite Games , volume 2500 of LNCS.
[11] Ralf KŸsters, Memoryless Determinacy of Parity Games. In Automata Logics, and Infinite Games , volume 2500 of LNCS.
[12] Roderick Bloem,Barbara Jobstmann,Nir Piterman, Amir Pnueli and Yaniv Sa'ar. Synthesis of reactive (1) designs. Journal of Computer and System Sciences, volume 78, issue 3, May 2012, pages 911-938.
[13] Yonit Kesten, Nir Piterman and Amir Pnueli. Bridging the gap between fair simulation and trace inclusion. Information and Computation, volume 200, issue 1, July 2005, pages 35-61.
Date | Descr | Topics covered | Resources/materials |
---|---|---|---|
6/1/2020 | Lecture 1 | ω-words, ω-languages Büchi automata, deterministic Büchi automata, examples..
|
References: Sections 1.1, 1.2, 1.3 of [1] |
7/1/2020 | Lecture 2 |
|
References: Chapter 1 of [1] |
7/1/2020 | Problem set 1 | These problem sets are not graded. However students are strongly encouraged to solve these problems and submit solutions for feedback. Submissions shall be accepted till Thursday, 9th January 2020 for feedback. Feel free to contact the TA in case of any doubts. | Problem Set 1 |
13/1/2020 | Lecture 3 |
|
References: [4] |
14/1/2020 | Lecture 4 |
|
References: [4] |
14/1/2020 | Problem set 2 | These problem sets are not graded. However students are strongly encouraged to solve these problems and submit solutions for feedback. Submissions shall be accepted till Thursday, 16th January 2020 for feedback. Feel free to contact the TA in case of any doubts. | Problem Set 2 |
20/1/2020 | Lecture 5 |
|
References: [4], [9] |
21/1/2020 | Lecture 6 |
|
References:[9], Section 1.3 of [3] |
22/1/2020 | Problem set 3 | These problem sets are not graded. However students are strongly encouraged to solve these problems and submit solutions for feedback. Submissions shall be accepted till Friday, 24th January 2020 for feedback. Feel free to contact the TA in case of any doubts. | Problem Set 3 |
28/1/2020 | Lecture 7 | first-order logic on omega words.. examples | |
3/2/2020 | Lecture 8 | monadic second-order logic on omega words.. examples | |
4/2/2020 | Lecture 9 | monadic second-order logic on omega words.. examples .. succ can be expressed using order and vice-versa. | |
5/2/2020 | Problem set 4 | These problem sets are not graded. However students are strongly encouraged to solve these problems and submit solutions for feedback. Submissions shall be accepted till Friday,7th February for feedback. Feel free to contact the TA in case of any doubts. | Problem Set 4 |
10/2/2020 | Lecture 10 | monadic second-order logic on omega words.. from logic to automata | |
11/2/2020 | Lecture 11 | labeling by propositions vs labeling by letters, decidability of Presburger arithmetic, LTL (X, F, G) | References:[9] |
11/2/2020 | Problem set 5 | These problem sets are not graded. However students are strongly encouraged to solve these problems and submit solutions for feedback. Submissions shall be accepted till Friday,14th February for feedback. Feel free to contact the TA in case of any doubts. | Problem Set 5 |
17/2/2020 | Lecture 12 | LTL (X, F, G, U) - model checking problem. satisfiability problem. from LTL to Automata (to be continued) | References:Lectures notes on Linear-Time Temporal Logic and Büchi Automata by Prof. Madhavan Mukund. |