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

结合硬件和软件验证，已经广泛地研究了用于描述标记树的属性的逻辑以及在这种树上操作的自动机。最近，它们一直是XML文档的规范和查询语言研究的主题，这将注意力集中在未排名的树上-在这些树中，节点的子节点数量没有固定的界限。然而，关于这种逻辑的表达能力的许多基本问题仍然没有得到回答；例如，我们还没有对一阶逻辑的各种版本中可表达的树的性质进行有效的描述。这项研究项目通过一种新的代数自动机理论来探讨这些问题。虽然这项工作的大部分动机来自逻辑，但遇到的困难问题本质上是代数的：所需要的是加深对树自动机的一种新的代数不变量--称为森林代数--的理想和分解结构的理解。该项目将借鉴有限半群结构的非常丰富的理论，这些理论是在研究单词自动机的过程中发展起来的。其中一个主要的挑战是将已知的关于有限半群结构的知识推广到这种新的更复杂的环境中。这项研究将进一步发展新的数学工具来确定树上逻辑的表达能力。该项目的成功完成最终将使这些工具的应用远远超出最初推动这项研究的问题，并在开发和分析软件和硬件验证语言、XML查询语言和表示数据的相关方案方面产生潜在的实际影响。

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.