基于模型檢測的半結(jié)構(gòu)化數(shù)據(jù)查詢及其應用.pdf

1、Internet的迅猛發(fā)展，導致Web上的半結(jié)構(gòu)化數(shù)據(jù)急劇膨脹。因此，對這類數(shù)據(jù)的查詢?nèi)找娉蔀樾畔⒓夹g(shù)領(lǐng)域一個重要的研究發(fā)展方向?，F(xiàn)有的半結(jié)構(gòu)化數(shù)據(jù)查詢語言在查詢方式以及查詢效率上存在著不足。本文針對這些問題提出了將模型檢測技術(shù)應用于半結(jié)構(gòu)化數(shù)據(jù)查詢的方法，并給出了該方法在現(xiàn)有半結(jié)構(gòu)化數(shù)據(jù)查詢語言上的應用過程。 本文首先介紹了半結(jié)構(gòu)化數(shù)據(jù)及其數(shù)據(jù)模型與查詢語言。對現(xiàn)有的半結(jié)構(gòu)化數(shù)據(jù)查詢語言的查詢方式及數(shù)據(jù)模型進行分析，得知半結(jié)構(gòu)

2、化數(shù)據(jù)的數(shù)據(jù)模型通常表示為有向標記圖，因此，對半結(jié)構(gòu)化數(shù)據(jù)的查詢操作就對應為從標記圖中抽出信息，即查詢過程也就是對半結(jié)構(gòu)化數(shù)據(jù)庫實例圖查找滿足查詢條件的子圖的過程。該過程涉及到圖的等價問題，目前已有的兩種等價關(guān)系為圖同構(gòu)和圖雙模擬。但是，對圖同構(gòu)問題并沒有具體的多項式算法用于解決子圖的同構(gòu)問題也不能解決圖的同構(gòu)問題。判斷兩個圖的雙模擬等價過程可以在多項式時間內(nèi)完成，但是會涉及到搜索實例圖中匹配查詢條件的子圖過程，而該過程是NP完全的。

3、 本文針對以上問題，提出將模型檢測技術(shù)應用到半結(jié)構(gòu)化數(shù)據(jù)查詢，也即是將時序邏輯公式ψ與圖查詢聯(lián)系起來，且將數(shù)據(jù)庫實例解釋為Kripke變遷系統(tǒng)。這樣，查找數(shù)據(jù)庫實例圖中與查詢相匹配的子圖問題就簡化為了對KTS查找滿足時序邏輯公式ψ的狀態(tài)問題。這是模型檢測問題的一個實例，眾所周知，如果公式ψ是CTL公式，S是KTS系統(tǒng)，那么對ψ的CTL模型檢測算法可以在關(guān)于KTS和公式大小的線性組合復雜度內(nèi)完成。 最后，文中將該技術(shù)應用于現(xiàn)