| 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.
| 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 | With solutions. | |
| 6 | Verification of safety properties | Forum 6 |
With solutions. 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: Promela files used in this class: #6.2(c) naive_mutex.pml: #6.3(c) mutex.pml: |
|
| 7 | FO and MSO | Forum 7 | With solutions. | |
| 8 | MSO and Presburger | Forum 8 | With solutions. | |
| 9 | Buchi automata | Forum 9 | With solutions. Solutions of Exercise 9.3 from tutorial can be found here. | |
| 10 | Conversions of acceptance conditions | Forum 10 | With solutions. | |
| 11 | Boolean operations on omega-automata | Forum 11 | With solutions. | |
| 12 | Buchi emptiness and LTL | Forum 12 | With solutions. | |
| 13 | Linear Temporal Logic | Forum 13 | With solutions. |