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 |
|---|
| 01 |
02.10 & 06.10 |
deterministic finite automata, closure properties |
pdf (1x1, 4x1) |
pdf |
pdf |
| 02 |
09.10 |
non-determinism, epsilon transitions |
pdf (1x1, 4x1) |
pdf |
pdf |
| 03 |
16.10 & 20.10 |
regular expressions, homomorphisms |
pdf (1x1, 4x1) |
|
|
| 04 |
23.10 & 27.10 |
minimization, weak monadic second-order logic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 05 |
30.10 & 03.11 |
weak monadic second-order logic, Myhill-Nerode relations |
pdf (1x1, 4x1) |
pdf |
pdf |
| 06 |
06.11 & 10.11 |
weak monadic second-order logic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 07 |
13.11 & 17.11 |
Presburger arithmetic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 08 |
20.11 & 24.11 |
Büchi automata |
pdf (1x1, 4x1) |
pdf |
pdf |
| 09 |
27.11 & 01.12 |
Büchi automata, complementation, monadic second-order logic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 10 |
04.12 |
generalized Büchi automata, linear-time temporal logic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 11 |
11.12 & 15.12 |
LTL model checking |
pdf (1x1, 4x1) |
|
|
| 12 |
08.01 & 12.01 |
alternating (Büchi) automata, LTL model checking |
pdf (1x1, 4x1) |
pdf |
pdf |
| 13 |
15.01 & 19.01 |
tree automata |
pdf (1x1, 4x1) |
pdf |
pdf |
| 14 |
22.01 & 26.01 |
tree automata, weak monadic second-order logic |
pdf (1x1, 4x1) |
pdf |
pdf |
|
29.01 |
1st exam
(solution) |
|
|
|
|
23.02 |
2nd exam
(solution) |
|
|
|
Literature
Slides and solutions to selected exercises will be made available online.
Accompanying literature will be provided.