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 |
03.10 & 07.10 |
deterministic finite automata, closure properties |
|
|
|
| 02 |
10.10 |
non-determinism, epsilon transitions |
|
|
|
| 03 |
17.10 & 21.10 |
regular expressions, homomorphisms |
|
|
|
| 04 |
24.10 & 28.10 |
minimization, weak monadic second-order logic |
|
|
|
| 05 |
31.10 & 04.11 |
weak monadic second-order logic, Myhill-Nerode relations |
|
|
|
| 06 |
07.11 & 11.11 |
weak monadic second-order logic |
|
|
|
| 07 |
14.11 & 18.11 |
Presburger arithmetic |
|
|
|
| 08 |
21.11 & 25.11 |
Büchi automata |
|
|
|
| 09 |
28.11 & 02.12 |
Büchi automata, complementation, monadic second-order logic |
|
|
|
| 10 |
05.12 & 09.12 |
acceptance conditions, linear-time temporal logic |
|
|
|
| 11 |
12.12 & 16.12 |
LTL model checking |
|
|
|
| 12 |
09.01 & 13.01 |
alternating (Büchi) automata, LTL model checking |
|
|
|
| 13 |
16.01 & 20.01 |
tree automata |
|
|
|
| 14 |
23.01 & 27.01 |
tree automata, weak monadic second-order logic |
|
|
|
|
30.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.