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
ModulNummer:IN2042
Beschreibung:    Advanced automata models for program analysis and XML processing.

News

  • 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!

Content

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.

Slides

Lecture slides until 08.06.2017.

Exercises

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

exercise02-solution-p.pdf

exercise02-solution.pdf

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

exercise03-solution-p.pdf

exercise03-solution.pdf

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

exercise04-solution-p.tar.gz

exercise04-solution.tar.gz

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

exercise05-solution-p.tar.gz

exercise05-solution.tar.gz

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

 



angehängte Dateien:

    folien-1.pdf
    folien-2.pdf
    folien-3.pdf
    h1-solver.tar.gz
    folien-4.pdf
    folien-6.pdf

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