基于模型检测的半结构化数据查询  

Model-Checking Based Semi-structured Data Query

作　　者：刘林霞[1] 张自强[1] 何安平[2] 

机构地区：[1]兰州大学信息工程与科学学院,兰州730000 [2]兰州大学数学院,兰州730000

出　　处：《计算机与数字工程》2009年第8期75-79,共5页Computer & Digital Engineering

摘　　要：在Web迅猛发展和半结构化数据急剧膨胀的今天,Web上的半结构化数据查询日益成为信息技术领域一个重要的研究发展方向。现有的半结构化查询语言在查询效率上存在着不足。文章提出了一个将模型检测技术应用到半结构化数据查询的新方法,它通过把数据库看作Kripke状态变迁系统,把查询解释为时序逻辑CTL公式,将查询过程转化为模型对公式的满足问题,通过模型检测过程高效地完成数据查询,从而使查询可以在多项式时间内完成,很好地改善了查询效率。最后,给出了该方法在现有半结构化查询语言Lorel上的应用。With the rapid development of Web, larger volumes of semistructured data have been available. Therefore, querying semistructured data on the Web has been more and more important nowadays. Existing semistructured data query languages have disadvantages in efficiency. In this paper, a new method is proposed to improve the problem, namely, use the model checking to solve semistructured data query, the main idea is to see a database as a Kripke Transition System （Kripke structure） and a query as a formula of the temporal logic CTL. In this way, the query is reduced to the problem of finding out the states of the model which satisfy the formula, then by using the process of model checking to achieve the query in polynomial time, so as to improve the efficiency of querying. Finally, the method is applied on existing language Lorel.

关 键 词：模型检测 时序逻辑 Lorel OEM模型 

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