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 |
07.10 & 11.10 |
deterministic finite automata, closure properties |
pdf (1x1, 4x1) |
pdf |
pdf |
| 02 |
14.10 |
non-determinism, epsilon transitions |
pdf (1x1, 4x1) |
pdf |
|
| 03 |
21.10 & 25.10 |
regular expressions, homomorphisms |
pdf (1x1, 4x1) |
|
pdf |
| 04 |
28.10 |
minimization, weak monadic second-order logic |
pdf (1x1, 4x1) |
pdf |
|
| 05 |
04.11 & 08.11 |
weak monadic second-order logic, Myhill-Nerode relations |
pdf (1x1, 4x1) |
|
pdf |
| 06 |
11.11 & 15.11 |
weak monadic second-order logic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 07 |
18.11 & 22.11 |
Presburger arithmetic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 08 |
25.11 & 29.11 |
Büchi automata |
pdf (1x1, 4x1) |
pdf |
pdf |
| 09 |
02.12 & 06.12 |
Büchi automata, complementation, monadic second-order logic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 10 |
09.12 & 13.12 |
generalized Büchi automata, linear-time temporal logic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 11 |
16.12 & 10.01 |
LTL model checking |
pdf (1x1, 4x1) |
pdf |
|
| 12 |
13.01 & 17.01 |
alternating (Büchi) automata, LTL model checking |
pdf (1x1, 4x1) |
pdf |
|
| 13 |
20.01 & 24.01 |
exam practice |
|
|
|
|
27.01 |
1st exam |
|
|
|
Literature
Slides and solutions to selected exercises will be made available online.
Accompanying literature will be provided.