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.



Schedule

Date Descr Topics covered Resources/materials
6/1/2020 Lecture 1

ω-words, ω-languages

Büchi automata, deterministic Büchi automata, examples..

  •  deterministic BA are strictly less powerful. 

References: Sections 1.1, 1.2, 1.3 of [1]

7/1/2020 Lecture 2
  •  If U  ⊆ Σ is a regular language and  L  ⊆ Σω is Buchi recognizable, then U.L is Büchi recognizable.
  • If U  ⊆ Σ  is a regular language then Uω is  Büchi recognizable.
  • If U  ⊆ Σ  is a regular language then Lim(U) is  Büchi recognizable. In fact it is deterministic Buchi recognizable. 
  • Non-deterministic BA recognizable languages are closed under union and intersection.
  • Deterministic BA recognizable languages are closed under union and intersection.
  • Generalized Buchi acceptance condition, and conversion to normal Buchi acceptance.
  • Characterization: BA recongnizable languages = ω-regular languages (finite union of U.Vω)
  • ω-regular expressions.
  • Non-emptiness checking algorithm.
  • Every ω-regular language contains an ultimately periodic word

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
  • Towards complementing non-deterministic Buchi automata ... Given an NBA A recognizing an ω-regular language L
    • two finite words are equivalent if they have identical flow matrices. The flow matrix of a word w represents, for every pair of states (p,q) of A, whether there is a w-labelled path from p to q visiting a final state, whether there is a w-labelled path p to q (but none visiting final state), or whether there is no path from p to q on w..
    • finitely many equivalence classes
    • For every u, [u] is regular.
    • For every u, v, [u][v]ω is either contained in L or disjoint from L.

References: [4]

14/1/2020 Lecture 4
  • ... complementing non-deterministic Buchi automata ... Given an NBA A recognizing an ω-regular language L
    • For every u, v, [u][v]ω is either contained in L or disjoint from L.
    • Every ω-word belongs to some [u][v]ω.
    • closure under complementation follows from the above and closure properties established in Lecture 1.
  • omega regular languages are finite union of (U_i)(Lim V_i)
  • proof to be continued...

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
  • omega regular languages are finite union of (U_i)(Lim V_i)
  • omega regular languages are Boolean combinations of (Lim V_i)

References: [4], [9]

21/1/2020 Lecture 6
  • Rabin acceptance condition.
  • closure under union, preserves determinism
  • omega regular languages are recognized by deterministic Rabin automata
  • Muller acceptance condition
  • translation from Rabin to Muller, preserving determinism
  • omega regular languages are recognized by deterministic Muller automata (McNaughton's theorem)

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.