Automata Theory 2
|Dozent:||Prof. Dr. Helmut Seidl|
|Ort/Zeit:||Seminar Room 02.07.014, Thur. 10-12|
|Beschreibung: ||Advanced automata models for program analysis and XML processing.|
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.