Mid-sem exam: Friday (22 Feb) 17:00, LH 803

Topics: Finite state automata for infinite words, temporal logics, games of infinite duration

Prerequisite: A pass in ToC

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
4/1/2019	Lecture 1	ω-words, ω-languages Büchi automata, deterministic Büchi automata, examples.. deterministic BA are strictly less powerful. 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. closure properties (to be continued)	References: Sections 1.1, 1.2, 1.3 of [1]
7/1/2019	Lecture 2	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. Non-deterministic BA recognizable languages are closed under projection. Characterization: BA recongnizable languages = ω-regular languages (finite union of U.V^ω) ω-regular expressions. Non-emptiness checking algorithm.	References: Chapter 1 of [1]
9/1/2019	Lecture 3	Every ω-regular language contains an ultimately periodic word Towards complementing non-deterministic Buchi automata ... 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), 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, v, [u][v]^ω is either contained in L or disjoint from L.	References: [4]
11/1/2019	Lecture 4	complementing non-deterministic Buchi automata ... 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), 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, v, [u][v]^ω is either contained in L or disjoint from L. Every ω-word belongs to some [u][v]^ω. [u][v]^ω forms a partition of Σ^∗ refining L. closure under complementation follows from the above and closure properties established in Lecture 1.	References: [4]
16/1/2019	Lecture 5	complementing non-deterministic Buchi automata ... illustration on an example Monadic second-order logic - syntax	References: [4]
18/1/2019	Lecture 6	Monadic second-order logic - syntax, semantics, examples...
28/1/2019	Lecture 7	EMSO sentence capturing the language of a Buchi automaton Constructing a Buchi automaton corresponding to an MSO formula MSO = EMSO over words
30/1/2019	Lecture 8	Illustration of MSO to Buchi automata Decidability of Presburger arithmetic
6/2/2019	Lecture 9	Linear-time Temporal Logics LTL to Buchi automata	References: [2] Lecture notes by Prof. Madhavan Mukund.
8/2/2019	Lecture 10	Linear-time Temporal Logics LTL to Buchi automata Proof of correctness of the construction Model checking problem. Complexity.	References: [2] Lecture notes by Prof. Madhavan Mukund.
11/2/2019	Lecture 11	Different acceptance conditions and translations between them.. Muller, Rabin, Streett, Parity	References: Section 1.3 of [3] Lecture notes by Prof. Madhavan Mukund.
13/2/2019	Lecture 12	omega regular languages are finite union of (U_i)(Lim V_i)	References: [4]
15/2/2019	Lecture 13	omega regular languages can be recognized by deterministic Rabin automata.	References: [9]