面向半结构化数据的树逻辑及其性质研究  

Tree Logic for Semistructured Data and Its Properties

作　　者：韩婷婷[1] 陈韬略[1] 俞春[1] 吕建[1] 

机构地区：[1]南京大学计算机软件新技术国家重点实验室,南京210093

出　　处：《南京大学学报（自然科学版）》2005年第2期162-170,共9页Journal of Nanjing University（Natural Science）

基　　金：国家重点基础研究发展规划973项目(2002CB12002);国家自然科学基金(60273034;60233010;60403014);国家863高科技项目(2002AA116010);江苏省自然科学基金(BK2002203;BK2002409)

摘　　要：　半结构化数据正以其灵活性而成为解决Internet环境下互操作语义层面问题的重要工具和网络数据交换格式的标准.从基础理论层面上对版结构化数据进行研究,在考察了进程代数和空间逻辑的有关结果后,从模型和逻辑系统的角度对半结构化数据特别是XML语言进行刻画.在[1]的基础上,在数据模型中加入了受限算子,并提出一种新的空间逻辑———树逻辑,在其中引入了一个新的模态算子,它们的意义在于能够对私有数据的性质进行刻画和表达.此外,通过修正数据模型中的同余关系,使得模型符合数据的有序性,从而使其更为合理.在此基础上证明了树逻辑系统公式可满足性的不可判定性,从而说明针对整个树逻辑系统的模型检测算法是不存在的.同时选择了其中一个子逻辑系统,给出了其模型检测算法,并证明了该算法的正确性.With the development of Internet, the semistructured data have already become a very important tool to deal with the problems of communication at the level of semantics and at the same time become the standard of the data exchange form in Internet. From the theoretical point of view, we characterize the semistructured data, especially the XML language, both in data model and in logic system inspired by the results of process algebra and spatial logic. Based on([1]), the so-called restriction operator is introduced into the data model and at the same time, we provide a new spatial logic-tree logic, in which a new modal operator is added. The two operators are mainly used to manipulate and describe the properties of private data elements, which becomes more and more important in modeling and analyzing semistructured data for security or other considerations. Besides, we refine the congruence relation in the data model so that the order of the data is presented. This is more rational since it is not always the same if the order of two sub-trees is exchanged. The properties of the tree logic system are studied. We prove the undecidability of the satisfaction problem for the logic. As a result, model checking the whole tree logic system is impossible. In addition, we choose an important sub-logic system for which a model checking algorithm is presented. The correctness of the algorithm is also proved.

关 键 词：半结构化数据 树逻辑 不可判定性 模型检测 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]