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
Schedule
| week |
date |
topics |
slides |
exercises |
solutions |
|---|
| 01 |
06.10 & 10.10 |
deterministic finite automata, closure properties |
pdf (1x1, 4x1) |
pdf |
pdf |
| 02 |
13.10 |
non-determinism, epsilon transitions |
pdf (1x1, 4x1) |
pdf |
pdf |
| 03 |
20.10 & 24.10 |
regular expressions, homomorphisms |
pdf (1x1, 4x1) |
|
|
| 04 |
27.10 & 31.10 |
minimization, weak monadic second-order logic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 05 |
03.11 & 07.11 |
weak monadic second-order logic, Myhill-Nerode relations |
pdf (1x1, 4x1) |
pdf |
pdf |
| 06 |
10.11 & 14.11 |
weak monadic second-order logic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 07 |
17.11 & 21.11 |
Presburger arithmetic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 08 |
24.11 & 28.11 |
Büchi automata |
pdf (1x1, 4x1) |
pdf |
pdf |
| 09 |
01.12 & 05.12 |
Büchi automata, complementation, monadic second-order logic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 10 |
08.12 & 12.12 |
|
|
pdf |
pdf |
| 11 |
15.12 & 09.01 |
generalized Büchi automata, linear-time temporal logic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 12 |
12.01 & 16.01 |
LTL model checking |
pdf (1x1, 4x1) |
pdf |
pdf |
| 13 |
19.01 & 23.01 |
alternating (Büchi) automata, LTL model checking |
pdf (1x1, 4x1) |
pdf |
pdf |
| 14 |
26.01 & 30.01 |
exam practice |
pdf (1x1, 4x1) |
pdf |
pdf |
|
02.02 |
1st exam
(solution) |
|
|
|
|
26.02 |
2nd exam |
|
|
|
Literature
Slides and solutions to selected exercises will be made available online.
Accompanying literature will be provided.