Logic, Automata and Games

Aug - Nov 2014




Hours

Lectures Mon   15:30 - 16:45 Lecture Hall 2
Fri   15:30 - 16:45 Lecture Hall 2


Grading

Mid-semester exam 50%
End-semester exam 50%


References

[1]   Automata on reactive systems by Prof. Wolfgang Thomas.

[2]   Finite state automata on infinite inputs by Prof. Madhavan Mukund.

[3]   Lecture notes by Prof. Narayan Kumar

[4]   Automata, logics and infinite games: a guide to current research by E. Grädel, W. Thomas, T. Wilke, LNCS 2500 Springer


Lectures



Lecture 1 05.08.2014 (Tue) Büchi automata, Characterizing non-deterministic and deterministic Büchi recognizable languages 1.1 - 1.4 of [1]
Lecture 2 07.08.2014 (Thu) Closure properties, Exercises 1.5 - 1.7 of [1]
Lecture 3,4 18.08.2014 (Mon) LTL, Conversion to NBA 2.3 - 2.5 of [1]
Lecture 5 22.08.2014 (Fri) LTL is exponentially succinct than NBA, less expressive than NBA; Model checking, Complexity 2.1, 2.2, 2.5 of [1]
Lecture 6 25.08.2014 (Mon) Ramsey-based complementation of Büchi automata Section 2 of Lecture 7 in [3]
Lecture 7 01.09.2014 (Mon) Muller and Rabin conditions 1.3 of [2]
Lecture 8 05.09.2014 (Fri) Determinizing Büchi automata: Problems with subset construction, Marked subset and Hierarchical Marked subset constructions 1.4 of [2]
Lecture 9 08.09.2014 (Mon) Safra's construction 1.4 of [2]
Lecture 10 12.09.2014 (Fri) Correctness of Safra's construction, Logic S1S 1.4, 1.2 of [2]
Lecture 11 15.09.2014 (Mon) S1S equivalent to Omega-regular languages 1.2 of [2]
26.09.2014 (Fri) Mid-Semester Exam
Lecture 12 29.09.2014 (Mon) Optimality of Safra's construction; Streett acceptance Section 3.3 of [1]; Page 19-20 of [2]
Lecture 13 10.10.2014 (Fri) DMA to DRA (LAR construction); Rabin chain and Parity conditions Section 1.4.2 of [4]; Section 3 in Lecture 12 of [3]
Lecture 14 13.10.2014 (Mon) Games, fundamental questions, reducing Muller games to Parity games Sections 2.1 to 2.4.3 of [4]
Lecture 15 17.10.2014 (Fri) Strategy automata for finite memory strategies; lifting strategies from vertices to sets of vertices Sections 2.4.4 of [4]
Lecture 16,17 24.10.2014 (Fri) Memoryless determinacy for Reachability, Büchi and Parity games Sections 3, 4 in Lecture 9 of [3]; Section 4.7 in [1]
Lecture 18 27.10.2014 (Mon) Algorithms for reachability, Büchi and Parity games; Complexity of solving parity games; Optimality of LAR construction Relevant slides of Barbara Jobstmann for algorithms, Section 4.9 of [1] and Section 4.2 of Paper for LAR-optimality
Lecture 19 31.10.2014 (Fri) Introduction to automata over infinite trees; Büchi tree automata less expressive than rest Section 5.1, 5.2 of [1]
Lecture 20 3.11.2014 (Mon) Complementation of tree automata Section 8.4 of [4]; Section 5.3 of [1]
Lecture 21 10.11.2014 (Mon) Emptiness problem for tree automata, S2S Section 5.4, 5.5 of [1]
Lecture 22 14.11.2014 (Fri) Decidability of S2S, SnS and SωS Section 5.5 of [1], Pages 222-223 of [4]