Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Home
 Contact
 Teaching
lectures
exercises
seminars
proseminars
research seminars
practical courses
WS 2020/21
SS 2020
WS 2019/20
SS 2019
WS 2018/19
SS 2018
WS 2017/18
SS 2017
WS 2016/17
SS 2016
WS 2015/2016
SS 2015
WS 2014/2015
SS 2014
WS 2013/2014
SS 2013
WS 2012/2013
SS 2012
WS 2011/2012
SS 2011
WS 2010/2011
SS 2010
WS 2009/2010
SS 2009
WS 2008/2009
SS 2008
WS 2007/2008
SS 2007
WS 2006/2007
SS 2006
WS 2005/2006
SS 2005
WS 2004/2005
SS 2004
Before 2004
 People
Publications
 Student Projects
Research
Tools
Heroes of Computer Science
 Help

































Automata and Formal Languages 2019/20

  News | Dates | Grading | Content | Exercises | Exam | Material | Programming Assignement

Exercises are voluntary and do not account for the final grades. Submitted exercises will be corrected and handed back. 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. The solutions will be published as part of the updated lecture notes.

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.


Past exercise sheets

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:
  • the first position of bit-vectors is -1, which you can ignore for our purposes since first/second-order variables can never hold -1;
  • first/second-order variables can hold 0;
  • the value of a first-order variables is represented by the position of the first "1" in a bit-vector (it needs not to be unique); e.g. "y: X001010" is a valid encoding of y = 2.
For more information on MONA, have a look at Sections 1 and 2 of its user manual: .
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:

Exercice Sheets 2015/2016:

Exercise Sheets 2012/2013:

Exercise Sheets 2011/2012:

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 Sheets 2009/2010:

Exercise Sheets 2008/2009: