|
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]
|