无穷字母表上的形式模型：逻辑与自动机

形式模型的研究是理论计算机科学的主要分支之一。经典的形式模型的一个基本假设是字母表是有限的。近年来，由于程序的形式验证和XML文档处理的研究的推动，无穷字母表（标号+数据）上的形式模型的研究正成为一个热点。本项目的目标是对具有无穷字母表的串和树上的逻辑和自动机的表达能力、复杂性和算法进行全面研究。首先在有限字母表上，自动机的代数（半群）理论已经发展比较成熟，本项目将对无穷字母表上的半群理论进行探讨，重点考虑如何利用半群理论来获得逻辑的表达能力的可判定刻画。为了简化问题，目前的大部分研究工作都假设无穷字母表中的数据只能进行是否相等的比较。本项目将对可以比较数据大小的无穷字母表上的串和树的形式模型进行重点研究。而且本项目还将探讨具有无穷字母表的串上的形式模型和时间串（timed word）上的形式模型之间的联系，以及考虑将有限字母表上的转换器（transducer）理论扩展到无穷字母表上。

本项目在无穷字母表上的形式模型方面展开研究，总体目标是寻找在表达能力与复杂性方面取得良好平衡的自动机模型与逻辑系统。围绕这个总体目标，本项目在多个方面进行了探讨，取得了以下四项主要成果：1. 找到了数据串上的经典自动机模型数据自动机的一个在表达能力与复杂性方面取得良好平衡的子模型，可交换数据自动机，证明其非空性问题具有初等时间的复杂度（3NEXPTIME），并将该结果扩展到无穷数据串上。2.对数据树上的递归查询语言Datalog的可满足性问题与蕴涵问题的可判定性与复杂性进行了全面的探讨。确定了这两个问题的可判定性的边界，证明了在数据树上，可满足性问题、Datalog查询相对于非递归Datalog查询的蕴涵问题、以及一元Datalog查询的蕴涵问题一般来说是不可判定的，而在深度受限的数据树上，这三个问题都是可判定的。3.对经典时序逻辑LTL和CTL的带数据变量量词的扩展（称为VLTL和VCTL）的可满足性问题和模型检测问题的可判定性进行了探讨。确定了不同子集的这两个问题的可判定性的边界，找到了一些在表达能力与复杂性方面取得良好平衡的子集。比如我们证明了对于VLTL和VCTL来说，存在数据变量量词或者公式最前面的单个全称数据变量量词就已经使得可满足性问题变得不可判定，但是如果存在数据量词不嵌套，则可满足性问题变得可以判定。而且对于VCTL来说，如果只含有存在的路径量词，则可满足性问题是可判定的，不管是否使用存在或者全称的数据变量量词。从可满足性问题的可判定性结果，我们可以进一步得到模型检测问题的可判定结果。4.提出了图数据库上的正规路径查询语言的带刚性数据约束的扩展，称为刚性正规数据路径查询语言。证明了其在表达能力与复杂性方面取得了良好的平衡：首先只需要对图数据库的结构作局部的变动，就可以将任何一个正规数据路径查询转换为刚性正规数据路径查询。而且与正规数据路径查询不同，刚性正规数据路径查询的蕴涵问题是可判定的。这些成果分别发表在理论计算机科学方面的知名国际会议Computer Science Logic, International Conference on Database Theory, Foundations of Software Technology and Theoretical Computer Science上。