[This local archive copy is from the official and canonical URL, http://www.informatik.uni-trier.de/~seidl/Trees.html; please refer to the canonical source document if possible.]
Applications of Tree Automata in Rewriting, Logic and Programming.
October 20-24, 1997.
Schloss Dagstuhl, Germany
|
Hubert Comon Ecole Normale Supérieure Lab. Specification et Verification 61 Ave. du Président Wilson F-94235 Cachan Cedex hubert.comon@lsv.ens-cachan.fr |
Dexter Kozen Cornell Univ., Comp. Sci. 5145 Upson Hall Ithaca, NY 14850-7501 kozen@cs.cornell.edu |
|
Helmut Seidl Universität Trier Fachbereich IV-Informatik D-54286 Trier seidl@uni-trier.de |
Mosche Y. Vardi Rice University Dep. of Comp. Sci. 6100S Main Street Houston, TX vardi@cs.rice.edu |
The idea of organizing 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 realized 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, ignore 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 specialized 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 realized recently. For instance, by forgetting (some of) the relations between the variables, we obtain a binary relation which can be recognized 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, m-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 m-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-fertilization, 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 meeting as 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.
We also like to thank Reinhard Wilhelm and the peaple at Dagstuhl who really made it a pleasure to organize the workshop. We all felt that Dagstuhl did a very good job in providing us with a friendly and stimulating surroundings for our work.