SHF: AF: Small: Algebraic Methods for the Study of Logics on Trees

点击翻译按钮获取中文摘要

Logics for describing properties of labeled trees, along with automata operating on such trees, have been studied extensively in connection with hardware and software verification. More recently they have been the subject of research on specification and query languages for XML documents, and this has focused attention on unranked trees---those in which there is no fixed bound on the number of children a node may have. However, many fundamental questions about the expressive power of such logics remain unanswered; for instance, we do not yet possess an effective description of the properties of trees that are expressible in various versions of first-order logic. This research project approaches these questions by means of a new algebraic theory of automata operating on unranked trees.While much of the motivation for this work comes from logic, the difficult questions encountered are algebraic in nature: what is required is a deepened understanding of the ideal and decomposition structure of a new kind of algebraic invariant ---called forest algebras---for tree automata. The project will draw on a very rich theory of the structure of finite semigroups developed in connection with the study of automata on words. One of the principal challenges entails generalizing what is already known about the structure of finite semigroups to this new and more complex setting.This research will further the development of new mathematical tools to determine the expressive power of logics on trees. Successful completion of the project should ultimately lead to the application of these tools well beyond the problems that originally motivated the study, and has a potential practical impact in the development and analysis of languages for software and hardware verification, and of query languages for XML and related schemes for representing data.