Lehrstuhl Informatik II   
Sprachen und Beschreibungsstrukturen      
   Home Lehre Sommersemester 18 Vorlesungen Automata Theory II (DISCONTINUED) login

Automata Theory II (DISCONTINUED)

Dozent:Prof. Dr. Helmut Seidl
Beschreibung:    Advanced automata models for program analysis and XML processing.


DISCONTINUED: Due to the lack of participating students, we decided to cancel the lecture, so neither the lecture, nor the exercises will take place during this semester.


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.


to be announced ...


to be announced ...


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


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