Lehrstuhl Informatik II   
Sprachen und Beschreibungsstrukturen      
   Home Lehre Sommersemester 17 Vorlesungen Automata Theory 2 login

Automata Theory 2

Dozent:Prof. Dr. Helmut Seidl
Ort/Zeit:Seminar Room 02.07.014, Thur. 10-12, Exercises Room 01.07.014, Wed. 9:30-11
Beschreibung:    Advanced automata models for program analysis and XML processing.


  • Update: The oral exam will be on Monday, 07.08.2017 starting at 10:30. See Exam section below.
  • The oral exam will be on Monday, 07.08.2017 starting at 9:30. Individual time slots will be assigned some days beforehand. Please unregister in TUMOnline if you do not want to be examined.
  • From now (21.06.) on the Wednesday meeting (usually exercises) will always take place in room 02.07.014.
  • We decided that there will be a lecture on Wednesday, 21.06.2017 at 9:30 instead of the exercise session. It will take place in room 02.07.014.
  • You may now do some homework in order to get a grade improvement (see Exercises section below).
  • Due to incorrect configuration, registration for exercises was not possible in TUM-Online. This should now be fixed.
    Anyway, exercise sessions take place on Wednesdays at 9:30 in room 01.07.014 and you are highly encouraged to participate.
  • Exercises start on 03.05.17 at 9:30 in room 01.07.014, so there is no exercise session on 26.04.17!


This course considers selected topics of automata theory for devices operating on tree structured data.
The models and methods which we develop have applications in the areas of static program analysis
of tree manipulating programming languages and and XML processors.

The lecture is organized as follows. In the first part, we review basic notions and properties
of finite tree automata. We demonstrate how these can be applied to the analysis of (1) functional
and (2) logic based programming languages. As a convenient tool, we introduce the class H1 of
Horn clauses which is flexible enough to provide us with a useful tool for the analysis of
cryptographic protocols.

In the second part, we equip finite state automata with output. In the center of our exposition
are macro tree transducers which are at the heart of XML transformation languages. We provide
several useful composition and decomposition results and ultimately show that type checking for
these is decidable. Here, type checking is the task to verify for a transformation that valid
input trees always will be transformed into valid output trees.

Finally in the third part, we turn to one central verification task, namely, to decide whether
or not two programs are equivalent. We review instances of this problem at various levels
of difficulty. As a warm-up, we consider the equivalence problem for straight-line programs.
On the next stage, we consider tree-to-tree, then tree-to-string transformations and, ultimately,
arbitrary programs. For each instance, we provide dedicated techniques which, in the most general case,
however, are doomed to be incomplete.


The oral exam will take place on Monday, 07.08.2017 at 10:30 in room 02.07.044.
Participants will be examined one after another (roughly 30 minutes each), so please bring some time!

There won't be a repeat exam.

Please unregister in TUMOnline, if you do want to withdraw.


Lecture slides until 20.07.2017.


We decided to provide homework assignments to give you an opportunity to practice and obtain a grade improvement of 0.3:

  • Exercise sheets (including homework assignments) will be handed out during the exercise sessions and will be uploaded here shortly before the session.
  • Homework assignments must be solved individually (no group solutions).
  • Solutions are accepted until the beginning of the following exercise session.
  • Solutions may be handed in at the exercise session or may be submitted electronically to nico.hartmann@in.tum.de.
  • Submissions will be corrected and graded with up to 20 points each.
  • You need to achieve 2/3 of the total points over all sheets in order to get a grade improvement of 0.3.
  • The grade improvement is only granted if the exam is passed (without the improvement).
  • A solution to the exercises will be uploaded after the deadline.

If you have any questions regarding organization or content of the exercises, please contact Nico Hartmann (nico.hartmann@in.tum.de).

# Date Keywords Sheet Solutions
1 03.05.2017 Deterministic and nondeterministic bottom-up tree automata. exercise01.pdf exercise01-solution.pdf
2 10.05.2017 Top-down tree automata, Dual Powerset Construction. exercise02.pdf



3 17.05.2017 H3-clauses, H3-normalization, analysis of functional programs. exercise03.pdf



4 24.05.2017 Analysis of functional programs, H1-solver, H1-normalization. exercise04.pdf



5 31.05.2017 Analysis of Prolog programs, H1-approximation, Magic-Set Transformation. exercise05.pdf



6 14.06.2017 Analysis of Communication Protocols (Needham-Schroeder), Transformation Language TL, Document Transformation exercise06.pdf



7 28.06.2017 TL to Macro Tree Transducers, Equivalence of Integer SLPs exercise07.pdf



8 05.07.2017 TL to Macro Tree Transducers (Local Movement) exercise08.pdf



9 12.07.2017 String SLPs, Complete Lattices, Fixpoint Computation exercise09.pdf



10 19.07.2017 String SLPs, Equivalence of Tree-To-Tree Transducers, Affine Closures exercise10.pdf



11 26.07.2017 Tree-To-String Transducers, Inductive Invariant exercise11.pdf  exercise11-solution.pdf


angehängte Dateien:


TUM - Lehrstuhl Informatik II (Sprachen und Beschreibungsstrukturen) Thanks: Tango and TinyMCE     Generationszeit: 10 ms