Automata and Formal Languages 2020/21 | ||
News | Dates | Grading | Content | Exercises | Exam | Material |
The tutorial format: We will release the exercise sheets a few days before the tutorial session. The idea is for you to have a look at the exercises and think of how to solve them. During the tutorial we will give you a few minutes to write your solutions for each exercise, during which there is time for individual questions. Then we will discuss the solution together. After the tutorial, we will post the solutions online for students who could not attend. The tutorials will not be live-streamed. There will be a Moodle forum for each exercise sheet in which you can ask questions and discuss solutions - both students and tutors can answer!
New: Instead of the in-person tutorials, starting from 10.11.2020 we will conduct the tutorial sessions on BBB at this link (no sign up or app needed) at the same time as before, 10:00 - 11:30 on Tuesdays. To make it interactive, we will use a shared whiteboard. We encourage you to use this as well as your microphone so that we can recreate the tutorial setting as much as possible.
Exercises are voluntary and do not account for the final grades.
It is highly recommended to work on the exercises, as this is the best preparation
for the exam. The exercises will mainly be taken from the
lecture notes and additional exercises may be added.
Exercice Sheets 2020/2021:
Week | Topic | Exercise sheet | Forum | Comments |
1 | DFAs, NFAs, regular expressions | Forum 1 | With solutions. | |
2 | Minimization, residuals | Forum 2 | With solutions. | |
3 | DFA and NFA operations | Forum 3 | With solutions. | |
4 | Pattern matching and Transducers | Forum 4 | With solutions. | |
5 | Fixed-length languages | Forum 5 | Without solutions. |
Past exercise sheets
Exercice Sheets 2019/2020:
Week | Topic | Exercise sheet | Additional files | Comments |
1 | DFAs, NFAs, regular expressions | With solutions. | ||
2 | Conversions, regular expressions | Python NFA-ε to NFA converter: | With solutions. | |
3 | Minimization, residuals | With solutions. | ||
4 | Reduction of NFAs and DFA operations | With solutions. | ||
5 | NFA operations | With solutions. | ||
6 | Pattern matching (plus residuals) | With solutions. | ||
7 | Transducers | With solutions. | ||
8 | Fixed-length languages | With solutions. | ||
9 | Verification of safety properties |
Promela files: #9.1(c) naive_mutex.pml: #9.2(c) mutex.pml: |
This week, we will
use Spin
to simulate and verify some algorithms. I will walk you
through Spin in class, assuming no prior knowledge. If you want to,
you can already try Spin by following these
instructions: . To understand the
basics of Promela, you can also have a look at this Wikipedia
page: . |
|
10 | Presburger arithmetic, FO, MSO | With solutions. | ||
11 | MSO, Buchi-automata | With solutions. | ||
12 | ω-automata and conversions of acceptance conditions | With solutions. | ||
13 | Boolean operations on omega-automata. | With solutions. | ||
14 | Emptiness check on omega-automata. | With solutions. In the exercise session we saw a brief introduction to JFLAP. | ||
15 | Emptiness check and Linear Temporal Logic | With solutions. | ||
16 | Linear Temporal Logic | With solutions. |
Exercice Sheets 2018/2019:
Week | Topic | Exercise sheet | Additional files | Comments |
1 | DFAs, NFAs, regular expressions | |||
2 | Conversions | Python NFA-ε to NFA converter: | ||
3 | Minimization, residuals | |||
4 | Reduction of NFAs, DFA and NFA operations | |||
5 | NFA operations | |||
6 | Pattern matching (extra topics: residuals, synchronizing automata) | |||
7 | Transducers | |||
8 | Fixed-length languages | |||
9 | Verification of safety properties |
Promela files: #9.1(c) naive_mutex.pml: #9.2(c) mutex.pml: |
This week, we will
use Spin
to simulate and verify some algorithms. I will walk you
through Spin in class, assuming no prior knowledge. If you want to,
you can already try Spin by following these
instructions: . To understand the
basics of Promela, you can also have a look at this Wikipedia
page: . |
|
10 | FO, MSO | |||
11 | ω-automata (Büchi, Rabin, Muller and parity automata) | |||
12 | Boolean operations on ω-automata and conversions of acceptance conditions. | The programming exercise is based on Owl and the template for the programming exercise can be found in the buchi-complementation branch. Please submit your solutions by mail. | ||
13 | Emptiness check, linear temporal logic (LTL) | You can use Spot for some of the exercises as tool support. | ||
14 | Linear temporal logic (LTL), verification of liveness properties | You can use Spot for some of the exercises as tool support. Check "state-based degeneralized Büchi automaton" to obtain Büchi automata. The full version of Spot is available here . |
Exercice Sheets 2017/2018:
Week | Topic | Exercise sheet | Solutions | Additional files | Comments |
1 | DFAs, NFAs, regular expressions | ||||
2 | Conversions | Python NFA-ε to NFA converter: | |||
3 | Minimization, residuals | ||||
4 | DFA operations | ||||
5 | NFA operations | ||||
6 | Pattern matching (extra topics: residuals, synchronizing automata) | Python implementation of the algorithms computing synchronizing words: | |||
7 | Transducers | ||||
8 | Fixed-length languages | Python implementation of the master automaton: | 19.02.18: There was a typo in the tree of #8.1(b). The node below the root should be labeled make(add-lang({bb}), add-lang({ba, bb})) and not make(add-lang({bb}), add-lang({bb})). It is now fixed. The rest of the tree was correct, so the rest of the answer is correct. | ||
9 | Verification of safety properties |
Promela files: #9.1(c) naive_mutex.pml: #9.1(h) mutex_chan.pml: #9.1(h) alternative_solution.pml: #9.2(c) mutex.pml: #9.3(c) hyman.pml: #9.4(c) mutex_three.pml: |
This week, we will
use Spin
to simulate and verify some algorithms. I will walk you
through Spin in class, assuming no prior knowledge. Since the
exercises were uploaded a bit late, I will also assume you
have not done the exercises at home. If you want to, you can
already try Spin by following these
instructions: . To understand the
basics of Promela, you can also have a look at this Wikipedia
page: . The papers of Hyman and Knuth discussed in class are available at and . Unfortunately they are not freely available, but you can obtain them online through the library: . 21.01.18: The solutions of #9.2(b) and (e) were incorrect. They have been updated. |
||
10 | Presburger arithmetic, first-order and second-order logic on words (FO/MSO) |
Python implementation of the algorithms of
#10.1: MONA files: #10.3(b) partial_solution.mona: #10.3(b) solution.mona: |
We will use MONA in class for Ex. #10.3(b). MONA is available
here: . You can either
install it or use it online here:
. In the online version, you may derive an automaton from a formula by selecting Output whole automaton in Graphviz format. MONA uses a slightly different bit-vector encoding than the one we have seen in class:
|
||
11 | ω-automata (Büchi, Rabin, Muller and parity automata) | ||||
12 | Büchi automata: conversions and operations | ||||
13 | Emptiness check, linear temporal logic (LTL) | ||||
14 | Linear temporal logic (LTL), verification of liveness properties | Spot's online translator can be found here: . Check "state-based degeneralized Büchi automaton" to obtain Büchi automata. The full version of Spot is available here . | |||
15 | Recap | We will go through last year's exam in class on Feb. 8. |
Exercice Sheets 2016/2017:
- Exercise sheet 14 (with solutions).
- Exercise sheet 13 (with solutions). Spot commands to manipulate LTL formulas can be found here.
- Exercise sheet 12 (with solutions).
- Exercise sheet 11 (with solutions). Solutions of #2 in the Hanoi Omega-Automata format: DBA #11.2a, NBA #11.2b. As seen in class, these automata can be minimized by Spot using these commands.
- Exercise sheet 10 (with solutions).
- Exercise sheet 9 (with solutions).
- Exercise sheet 8 (with solutions).
- Exercise sheet 7 (with solutions). Python implementation of the master automaton: fixedlength.py.
- Exercise sheet 6 (with solutions).
- Exercise sheet 5 (with solutions).
- Exercise sheet 4 (with solutions). Python implementations of the algorithms computing synchronizing words: synchronizing.py.
- Exercise sheet 3 (with solutions). NFA-ε to NFA converter: nfa-eps2nfa.py.
- Exercise sheet 2 (with solutions). JFLAP examples: DFA #2.1c.
- Exercise sheet 1 (with solutions). JFLAP examples: DFA #1.2, NFA #1.3a, NFA #1.3b.
Exercice Sheets 2015/2016:
- Exercise Sheet 1 (Wed 21.10.15) [Sample Solution]
- Exercise Sheet 2 (Fri 23.10.15) Now equipped with solutions. Don't hesitate to let me know if you have any questions arising therefrom.
- Exercise Sheet 3. [Sample Solution] Also discussed in the class: Exercises 1.3, 1.4
- Exercise Sheet 4 (Wed 04.10.15). With solutions
- Exercise Sheet 5. [Sample Solution]
- Exercise Sheet 6 With solutions
- Exercise Sheet 7 [Sample Solution]
- Exercise Sheet 8 With solutions
- Exercise Sheet 9 [Sample Solution]
- Exercise Sheet 10 . With solutions
- Exercise Sheet 11 [Sample Solution]
- Exercise Sheet 12 . With solutions.
- Exercise Sheet 13 [Sample Solution]
- Exercise Sheet 14 . With solutions.
- Exercise Sheet 15 (Mon 01.02.16) [Sample Solution]
- Exercise Sheet 16 (Wed 03.02.16) . With solutions.
Exercise Sheets 2012/2013:
- Exercise 1, solution to Ex.1.3
- Exercise 2, solution to Ex.2.6 and 7
- Exercise 3 (updated on Nov 6, two of the exercises originally posted here will be dealt with later)
- Exercise 4
- Exercise 5, transducer for Ex.5.3
- Exercise 6
- Exercise 7
- Exercise 8
- Exercise 9
- Exercise 10
- Exercise 11
- Exercise 12
- Exercise 13: Q&A session + some LTL
Exercise Sheets 2011/2012:
- Exercise 1
- Exercise 2
- Exercise 3
- Exercise 4
- Exercise 5
- Exercise 6
- Exercise 7
- Exercise 8
- Exercise 9
- Exercise 10
- Exercise 11
- Exercise 12
- Exercise 13: 12.2
- Exercise 14: Q&A session + some LTL
Exercise Sheets 2010/2011:
Exercises with two stars form a necessary part of your preparation for the exam. One starred ones are recommended. Exercises with no star are useful for deeper understanding.
- Exercise 1 (**: 1,3)
- Exercise 2 (**: 1,2,4)
- Exercise 3 (**: 1,2,3,5)
- Exercise 4 (**: 1,2,5)
- Exercise 5 (**: 2)
- Exercise 6 (**: 1,2)
- Exercise 7 (**: 1)
- Exercise 8 (stars indicated in the sheet)
- Exercise 9 (stars indicated in the sheet)
- Exercise 10 (**: 1,2)
- Exercise 11 (**: 2)
- Exercise 12 (stars indicated in the sheet)
- Last year's exam and its solution
Exercise Sheets 2009/2010:
- Exercise 1
- Exercise 2
- Exercise 3
- Exercise 4
Slides for the bisim game exercise - Exercise 5
- Exercise 6
- Exercise 7
- Exercise 8
- Exercise 9
- Exercise 10
- Exercise 11
- Exercise 12