20. – 24. Oktober 1997, Dagstuhl-Seminar 9743

Applications of Tree Automata in Rewriting, Logic and Programming


H. Comon (LRI Orsay), D. Kozen (Cornell), H. Seidl (Trier), M. Vardi (Rice)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Externe Homepage
Dagstuhl-Seminar-Report 193


The idea of organising this seminar came during the Federated Logic Conference, New Brunswick, 1996, which brought together the Symposium on Logic in Computer Science, the Conference on Rewriting Techniques and Applications, the Conference on Automated Deduction and the Conference on Computer Aided Verification. We realised there that, though logic was the straightforward intersection between these four communities, there were also common underlying themes and techniques of more specific nature. An important example was, applications of tree automata". This computational model is indeed used in various domains of applications which, to some extent, have ignored each other.

In automated deduction, it seems that general purpose fully automated theorem provers are reaching a limit; they still improve, but the factor of improvement is decreasing. The idea which was raised to combine specialised theorem provers which provide efficient techniques for some specific problems, together with a general purpose prover. An idea would be to use tree automata techniques each time this is possible. For example, equality modulo ground term equations can handled in this way.

Most of the properties of term rewriting systems (like reachability, word problem, sequentiality,...) are undecidable. Hence we are led either to consider only subclasses or to design sufficient conditions guaranteeing these properties. Tree automata play an important role in the design of such classes (or sufficient conditions), which has only been realised recently. For instance, by forgetting (some of) the relations between the variables, we obtain a binary relation which can be recognised by a Ground Tree Transducer. Then all properties of rewrite systems become decidable.

Computer Aided Verification, and especially model checking, became very popular in the recent years because of its security applications; some critical applications might have disastrous consequences if the software managing them is not correct. Several logics and several models have been proposed in the last years. For instance, mu-calculus and CTL on the logical side, and Kripke structures and their unfoldings in tree form on the model side. Already in the sixties, it was shown that monadic second-order formulas and hence mu-calculus expressions and CTL-formulas can be converted into automata. The model checking problem was thus reduced to an inclusion test for languages defined by (sequential or tree) automata, possibly consisting also of infinite strings or trees. Although efficient model checking procedures are by now a standard tool, refinements of the theory are needed to overcome several practical problems, notably the, state explosion problem and deficiencies in expressiveness.

Also compiler construction turns out to be a surprisingly wide area of applications for tree automata. These range from backend generation over generation of attribute evaluators to program analysis. In the case of program analysis, the basic idea is to approximate the program by some formal device for which there are tractable algorithms. Tree automata or, equivalently, regular tree grammars and various subclasses of set constraints have attracted attention for such an approximation. While simple forms of set constraints are directly equivalent to finite tree automata, it turns out that more general forms also require advanced tree automata techniques.

In order to stimulate cross-fertilisation, this seminar brought together researchers who are involved in such applications.

A special session discussed the impact of our results on education. In our opinion, the workshop was a success. Exciting discussions took place until late in the evenings -- which has been especially supported by this form of meetings well as by facilities offered at Dagstuhl, like open access to seminar rooms or the library. By a group of French researchers, a first draft of a basic textbook on tree automata was presented. The community is invited to comment on details or contribute sections.


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.