Semi-structured Data Query Based Model-Checking And Its Application

The rapid development of Internet must be involved in an extreme expansion of semi-structured data, therefore, querying on such data is increasingly becoming an important research field of information and technology. Existing semi-structured data query languages have disadvantages in query model and query efficiency. In this paper, a new method is proposed to improve these problems, namely, using the model checking technology to solve the queries of semi-structured data, then a process of applying this method on existing semi-structured data query language is provided.Firstly, this thesis has introduced the semi-structured data and its data model and query languages. Under the analysis of the query model and data model of existing query languages, concluded that it is a common approach to represent semi-structured data by using directed labeled graphs, then a query on semi-structured database is becomes to get information stored in directed labeled graphs, i.e. query is substituted for finding subgraphs which satisfy the requirements of the query from database instance graph. However, the query would involve graph equivalence, there are two kinds of popular graph equivalence relations: graph isomorphism and graph bisimulation, but none represents good performance. For example, the graph isomorphism expresses neither polynomial time for the Subgraph Isomorphism problem, which is NP-complete, nor for the Graph Isomorphism problem, which is NP but not clear whether P or not; although the bisimulation test between two graph can be done in polynomial time, the task of finding subgraphs bisimilar to a given one is NP-complete.In order to solve the above problem , this paper propose an application of model checking technology based queries of semi-structured data, the main idea is to treat a query as a formulaΨof the Computing Tree logic (CTL) and a database as a Kripke Transition System (KTS) S. So finding satisfied subgraphs of database instance graph is reduced to the problem of verification ofΨwith S, which are derived from the instance graph and query separately. This is a model checking problem, and it is well-known that the CTL-model checking is decidable in linear time in the product of the size of KTS and the formula.The method proposed in this thesis will be applied on existing semi-structured querying language Lorel and UnQL, and the procedures will be given step by step, so it will be very clear how to build the KTS associated with database model and extract formulas from queries. And a detailed case study will be also provided. Finally, we ended in a conclusion.