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

半结构化数据正以其灵活性而成为解决Internet环境下互操作语义层面问题的重要工具和网络数据交换格式的标准．从基础理论层面上对版结构化数据进行研究，在考察了进程代数和空间逻辑的有关结果后，从模型和逻辑系统的角度对半结构化数据特别是XML语言进行刻画．在1]的基础上，在数据模型中加入了受限算子，并提出一种新的空间逻辑——树逻辑，在其中引入了一个新的模态算子，它们的意义在于能够对私有数据的性质进行刻画和表达．此外，通过修正数据模型中的同余关系，使得模型符合数据的有序性，从而使其更为合理．在此基础上证明了树逻辑系统公式可满足性的不可判定性，从而说明针对整个树逻辑系统的模型检测算法是不存在的．同时选择了其中一个子逻辑系统，给出了其模型检测算法，并证明了该算法的正确性．

Tree Logic for Semistructured Data and Its Properties

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.