Logic, Automata and Games (August

Logic, Automata and Games (August - November 2016)

References

Notes for the course automata and reactive systems by Prof. Wolfgang Thomas at RWTH Aachen university.
Linear-Time Temporal Logic and Büchi Automata
Finite-state Automata on Infinite Inputs
Automata, Logics and Infinite Games, edited by Erich Grädel, Wolfgang Thomas and Thomas Wilke, 2002, Springer.

Outline

Reactive systems and infnite words, automata on infinite words.
Linear temporal logic, satisfiability and model checking.
Advanced topics in automata on infinite words - acceptance modes, determinization, complementation.
Monadic Second Order logic on infinite words.
Games: reachability, Büchi and parity games.
Automata and Monadic Second Order logic on infinite trees.

Exercises

Lectures

Date	Topics Covered	References
2^nd August	Infinite strings on finite alphabets, Büchi automata, deterministic vs. non-deterministic automata.	[1], sections 1.1-1.2.
4^th August	Deterministic Büchi automata are less powerful than non-deterministic ones. Basic constructions and characterizations.	[1], sections 1.3-1.4.
9^th August	Intersection of Büchi automata, generalized Büchi automata. Introduction to Linear Temporal Logic (LTL).	[1], sections 1.5-1.6, 2.3. [2], section 1.
11^th August	Designing a Büchi automaton that accepts the set of all models of a given LTL formula.	[2], section 3.1.
16^th August	Proof of correctness of the reduction from LTL to Büchi automata.	[2], section 3.1.
18^th August	LTL Model checking, polynomial space upper bound. Büchi automata are more powerful than LTL.	Section 3.1 of [2], section 2.5 of [1].
23^rd August	Introduction to Muller, Rabin and Streett acceptance modes. Simulating one with another.	Section 1.3 of [3].
25^th August	Translation from Streett automata to non-deterministic Büchi automata. Translation from deterministic Muller automata to deterministic Rabin automata.	Section 1.3 of [3] and section 1.4.2 of [4].
30^th August	Translation from non-deterministic Büchi automata to deterministic Rabin automata.	Section 1.4 of [3].
1^st September	Safra's construction.	Section 1.4 of [3].
6^th September	Correctness of Safra's construction.	Section 1.4 of [3].
8^th September	Monadic second order logic over infinite strings (S1S), defining Büchi recognizable languages in S1S.	Section 2.6 of [1].
15^th September	Recognizing S1S definable languages using Büchi automata.	Section 3.4 of [1].
27^th September	Translation from S1S to Büchi automata. Introduction to infinite tree automata.	Section 3.4 and 5.1 of [1].
29^th September	Non-deterministic Büchi tree automata less powerful than Muller tree automata. Parity tree automata, closure under finite union and projection.	Sections 5.1 and 5.2 of [1].
4^th October	Introduction to games, how they are useful for complementation of tree automata.	Sections 8.4, 2.1-2.4 of [4], sections 5.3 and 4.1 of [1].
6^th October	Introduction to finite memory and memoryless strategies. From Muller games to parity games.	Section 2.4 of [4].
12^th October	Memoryless determinacy of reachability and 1 games. Attractor and trapping strategies.	Section 2.5 of [4].
13^th October	Memoryless determinacy of Büchi games.	Section 2.5 of [4].
18^th October	Properties of traps and attractors.	Section 6.2 of [4].
20^th October	Paradises and their properties.	Sections 6.2 and 6.3 of [4].
25^th October	Memoryless determinacy of parity games.	Section 6.3 of [4].
27^th October	Relation between memoryless determinacy of parity games and complementing parity tree automata.	Section 8.4 of [4].
1^st November	Parity tree automata are closed under complementation.	Section 8.4 of [4].
3^rd November	Non-emptiness of parity tree automata is decidable.	Section 8.5 of [4].