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
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 email@example.com.
- 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 (firstname.lastname@example.org).
||Deterministic and nondeterministic bottom-up tree automata.
||Top-down tree automata, Dual Powerset Construction.
||H3-clauses, H3-normalization, analysis of functional programs.
||Analysis of functional programs, H1-solver, H1-normalization.
||Analysis of Prolog programs, H1-approximation, Magic-Set Transformation.
||Analysis of Communication Protocols (Needham-Schroeder), Transformation Language TL, Document Transformation
||TL to Macro Tree Transducers, Equivalence of Integer SLPs
||TL to Macro Tree Transducers (Local Movement)
||String SLPs, Complete Lattices, Fixpoint Computation
||String SLPs, Equivalence of Tree-To-Tree Transducers, Affine Closures
||Tree-To-String Transducers, Inductive Invariant