Content
The course covers automata theory and its connection to logic.
The following topics will be discussed:
-
(deterministic, non-deterministic, alternating) finite automata
-
regular expressions
-
(weak) monadic second-order logic
-
Presburger arithmetic
-
(alternating) Büchi automata
-
linear-time temporal logic
-
tree automata
Schedule
| week |
date |
topics |
slides |
exercises |
solutions |
|---|
| 1 |
03.10 & 07.10 |
deterministic finite automata, closure properties |
pdf (1x1, 4x1) |
pdf |
pdf |
| 2 |
10.10 |
non-determinism, epsilon transitions |
pdf (1x1, 4x1) |
pdf |
pdf |
| 3 |
17.10 & 21.10 |
regular expressions, homomorphisms |
pdf (1x1, 4x1) |
pdf |
pdf |
| 4 |
24.10 & 28.10 |
minimization, weak monadic second-order logic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 5 |
31.10 & 04.11 |
weak monadic second-order logic, Myhill-Nerode relations |
pdf (1x1, 4x1) |
pdf |
pdf |
| 6 |
07.11 & 11.11 |
weak monadic second-order logic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 7 |
14.11 & 18.11 |
Presburger arithmetic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 8 |
21.11 & 25.11 |
Büchi automata |
pdf (1x1, 4x1) |
pdf |
pdf |
| 9 |
28.11 & 02.12 |
Büchi automata, complementation, monadic second-order logic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 10 |
05.12 & 09.12 |
acceptance conditions, linear-time temporal logic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 11 |
12.12 & 16.12 |
LTL model checking |
pdf (1x1, 4x1) |
pdf |
pdf |
| 12 |
09.01 & 13.01 |
alternating (Büchi) automata, LTL model checking |
pdf (1x1, 4x1) |
pdf |
pdf |
| 13 |
16.01 & 20.01 |
tree automata |
pdf (1x1, 4x1) |
pdf |
pdf |
| 14 |
23.01 & 27.01 |
tree automata, weak monadic second-order logic |
pdf (1x1, 4x1) |
pdf |
|
| 15 |
30.01 |
1st exam |
|
|
|
Literature
Slides and solutions to selected exercises will be made available online.
Accompanying literature will be provided.