基于模型檢查的XML樹模式優(yōu)化動(dòng)作生成

趙瑞芳 劉 科 楊紅麗 廖湖聲

(北京工業(yè)大學(xué) 北京 100124)

基于模型檢查的XML樹模式優(yōu)化動(dòng)作生成

趙瑞芳 劉 科 楊紅麗 廖湖聲

(北京工業(yè)大學(xué) 北京 100124)

針對(duì)XML數(shù)據(jù)查詢的核心操作-樹模式查詢，提出基于XML Schema約束來優(yōu)化樹模式查詢的方法。該方法提出了統(tǒng)一的優(yōu)化規(guī)則描述語言O(shè)RS的語法與語義。ORS描述的優(yōu)化規(guī)則中包括對(duì)樹模式條件的描述、對(duì)XML Schema條件的描述以及在滿足前兩個(gè)條件下應(yīng)該輸出的動(dòng)作。根據(jù)ORS語言描述的優(yōu)化規(guī)則以及待處理的樹模式，系統(tǒng)會(huì)自動(dòng)輸出該樹模式的優(yōu)化動(dòng)作。該方法一方面簡化了樹模式優(yōu)化的過程，另一方面把模型檢查技術(shù)運(yùn)用到XML樹模式查詢優(yōu)化上，利用時(shí)態(tài)邏輯公式描述優(yōu)化規(guī)則中的約束條件，利用模型檢查的方法提取XML Schema的約束，對(duì)ORS語法和語義的嚴(yán)格定義確保了生成的優(yōu)化動(dòng)作的正確性。

樹模式優(yōu)化 ORS XML Shema 模型檢查

0 引 言

XML以其簡單易用性，迅速在互聯(lián)網(wǎng)內(nèi)得到了廣泛的應(yīng)用。為了推動(dòng)XML數(shù)據(jù)查詢和處理的標(biāo)準(zhǔn)化，國際萬維網(wǎng)組織W3C發(fā)展了XQuery語言作為XML數(shù)據(jù)的查詢語言。XQuery語言采用XPath表達(dá)式定位數(shù)據(jù)，它對(duì)于XML的作用類似于SQL對(duì)于關(guān)系數(shù)據(jù)庫的作用[1]。XQuery作為其查詢語言，近年來也受到了大量的關(guān)注。而樹模式查詢作為XQuery查詢的核心操作，樹模式查詢的優(yōu)化也受到了廣大學(xué)者的關(guān)注。他們或是提出更加高效的算法，或是應(yīng)用更加有效地?cái)?shù)據(jù)結(jié)構(gòu)來優(yōu)化查詢。

樹模式優(yōu)化基本可以分為有約束和無約束兩種情況[2]。在有約束的情況下，這些約束一般來自于DTD和XML Shema等XML文檔的結(jié)構(gòu)信息中。經(jīng)典的文獻(xiàn)[3]論述了在有約束和無約束的情況下樹模式最小化的策略。例如在有shema約束的情況下，要求約束有必然后代、必然子女關(guān)系等，而且對(duì)最小化的結(jié)論給出了嚴(yán)格的數(shù)學(xué)證明。文獻(xiàn)[4]利用XML Schema中的約束信息首先將XML查詢轉(zhuǎn)化為等價(jià)的語義查詢，然后捕獲給定的XML文檔的結(jié)構(gòu)并存儲(chǔ)到關(guān)系數(shù)據(jù)庫的一個(gè)表中，最后執(zhí)行查詢。在通過提高算法效率來優(yōu)化樹模式的相關(guān)工作也有很多。文獻(xiàn)[5]提出了一種整體的不需要分解樹模式的算法處理帶有OR謂詞的樹模式，并驗(yàn)證了自己算法較基于樹模式分解的算法具有更好的性能。文獻(xiàn)[6]為樹模式匹配算法和查詢執(zhí)行的綜述性文章，首先系統(tǒng)介紹了關(guān)于樹模式查詢方面的研究現(xiàn)狀，然后介紹了幾種不同的樹模式匹配算法。文獻(xiàn)[1]提出了一種基于XML Schema中的約束對(duì)樹模式中的查詢結(jié)點(diǎn)，帶有OR謂詞和AND謂詞的樹模式進(jìn)行優(yōu)化的方法。根據(jù)XML Schema中提取出來元素之間的特定關(guān)系，對(duì)樹模式進(jìn)行優(yōu)化。文獻(xiàn)[7]提出了優(yōu)化帶有通配符的樹模式的方法。利用一個(gè)自定義的AD-dis的邊，等價(jià)地重寫帶有通配符的查詢(非分支和分支通配符)，簡化為一個(gè)不帶任何通配符的查詢并給出了高效的重寫算法和樹模式匹配算法來重寫查詢。文獻(xiàn)[8]全面總結(jié)了目前的工作中關(guān)于樹模式查詢處理與優(yōu)化技術(shù)在不同種類的XML數(shù)據(jù)中的研究現(xiàn)狀，作者在最后探討了樹模式優(yōu)化相關(guān)技術(shù)的發(fā)展趨勢和研究方向。

綜上，通過改進(jìn)算法對(duì)樹模式的優(yōu)化已經(jīng)達(dá)到了相對(duì)完善的地步，而且一種算法只能優(yōu)化具有某種特定形式的樹模式，而將形式化的方法應(yīng)用于樹模式優(yōu)化中，對(duì)樹模式優(yōu)化過程進(jìn)行描述和優(yōu)化執(zhí)行還是一個(gè)比較新穎的課題。本文中我們把樹模式的各種優(yōu)化方法稱之為優(yōu)化規(guī)則，并給出了優(yōu)化規(guī)則的嚴(yán)格定義。為了更嚴(yán)格地定義優(yōu)化規(guī)則，我們還定義了優(yōu)化規(guī)則的描述語言O(shè)RS(Optimizing Rule Specification)，這樣為樹模式優(yōu)化的自動(dòng)化進(jìn)行夯實(shí)了基礎(chǔ)。樹模式優(yōu)化的自動(dòng)化完成的重要意義在于基于規(guī)則的方法把多種優(yōu)化方法統(tǒng)一于同一個(gè)優(yōu)化框架之下，只要能用ORS描述的優(yōu)化規(guī)則都可以對(duì)樹模式進(jìn)行優(yōu)化。并且由于借助模型檢查[10]等形式化的理論和工具，以及對(duì)規(guī)則描述語言語法和語義的嚴(yán)格定義，確保了樹模式優(yōu)化過程的正確性和對(duì)相關(guān)結(jié)論的可驗(yàn)證性。

1 樹模式定義

樹模式[10]是XML查詢語言XPath或XQuery等的通用查詢表達(dá)形式。

下面根據(jù)文獻(xiàn)[9]中定義的樹模式形式化模型GTP(Generalized Tree Pattern)，給出如下的GTP的定義：

定義1 GTP定義為如下的六元組：

GTP={TNode,TEdge,Type,Label,Root,Return}

TNode：由樹模式中各個(gè)結(jié)點(diǎn)id所組成的集合，每個(gè)不同的id都標(biāo)識(shí)樹模式中的唯一一個(gè)結(jié)點(diǎn)；

TEdge：代表樹模式中邊的集合，其中每條邊都由兩個(gè)結(jié)點(diǎn)連接，我們將每條邊采用三元組(TNode,TNode，Etype)的形式表示，其中Etype={“S-PC”,“S-AD”,“D-PC”,“D-AD”}，是邊的類型。“S-PC”，“D-PC”分別表示在樹模式中父子之間的強(qiáng)綁定和弱綁定的關(guān)系，“S-AD”、 “D-AD”分別表示祖先后代之間的強(qiáng)綁定和弱綁定的關(guān)系，其中的弱綁定關(guān)系表示約束可有可無。

Type：代表樹模式中的每個(gè)結(jié)點(diǎn)和其類型的映射關(guān)系，將此關(guān)系采用二元組(TNode,Ntype)的形式，其中Ntype={“QUERY”,“AND”,“OR”}，“QUERY”表示樹模式中的查詢結(jié)點(diǎn)(即元素結(jié)點(diǎn)),“AND”和“OR”是樹模式中的兩種邏輯結(jié)點(diǎn)。

Label：是樹模式中的每個(gè)結(jié)點(diǎn)和這個(gè)結(jié)點(diǎn)的名字之間的映射關(guān)系的集合，使用二元組(TNode,String)的形式表示。

Root：表示樹模式的根結(jié)點(diǎn)，是TNode中的元素。

Return：是TNode的一個(gè)子集，代表樹模式中全部的返回結(jié)點(diǎn)。

下面我們將通過一個(gè)樹模式的例子以及該樹模式對(duì)應(yīng)的GTP模型進(jìn)行說明。

例如圖1中樹模式舉例，單線代表結(jié)點(diǎn)之間的父子(PC)關(guān)系，雙線代表結(jié)點(diǎn)之間的子孫后代關(guān)系，實(shí)線表示強(qiáng)綁定的關(guān)系，虛線表示弱綁定的關(guān)系即可有可無的約束，標(biāo)注星號(hào)的結(jié)點(diǎn)表示樹模式查詢的返回結(jié)點(diǎn)，結(jié)點(diǎn)內(nèi)的字符串表示對(duì)應(yīng)結(jié)點(diǎn)的標(biāo)識(shí)。圖2是圖1中樹模式所對(duì)應(yīng)的GTP模型，其中結(jié)點(diǎn)旁邊的標(biāo)識(shí)表示對(duì)應(yīng)結(jié)點(diǎn)的ID。

圖1 樹模式舉例

圖2 樹模式對(duì)應(yīng)的GTP

根據(jù)GTP的形式化定義可知圖1中樹模式對(duì)應(yīng)的GTP定義如下：

TNode={1， 2， 3， 4， 5,6,7,8}

TEdge= {(1,2,S-PC),(1,3,S-PC),

(1,4,S-PC),(3,5,S-AD),

(3,6,S-PC),(3,7,D-PC),

(4,8,S-PC)}

Type={(1,QUERY),(2,QUERY),

(3,QUERY),(4,QUERY),

(5,QUERY),(6,QUERY),

(7,QUERY),(8,QUERY)}

Label={(1,shiporder),(2,person),(3,shipto),

(4,item),(5,country),(6,city),

(7,address),(8,title)}

Root=1

Return={7}

我們將樹模式的優(yōu)化方法描述為樹模式的優(yōu)化規(guī)則，而每一條優(yōu)化規(guī)則都包括：對(duì)XMLSchema特征的描述(稱之為schema條件)、對(duì)樹模式條件的描述(即樹模式子結(jié)構(gòu)所滿足的條件稱之為樹條件)，以及對(duì)優(yōu)化動(dòng)作的描述，其中優(yōu)化動(dòng)作是在滿足schema條件和樹條件時(shí)所應(yīng)執(zhí)行的動(dòng)作。為了更好地描述優(yōu)化規(guī)則，我們?cè)诘?部分定義了優(yōu)化規(guī)則的描述語言O(shè)RS，其中每條由ORS表達(dá)的優(yōu)化規(guī)則都由以上的三部分組成，本文會(huì)在第3部分詳細(xì)介紹ORS的語法和語義。

2 樹模式優(yōu)化動(dòng)作生成框架

如圖3所示為優(yōu)化動(dòng)作生成框架，將優(yōu)化規(guī)則，樹模式，XMLSchema文檔作為優(yōu)化動(dòng)作生成模塊的輸入，就會(huì)輸出優(yōu)化動(dòng)作列表。圖中實(shí)線箭頭表示數(shù)據(jù)的流向，虛線箭頭表示模塊間的調(diào)用關(guān)系，其中虛線箭頭的指向是被調(diào)用的模塊，菱形框表示輸入或輸出數(shù)據(jù)，曲線框表示XMLSchema文檔，可以看出該框架有三個(gè)輸入數(shù)據(jù)：優(yōu)化規(guī)則、樹模式、XMLSchema文檔，輸出給定樹模式優(yōu)化動(dòng)作列表。XMLSchema約束檢查模塊主要是完成優(yōu)化規(guī)則中的schema條件在XMLSchema中是否存在相應(yīng)的約束。

圖3 樹模式優(yōu)化動(dòng)作生成框架

3 優(yōu)化規(guī)則描述語言O(shè)RS

3.1ORS語法

ORS是我們定義的樹模式優(yōu)化規(guī)則的描述語言，其中ORS的語法定義如下所示：

ors:=tree_conditionsche_conditionaction

(1)

一條用ORS描述的優(yōu)化規(guī)則由tree_condition(樹條件)、sche_condition(schema條件)、action(動(dòng)作)三部分組成。

樹條件的語法定義如下：

tree_condition:=pred|!tree_condition|tree_condition∧tree_condition|tree_condition∨tree_condition|?metavar.(tree_condition)

(2)

metavar:=A|B|C|D|…|Z

(3)

tree_condition描述樹模式中具有的某種特定的子結(jié)構(gòu)，通常由基本謂詞通過布爾連接詞和存在量詞所組成，樹條件描述的是樹模式中的子結(jié)構(gòu)應(yīng)該滿足的約束條件。

(4)

constliteral:=all|seq|plus|star|choice|opt

(5)

sche_condition是CTL公式的一個(gè)子集，這些CTL表達(dá)式用來描述XMLSchema中的約束，即文獻(xiàn)[2,13]中所使用的的RPC(必然父子)、RAD(必然后代)等Schema約束。

aciton:=delLeaf(metavar)|updateChild(metavar,metavar,metavar)|addPcChild(metavar,metavar,int)|addAdChild(metavar,metavar,int)|strongBoundPc(metavar,metavar)|strongBoundAd(metavar,metavar)|weakBoundPc(metavar,metavar)|weakBoundAd(metavar,metavar)

(6)

int:=[1…9][0…9]*

(7)

action表示sche_condition和tree_condition都滿足的條件下應(yīng)執(zhí)行的優(yōu)化動(dòng)作，到目前的研究為止，我們的工具所支持的動(dòng)作有：delLeaf(literal)刪除樹模式中由literal表示的葉子結(jié)點(diǎn)；updateChild(p,x,y)即將樹模式中結(jié)點(diǎn)p的后繼結(jié)點(diǎn)x用結(jié)點(diǎn)y替換，并且要求y必須為x的唯一孩子(pc)或后代(ad)結(jié)點(diǎn)，即刪除x并用x的唯一孩子或是后代y來統(tǒng)替換x；addPcChild(p,x,i)在樹模式中結(jié)點(diǎn)p的第i個(gè)位置增加結(jié)點(diǎn)孩子結(jié)點(diǎn)x。addAdChild(p,x,i)在樹模式結(jié)點(diǎn)p的第i個(gè)位置增加后代結(jié)點(diǎn)x，并且要求x結(jié)點(diǎn)是從樹模式中的其他位置裁剪下來的分枝的根結(jié)點(diǎn)。strongBoundPc(A,B): 將B強(qiáng)綁定連接到A上，A、B之間是單線。strongBoundAd(A,B): 將B強(qiáng)綁定連接到A上，A、B之間是雙線。weakBoundPc(A,B): 將B弱綁定連接到A上，A、B之間是單線。weakBoundAd(A,B): 將B弱綁定連接到A上，A、B之間是雙線。

pred:=isLeaf(metavar)|isElem(metavar)|isOr(metavar)|isAnd(metavar)|isRoot(metavar)|isReturn(metavar)|isOneChild(metavar)|pcEdge(metavar,metavar)|adEdge(metavar,metavar)|pcEdgeD(metavar,metavar)|adEdgeD(metavar,metavar)

(8)

pred是構(gòu)成tree_condition的基本謂詞，根據(jù)謂詞變?cè)獋€(gè)數(shù)的不同，本文中將謂詞分為一元(SinglePred)謂詞和二元謂詞(BinaryPred)兩種類型。一元謂詞主要用來判斷樹模式中相應(yīng)結(jié)點(diǎn)的屬性，例如邏輯結(jié)點(diǎn)、元素結(jié)點(diǎn)、返回結(jié)點(diǎn)等。例如isAnd謂詞用來判斷樹模式中的結(jié)點(diǎn)是否為and結(jié)點(diǎn)，isOr謂詞用來判斷樹模式中的結(jié)點(diǎn)是否是or結(jié)點(diǎn)，我們將and結(jié)點(diǎn)和or結(jié)點(diǎn)稱為邏輯結(jié)點(diǎn)；isElem謂詞用來判斷當(dāng)前結(jié)點(diǎn)是否是元素結(jié)點(diǎn)，即除邏輯結(jié)點(diǎn)以外的剩余元素結(jié)點(diǎn)；isRoot謂詞用來判斷給定的結(jié)點(diǎn)是否為樹模式的根結(jié)點(diǎn)，isReturn謂詞用來判斷樹模式中的結(jié)點(diǎn)是否為返回的結(jié)點(diǎn)等。二元謂詞則通常被用來判斷結(jié)點(diǎn)間的連接邊的類型。例如謂詞pcEdge用來判斷給定樹模式中的兩個(gè)結(jié)點(diǎn)之間的連接邊是否是強(qiáng)綁定的pc關(guān)系，即用單實(shí)線表示的連接邊。而adEdge謂詞則用來判斷樹模式中給定的兩個(gè)結(jié)點(diǎn)之間的連接邊是否為強(qiáng)綁定的ad類型的邊，即用實(shí)雙線表示的邊。pcEdgeD謂詞是判斷樹模式中給定的兩個(gè)結(jié)點(diǎn)之間的連接邊是否是弱綁定的pc邊關(guān)系，即用單虛線表示的連接邊。而adEdgeD謂詞用來判斷弱綁定的ad類型的邊，即用虛雙線表示的連接邊。

3.2ORS語義

優(yōu)化規(guī)則描述語言O(shè)RS的語義是以優(yōu)化規(guī)則中出現(xiàn)的元變量中的自由變量(不受存在量詞約束的變量)進(jìn)行正確綁定為基礎(chǔ)的，即將優(yōu)化規(guī)則中的自由變量和樹模式中的某些特定結(jié)點(diǎn)進(jìn)行綁定。為了方便定義語義，我們用V表示自由變量和樹模式中的結(jié)點(diǎn)的綁定過程，用M表示給定XMLSchema的MCSG模型[2]，用TP表示樹模式的GTP模型，下面是根據(jù)ORS語言中不同的語法成分分別對(duì)ORS語言的語義進(jìn)行詳細(xì)定義。

(1)sche_condition(Schema條件)語義

sche_condition是由擴(kuò)展標(biāo)準(zhǔn)CTL后的時(shí)態(tài)邏輯公式所表示的，我們可以通過待檢查的模型來驗(yàn)證標(biāo)準(zhǔn)意義上的CTL公式的真假。但是本文中的schema條件是帶有變量的，代表樹模式中的結(jié)點(diǎn)，所以要判斷一個(gè)schema條件的真假需要依賴我們所使用的MCSG模型M[2]。將schema條件中出現(xiàn)的變量映射為相應(yīng)的樹模式中的結(jié)點(diǎn)，這個(gè)過程依賴于求值映射Vs以及樹模式TP?？紤]能夠方便地定義schema條件的語義，在定義schema條件的語義之前先定義如下的語義函數(shù)，此語義函數(shù)描述對(duì)于MCSG中特定結(jié)點(diǎn)的語義函數(shù)。

我們首先給出在給定模型中對(duì)應(yīng)于一個(gè)狀態(tài)s的語義函數(shù)。

定義2 對(duì)于某個(gè)特定的狀態(tài)，其語義函數(shù)如下：

「·?:sche_condition→((Vs×M×TP×s)→Bool)「Φ∧Ψ?(Vs,M,TP,s)=「Φ?(Vs,M,TP,s) and 「Ψ?(Vs,M,TP,s)「Φ∨Ψ?(Vs,M,TP,s)=「Φ?(Vs,M,TP,s) or 「Ψ?(Vs,M,TP,s)「Φ?(Vs,M,TP,s)=not 「Φ?(Vs,M,TP,s)「state(v)?(Vs,M,TP,s)=G.Label(Vs(v))=M.F(s)「state(constliteral)?(Vs,M,TP,s)=onstliteral=M.F(s)「EX(Φ)?(Vs,M,TP,s)=?t:t∈M.S:(s,t)∈M.R:「Φ?(Vs,M,TP,s)「E[ΦUΨ]?(Vs,M,TP,s)=?p:p∈MPaths(M,s):Until(p,Φ,Ψ)「Φ→Ψ?(Vs,M,TP,s)=「Ψ?(Vs,M,TP,s) or 「Φ?(Vs,M,TP,s)

(9)

Until(p,Φ,Ψ)成立,當(dāng)且僅當(dāng)對(duì)于MCSG中的路徑p=n0n1n2…nk，sche_condition公式Φ,Ψ：

?j:「Ψ?(V,M,TP,nj)∧?0≤i

(10)

Schema條件的語義函數(shù)如下：

定義3 sche_condition的語義函數(shù)：

「·?:sche_condition→((Vs×M×TP)→Bool)

(11)

「Φ∧Ψ?(Vs,M,TP)=「Φ?(Vs,M,TP) and 「Ψ?(Vs,M,TP)「Φ∨Ψ?(Vs,M,TP)=「Φ?(Vs,M,TP) or 「Ψ?(Vs,M,TP)「Φ?(Vs,M,TP)=not「Φ?(Vs,M,TP,s)「state(v)?(Vs,M,TP)=?s:s∈M.S:「state(v)?(Vs,M,TP,s)「state(constliteral)?(Vs,M,TP)= ?s:s∈M.S:「state(constliteral)?(Vs,M,TP,s)「EX(Φ)?(Vs,M,TP)=?s:s∈M.S:「EX(Φ)?(Vs,M,TP,s)「E[ΦUΨ]?(Vs,M,TP)= ?s:s∈M.S:「E[ΦUΨ]?(Vs,M,TP,s)「Φ→Ψ?(Vs,M,TP)= ?s:s∈M.S:「Φ→Ψ?(Vs,M,TP,s)

(12)

(2) tree_condition的語義

優(yōu)化規(guī)則中的樹條件部分是用來描述樹模式子結(jié)構(gòu)的謂詞邏輯公式，由于樹條件中也包含自由變量，因此樹條件的語義會(huì)依賴于求值映射Vt和樹模式模型TP，樹條件的語義函數(shù)如下。

定義4 tree_condition的語義函數(shù)：

?·」:tree_condition→((Vt×TP)→Bool)?Φ∨Ψ」(Vt,G)=?Φ」(Vt,G) and ?Ψ」(Vt,G)?Φ∨Ψ」(Vt,G)=?Φ」(Vt,G) or ?Ψ」(Vt,G)?Φ」(Vt,G)=not?Φ」(Vt,G)??x.Φ」(Vt,G)=?τ:τ∈QNode:?Φ」(Vt[xτ],G)?pred(x)」(Vt,G)=‖pred‖((x),Vt,G)?pred(x,y)」(Vt,G)=‖pred‖((x,y),Vt,G)

(13)

定義5pred謂詞的語義：

pred是用來描述樹模式中的特定子結(jié)構(gòu)的謂詞，這些謂詞會(huì)含有參數(shù)，我們根據(jù)參數(shù)的個(gè)數(shù)(1個(gè)，2個(gè)，…n個(gè))將謂詞分為一元謂詞，二元謂詞，…，n元謂詞。謂詞把由自由變量所代表樹模式結(jié)點(diǎn)和樹模型TP以及相應(yīng)的求值映射Vt映射為布爾值，因此n元謂詞的語義函數(shù)可以用下面的公式來表示：

‖·‖:predn→((QNoden×Vt×TP)→Bool)

(14)

‖isLeaf‖(x,Vt,TP)=?n:n∈QNode,etype∈{″S-PC″,″S-AD″,″D-PC″,″D-AD″} :(Vt(x),etype,n)?TP.TEdge‖isOr‖(x,Vt,TP)=TP.Type(Vt(x))=″OR″‖isAnd‖(x,Vt,TP)=TP.Type(Vt(x))=″AND″‖isElem‖(x,Vt,TP)=TP.Type(Vt(x))=″QUERY″‖isReturn‖(x,Vt,TP)=Vt(x)∈TP.Return‖isRoot‖(x,Vt,TP)=Vt(x)=TP.Root‖pcEdge‖(x,y,Vt,TP)=(Vt(x),″S-PC″,Vt(y)) ∈TP.TEdge‖adEdge‖(x,y,Vt,TP)= (Vt(x),″S-AD″,Vt(y))∈TP.TEdge‖isOneChild‖(x,Vt,TP)=?m∈TP.TNode,n∈TP.TNode,etype∈{″S-PC″,″S-AD″, ″D-PC″,″D-AD″}, (Vt(x),etype,m)∈TP.Edgeand(Vt(x),etype,n)∈TP.Edge→(m=n)

(15)

(3)action的語義

優(yōu)化規(guī)則的action部分是用來表達(dá)在滿足schema條件和樹條件的情況下，樹模式是如何被優(yōu)化的。同理，action以求值映射Va為基礎(chǔ)，優(yōu)化給定的樹模式TP，優(yōu)化樹模式之后會(huì)產(chǎn)生新的樹模式，因此我們定義action的語義函數(shù)如下：

定義6action的語義函數(shù)：

?·」:action→(Va×TP→TP)

(16)

目前，優(yōu)化規(guī)則描述語言O(shè)RS支持如下幾種的對(duì)于樹模式上的優(yōu)化操作，即刪除由某個(gè)literal代表的葉子結(jié)點(diǎn)，在某個(gè)結(jié)點(diǎn)的特定位置上增加結(jié)點(diǎn)，以及更新結(jié)點(diǎn)，強(qiáng)綁定連接和弱綁定連接(都分別包含PC關(guān)系和AD關(guān)系的綁定)。

刪除葉子節(jié)點(diǎn)delLeaf(x)，葉子結(jié)點(diǎn)是樹模式中沒有子孫后代的結(jié)點(diǎn)，如果要?jiǎng)h除某個(gè)葉子結(jié)點(diǎn)前提是該結(jié)點(diǎn)并不是返回結(jié)點(diǎn)。是否是返回結(jié)點(diǎn)這些條件都會(huì)在樹條件中進(jìn)行嚴(yán)格判斷的，執(zhí)行的優(yōu)化動(dòng)作都是在滿足schema條件和樹條件的情況下才會(huì)執(zhí)行的。當(dāng)我們刪除葉子結(jié)點(diǎn)x后，相應(yīng)地GTP模型TP也會(huì)做出改變。例如TNode會(huì)減少刪除的葉子結(jié)點(diǎn)，跟x相連的邊也會(huì)被刪除，對(duì)應(yīng)的集合TEdge也會(huì)減少，Type和Label定義的都是某個(gè)結(jié)點(diǎn)到其自身字符串的映射，因此也應(yīng)作相應(yīng)的修改，Parent(x)表示給定結(jié)點(diǎn)x的父結(jié)點(diǎn)。

增加結(jié)點(diǎn)addPcChild(p,x,i)、addAdChild(p,x,i)，表示在結(jié)點(diǎn)p的第i個(gè)位置增加結(jié)點(diǎn)x，其中這兩個(gè)動(dòng)作的p、x之間的邊類型分別為pc和ad關(guān)系。在樹模式優(yōu)化的操作中，在給某個(gè)結(jié)點(diǎn)增加其他結(jié)點(diǎn)的情況往往是從樹模式的其他子結(jié)構(gòu)中裁剪而來的，而在樹模式中某個(gè)結(jié)點(diǎn)下增加一個(gè)全新的結(jié)點(diǎn)的情況基本是不可能發(fā)生的。

更新孩子結(jié)點(diǎn)操作，updateChild(p,x,y)，用y把結(jié)點(diǎn)p的孩子x替換，這個(gè)操作的前提是結(jié)點(diǎn)y必須是結(jié)點(diǎn)x唯一的孩子結(jié)點(diǎn)，x和y之間的連接邊可以是pc關(guān)系也可以是ad關(guān)系。

strongBoundPc(A,B): 將結(jié)點(diǎn)B強(qiáng)綁定連接到結(jié)點(diǎn)A上，A、B之間是單線即父子關(guān)系。strongBoundAd(A,B): 將結(jié)點(diǎn)B強(qiáng)綁定連接到結(jié)點(diǎn)A上，A、B之間是雙線即子孫后代關(guān)系。weakBoundPc(A,B): 將結(jié)點(diǎn)B弱綁定連接到結(jié)點(diǎn)A上，A、B之間是單線，即父子關(guān)系。weakBoundAd(A,B): 將B弱綁定連接到A上，A、B之間是雙線。

(4)ors規(guī)則語義

由于我們要對(duì)整個(gè)樹模式進(jìn)行優(yōu)化，因此需要計(jì)算出所有滿足樹條件的求值映射V，保證schema條件和樹條件兩個(gè)語義函數(shù)都滿足，然后才能執(zhí)行優(yōu)化動(dòng)作action。我們求得的求值映射V是個(gè)集合，對(duì)于結(jié)合V中的任一v，ors都會(huì)將樹模式從一種形式變換到另一種形式。對(duì)于不同的v，會(huì)對(duì)應(yīng)到樹模式中不同的部分，每個(gè)部分在執(zhí)行相應(yīng)的優(yōu)化動(dòng)作后，都將會(huì)把樹模式從舊的形式變?yōu)閮?yōu)化后的新的形式。在這種情況下，我們可以用樹模式組成的有序?qū)肀硎?，即形?TP,TP)的形式。對(duì)于每一個(gè)這樣的有序?qū)Χ紩?huì)對(duì)應(yīng)一個(gè)映射函數(shù)v，為了能表達(dá)這樣的有序?qū)λM成的集合，我們引入部分求值函數(shù)P。部分求值函數(shù)也會(huì)把優(yōu)化規(guī)則中的樹條件部分中的自由變量映射到樹模式中的結(jié)點(diǎn)，而于前面介紹的求值映射函數(shù)的區(qū)別在于：部分求值函數(shù)對(duì)于樹條件中的某些自由變量是無定義的。假設(shè)有如下的求值函數(shù)集合{v1,v2,…,vn}，由于求值映射函數(shù)是將樹條件中的自由變量映射為樹模式中的特定結(jié)點(diǎn)，也就是說對(duì)于求值映射集合中的映射的定義域是相同的都為樹條件中的自由變量集合。對(duì)于這個(gè)定義域中的任一自由變量x來說，如果集合中所有的求值函數(shù)都將自由變量x映射到樹模式中的某個(gè)相同的結(jié)點(diǎn)node時(shí)，那么我們就稱P(x)=node；反之，如果自變量x在不同的求值函數(shù)的函數(shù)值對(duì)應(yīng)樹模式中的不同的結(jié)點(diǎn)時(shí)，我們就說P(x)是沒有定義的。因此，我們可以將ORS的語義函數(shù)定義如下：

定義7ors的語義函數(shù)：

「·?:ors→(P×TP×M→2(TP→TP))

(17)

其中，2TP→TP代表TP—>TP的冪集。

「tree_conditionschea_conditionaction?(P,TP,M)=

{(x,「action?(σ,x))|「sche_condition?(σ,TP)and

「tree_condition?(σ,TP)andσ↑dom(P)=P}

(18)

式中，σ↑dom(P)=P表示的是求值函數(shù)σ在部分求值函數(shù)P的定義域上的函數(shù)值與P保持一致。

3.3ORS優(yōu)化規(guī)則舉例

以下將每條優(yōu)化規(guī)則用ORS語言進(jìn)行描述的實(shí)例，其中的每一條實(shí)例都是按照優(yōu)化規(guī)則的定義即將tree_condition，sche_condition，action的形式分成了三部分分別表示。

規(guī)則1 在給定樹模式中的A、B兩個(gè)結(jié)點(diǎn)，它們之間用單線連接即A與B之間是PC關(guān)系，且A、B兩個(gè)結(jié)點(diǎn)類型都是元素結(jié)點(diǎn)，并且B是葉子結(jié)點(diǎn)(即沒有子孫后代的結(jié)點(diǎn))；如果A、B兩個(gè)結(jié)點(diǎn)的名字在XMLSchema中滿足必然孩子約束[2]，因此，就可以刪除樹模式中的B結(jié)點(diǎn)：

用ORS語言所表達(dá)的上述規(guī)則如下：

pcEdge(A,B)∧isElem(A)∧isElem(B)∧isLeaf(B)

∧!isReturn(B)

RPC(A,B)

delLeafB

其中，將schema條件用CTL表示為：

RPC(A,B)=(state(A))→

EX(E[(state(seq)∨

state(plus)∨state(all))Ustate(B)])

規(guī)則2 樹模式中的A、B兩個(gè)結(jié)點(diǎn)，A、B之間存在一個(gè)邏輯結(jié)點(diǎn)“and”，A、B結(jié)點(diǎn)類型都是元素結(jié)點(diǎn)，并且A、L，B、L兩對(duì)結(jié)點(diǎn)之間都滿足父子關(guān)系[2]，B是樹模式的一個(gè)葉子結(jié)點(diǎn)；如果有A、B的結(jié)點(diǎn)名字在XMLSchema中滿足必然孩子的約束成立，那么我們就可以將樹模式中的B結(jié)點(diǎn)刪除。

ORS表示如下：

?L(pcEdge(A,L)∧pcEdge(L,B)?∧isAnd(L)∧isLeaf(B)∧isElem(B)?∧isElem(A))∧！isReturn(B)

RPC(A,B)

delLeafB

規(guī)則3 與規(guī)則2相似，不同點(diǎn)在于A與B之間的邏輯結(jié)點(diǎn)替換為“or”：

ORS表示如下：

?L(pcEdge(A,L)?∧pcEdge(L,B)∧isOr(L)∧isLeaf(B)∧isElem(B)∧isElem(A))∧！isReturn(B)

RPC(A,B)

delLeafB

規(guī)則4 該規(guī)則與1類似，不同的是樹模式的A、B兩個(gè)結(jié)點(diǎn)之間是后代關(guān)系，并且A、B的名字間在Schema中滿足必然的后代關(guān)系：

ORS表示如下：

adEdge(A,B)∧isElem(A)∧isElem(B)∧isLeaf(B)∧！isReturn(B)

RAD(A,B)

delLeafB

將schema條件用CTL表示為如下形式：

RAD(A,B)=(state(A))→EX(E[(!state(opt)∨!state(star)∨!state(choice))Ustate(B)])

規(guī)則5 樹模式中的A、B、C三個(gè)結(jié)點(diǎn)，C和A、A和B，兩對(duì)結(jié)點(diǎn)之間分別用雙線連接(即ad關(guān)系)，并且A、B、C三個(gè)結(jié)點(diǎn)都為元素結(jié)點(diǎn)，B為A的唯一孩子結(jié)點(diǎn)；如果在XML Schema中A、B兩個(gè)結(jié)點(diǎn)的名字之間滿足必然父母關(guān)系，那么我們可以刪除樹模式中的A結(jié)點(diǎn)，并將B結(jié)點(diǎn)作為C結(jié)點(diǎn)的孩子結(jié)點(diǎn)：

ORS表示如下：

adEdge(C,A)∧adEdge(A,B)∧isElem(A)∧isElem(B)∧isElem(C)∧isOneChild(A)∧！isReturn(B)

PRAD(A,B)

UpdateChild(C,A,B)

規(guī)則6 樹模式中的A、B、C三個(gè)結(jié)點(diǎn)，A和B、B和C，兩對(duì)結(jié)點(diǎn)之間都滿足pc關(guān)系，A、B、C三個(gè)結(jié)點(diǎn)為元素結(jié)點(diǎn)，且C結(jié)點(diǎn)是樹模式中的葉子結(jié)點(diǎn)；如果在XML Schema中，所有由A的所代表的結(jié)點(diǎn)所能到達(dá)的B結(jié)點(diǎn)都有必然有孩子結(jié)點(diǎn)C的話，那么我們可以將C結(jié)點(diǎn)刪除。

ORS表示如下：

pcEdge(A,B)∧pcEdge(B,C)∧isElem(A)∧isElem(B)

∧isElem(B)∧isLeaf(C)∧！isReturn(C)

RPCPATH(A,B,C)

delLeafC

規(guī)則7 同規(guī)則6，不同的是用ad關(guān)系替換其中的pc關(guān)系。

ORS表示如下：

adEdge(A,B)∧adEdge(B,C)∧isElem(A)∧isElem(B)∧isElem(C)∧isLeaf(C)∧！isReturn(C)

RADPATH(A,B,C)

delLeafC

規(guī)則8 樹模式中的A、B兩個(gè)結(jié)點(diǎn)，他們之間是弱綁定PC關(guān)系，且A、B兩個(gè)結(jié)點(diǎn)的類型都是元素結(jié)點(diǎn)，B為葉子結(jié)點(diǎn)且是返回結(jié)點(diǎn)；如果A、B的結(jié)點(diǎn)名字在XML Schema中有必然孩子關(guān)系，那么可以將樹模式中的B結(jié)點(diǎn)強(qiáng)綁定連接到A結(jié)點(diǎn)上：

ORS表示如下：

pcEdgeD(A,B)∧isElem(A)∧isElem(B)∧isLeaf(B)

∧isReturn(B)

RPC(A,B)

strongBoundPc(A,B)

當(dāng)然這里列舉的這些優(yōu)化規(guī)則并不是全部的，只是針對(duì)幾種典型的Schema特征(本文中Schema特征與Schema約束為同一概念)分別進(jìn)行了舉例。在實(shí)際工作當(dāng)中，可以根據(jù)樹模式的特點(diǎn)以及需要的Schema特征來寫出更多的優(yōu)化規(guī)則。

4 工具實(shí)現(xiàn)

4.1 系統(tǒng)實(shí)現(xiàn)流程

樹模式優(yōu)化動(dòng)作生成的實(shí)現(xiàn)流程如圖4所示。

流程中，平行四邊形表示輸入或輸出數(shù)據(jù)，矩形框表示流程中的處理模塊，實(shí)線箭頭表示數(shù)據(jù)的流向，虛線箭頭表示模塊間的調(diào)用關(guān)系，箭頭的指向是被調(diào)用的模塊。每個(gè)處理模塊左上角的文字是該模塊用到的輔助工具包。

根據(jù)圖4所示的流程，下面對(duì)幾個(gè)主要的模塊進(jìn)行介紹：

(1) 樹模式優(yōu)化模塊

即最后會(huì)輸出優(yōu)化動(dòng)作列表的子模塊。此模塊接受變量映射的結(jié)果和schema條件的語法樹形式，調(diào)用特征提取模塊完成優(yōu)化動(dòng)作列表輸出的任務(wù)。

(2) 約束檢查模塊

此模塊用于檢查Schema約束。將優(yōu)化規(guī)則中的schema條件和MCSG模型作為輸入，其中MCSG模型是用Xerces C++由Schema文檔轉(zhuǎn)換而來的，從而檢查相應(yīng)的約束是否滿足。

(3) 變量映射模塊

是將優(yōu)化規(guī)則中樹條件中的自由變量映射到樹模式中的具體變量的一個(gè)過程，主要使用CUDD[11-12]的相關(guān)功能完成到優(yōu)化規(guī)則樹條件到有序二叉決策圖(OBDD)的轉(zhuǎn)換，轉(zhuǎn)換完成后的結(jié)果即OBDD(代表布爾函數(shù))的每個(gè)最小項(xiàng)代表了變量映射的一個(gè)(或多個(gè))結(jié)果。

(4) 詞法分析模塊

是對(duì)由ORS表達(dá)的優(yōu)化規(guī)則進(jìn)行詞法分析的子模塊。詞法分析模塊的實(shí)現(xiàn)是以開源的Flex工具為基礎(chǔ)的。

(5) 語法分析模塊

此模塊是對(duì)ORS表達(dá)的優(yōu)化規(guī)則進(jìn)行語法分析的子模塊。此模塊的實(shí)現(xiàn)借助了工具Bison，通過建立ORS的語法樹，該模塊實(shí)現(xiàn)依賴詞法分析子模塊。

(6) Schema圖轉(zhuǎn)換模塊

利用工具Xerces C++完成由XML Schema文檔到MCSG模型的轉(zhuǎn)換。

總的來看，工具的輸入為XML Schema文檔，由ORS表示的優(yōu)化規(guī)則，待查詢的樹模式GTP，經(jīng)過一系列操作之后輸出對(duì)應(yīng)樹模式在特定優(yōu)化規(guī)則下的優(yōu)化動(dòng)作列表。

圖4 樹模式優(yōu)化動(dòng)作生成實(shí)現(xiàn)流程

4.2 優(yōu)化動(dòng)作輸出舉例

對(duì)于前文中如圖2所示的GTP模型：

其中橢圓內(nèi)的字符串為結(jié)點(diǎn)的名字，結(jié)點(diǎn)附近的數(shù)字是結(jié)點(diǎn)的編號(hào)，結(jié)點(diǎn)之間的單線表示結(jié)點(diǎn)之間的PC關(guān)系，雙線代表結(jié)點(diǎn)之間的祖先后代關(guān)系，標(biāo)星號(hào)的結(jié)點(diǎn)為返回結(jié)點(diǎn)。

如果我們能從對(duì)應(yīng)XML Schema文檔中得到如下結(jié)果：結(jié)點(diǎn)3和結(jié)點(diǎn)6、結(jié)點(diǎn)3和結(jié)點(diǎn)7之間、結(jié)點(diǎn)4和結(jié)點(diǎn)8之間存在必然的父子約束，結(jié)點(diǎn)3和結(jié)點(diǎn)5之間存在必然的子孫后代約束。那么我們對(duì)樹模式進(jìn)行如下的幾步優(yōu)化，會(huì)得到相應(yīng)結(jié)果。

針對(duì)規(guī)則1：

工具輸出截圖如下：

上述截圖中的結(jié)果表示刪除結(jié)點(diǎn)編號(hào)為8和結(jié)點(diǎn)編號(hào)為6的結(jié)點(diǎn)，即刪除title結(jié)點(diǎn)和city結(jié)點(diǎn)。因?yàn)閺腦ML Schema文檔中可知結(jié)點(diǎn)4和結(jié)點(diǎn)8、結(jié)點(diǎn)3和結(jié)點(diǎn)6之間存在必然的父子關(guān)系，根據(jù)必然父子關(guān)系的描述[2]，我們可以知道，在符合這個(gè)XML Schema文檔定義的XML文檔中，所有的shipto元素都必然會(huì)有city孩子元素，所有的item元素必然會(huì)有title子元素。而我們的GTP所示要求shipto結(jié)點(diǎn)有city子節(jié)點(diǎn)，item結(jié)點(diǎn)有title子節(jié)點(diǎn)，并且shipto結(jié)點(diǎn)和city結(jié)點(diǎn)之間以及item結(jié)點(diǎn)和title結(jié)點(diǎn)之間存在必然的父子關(guān)系，因此可以將shipto結(jié)點(diǎn)的孩子結(jié)點(diǎn)city結(jié)點(diǎn)以及item的孩子結(jié)點(diǎn)title結(jié)點(diǎn)裁剪掉。因?yàn)樵诶又械腉TP中根本就是冗余的查詢。

GTP模型在進(jìn)行上述優(yōu)化后變?yōu)槿鐖D5所示。

圖5 采用規(guī)則1優(yōu)化后的GTP模型

如果繼續(xù)采用規(guī)則4對(duì)上述GTP進(jìn)行優(yōu)化，工具會(huì)得到如下結(jié)果：

此次優(yōu)化的分析同采用優(yōu)化規(guī)則1的優(yōu)化，只不過將結(jié)點(diǎn)之間的父親孩子關(guān)系轉(zhuǎn)換為子孫后代關(guān)系，因?yàn)樵赬ML Schema中結(jié)點(diǎn)3和結(jié)點(diǎn)5之間存在必然的子孫后代的關(guān)系[2]。即在符合此XML Schema的XML文檔中shipto元素必會(huì)有country后代元素，此GTP查詢中要求shipto元素必須有country子孫元素也同樣為冗余查詢，故在這個(gè)GTP查詢中可刪除country結(jié)點(diǎn)。

GTP模型優(yōu)化為如圖6所示。

圖6 采用規(guī)則4優(yōu)化后的GTP

對(duì)上述的GTP繼續(xù)采用優(yōu)化規(guī)則8進(jìn)行優(yōu)化：工具會(huì)給出如下的輸出結(jié)果：

在樹模式查詢中一個(gè)XML文檔實(shí)例中的元素應(yīng)該滿足GTP的所有的強(qiáng)綁定，而不要求必須滿足弱綁定。強(qiáng)綁定可以有過濾更多的結(jié)點(diǎn)，使結(jié)果集更小，從而有利于提高查詢效率。盡可能地把弱綁定轉(zhuǎn)化為強(qiáng)綁定，是XML查詢處理中一個(gè)很大的優(yōu)化點(diǎn)[14]。

優(yōu)化后的樹模型如圖7所示。

圖7 采用規(guī)則8優(yōu)化后的GTP

從上面的優(yōu)化可以知道，本文中的方法在給定優(yōu)化規(guī)則，樹模式的GTP模型以及特定的schema特征條件就可以得到優(yōu)化動(dòng)作列表。

工具的實(shí)現(xiàn)環(huán)境：硬件環(huán)境：ThinkVision，軟件環(huán)境：操作系統(tǒng)：RedHat Linux，編譯器和編輯器：GCC、Vim。

5 結(jié) 語

針對(duì)一種算法只解決一種具有某種特定特點(diǎn)的樹模式優(yōu)化方案的缺陷，本文提出了一個(gè)完整的、統(tǒng)一的解決樹模式優(yōu)化動(dòng)作的生成問題的方案。本文所提出的方案以時(shí)態(tài)邏輯、謂詞邏輯、模型檢查等形式化的方法為基礎(chǔ)，實(shí)現(xiàn)了基于優(yōu)化規(guī)則的樹模式優(yōu)化動(dòng)作自動(dòng)生成工具。

具體地提出了一種描述優(yōu)化樹模式的優(yōu)化規(guī)則描述語言-ORS。是在考察了常見的XML Schema特征的時(shí)態(tài)邏輯公式表示和樹模式優(yōu)化方法的前提下，以時(shí)態(tài)邏輯和謂詞邏輯為基礎(chǔ)，提出了ORS語言。ORS由樹條件(tree_condition)、schema條件(sche_condition)、和action(動(dòng)作)三部分組成，ORS具有足夠的表達(dá)能力，表示基于XML Schema的樹模式優(yōu)化的常見規(guī)則。

本文的方案是基于優(yōu)化規(guī)則的優(yōu)化動(dòng)作自動(dòng)生成。由于本文將多種類的樹模式的優(yōu)化統(tǒng)一于同一個(gè)優(yōu)化框架之下，較之前一個(gè)算法只能優(yōu)化一種類型的樹模式的方法增加了通用性，此種方案增加了預(yù)處理的成本，與專門針對(duì)特定的schema約束的算法相比，存在性能下降的問題；另外，在描述優(yōu)化規(guī)則中的schema條件時(shí)，到目前僅支持判斷名字的謂詞。后續(xù)工作中，我們打算在現(xiàn)在方案的基礎(chǔ)上，擴(kuò)充其他schema條件中可能涉及到的謂詞，例如，孩子順序的謂詞、孩子結(jié)點(diǎn)個(gè)數(shù)的謂詞、有關(guān)Schema元素結(jié)點(diǎn)的屬性謂詞等，那么可能對(duì)樹模式進(jìn)行更徹底的優(yōu)化。并且繼續(xù)擴(kuò)充時(shí)態(tài)邏輯公式，以支持更多的Schema中的約束信息。

[1] Li H,Liao H S,Su H.Optimize Twig Query Pattern Based on XML Schema[J].Journal of Software,2013,8(6):1479-1486.

[2] 劉科,楊紅麗,廖湖聲,等.基于模型檢查的XML Schema特征提取[C]//2012中國計(jì)算機(jī)大會(huì),2012:160-164.

[3] AmerYahia S,Cho S R,Lakshmanan L V S,et al.Tree pattern query minimization[J].The VLDB Journal The International Journal on Very Large Data Bases,2002,11(4):315-331.

[4] Le D X T,Maghaydah M,Orgun M A,et al.Optimization of XML Queries by Using Semantics in XML Schemas and the Document Structure[J].Lecture Notes in Computer Science,2013,8180:343-353.

[5] Xu X,Feng Y,Wang F.Efficient Processing of XML Twig Queries with All Predicates[C]//2009 Eigth IEEE/ACIS International Conference on Computer and Information Science.IEEE Computer Society,2009:457-462.

[6] D Bujji Babu.XML Twig Pattern Matching Algorithms and Query Processing[J/OL].IJERT May-2012,1(3): 1-6 [2015-12-28].http://www.ijert.org/view-pdf/169/xml-twig-pattern-matching-algorithms-and-query-processing.

[7] Wu H,Lin C,Ling T W,et al.Processing XML Twig Pattern Query with Wildcards[M]//Database and Expert Systems Applications.Springer Berlin Heidelberg,2012:326-341.

[8] 畢鑫,王國仁,趙相國,等.XML數(shù)據(jù)中Twig查詢處理與優(yōu)化技術(shù)研究綜述[J].計(jì)算機(jī)科學(xué)與探索,2013(9):769-782.

[9] Jagadish H V,Lakshmanan L V S,Srivastava D,et al.TAX:A Tree Algebra for XML[J].Lecture Notes in Computer Science,2001,2397:149-164.

[10] Goranko V.Logic in Computer Science:Modelling and Reasoning About Systems[J].Ceskoslovenská Oftalmologie,2004,29(4):295-7.

[11] Somenzi F.CUDD:CU decision diagram package-release 2.4.0[D].Department of Electrical and Computer Engineering-University of Colorado at Boulder,1998.

[12] Schreiber E L.A CUDD Tutorial[DB/OL].2008.http://docslide.us/documents/schreiber-cudd-tutorial.html.

[13] 劉科,楊紅麗,趙瑞芳,等.XML Schema特征提取算法[J].計(jì)算機(jī)科學(xué),2015,42(11A):438-443.

[14] 孟小峰,羅道鋒,蔣瑜,等.QreintXA:一種有效的XQuery查詢代數(shù)[J].軟件學(xué)報(bào),2004,15(11):1648-1660.

XML TREE MODEL OPTIMIZATION OPERATION GENERATING BASEDON MODEL CHECKING

Zhao Ruifang Liu Ke Yang Hongli Liao Husheng

(BeijingUniversityofTechnology,Beijing100124,China)

For the core operation of XML data query, tree model query, a general method based on the constraints in XML Schema is proposed. This method presents a unified optimization rule to describe the syntax and semantic of the language ORS. The optimization rule of describing ORS includes the description of the tree model condition, the description of XML Schema condition and the action that should be output when meet the first two conditions. According to the optimization rules describing ORS and the tree model to be processed, the system will output the optimized actions automatically. On the one hand, this method simplifies the process of optimizing the cutting process of tree model. On the other hand, model checking technique is applied to the XML tree model query optimization. The constraint conditions of the optimization rules are described by the temporal logic formula. Using the model checking algorithm to extract the constraints of XML Schema, and the strict syntax and semantics definition of ORS ensures the correctness of the generated optimal actions.

Tree model optimization ORS XML schema Model checking

2015-12-25。趙瑞芳，碩士生，主研領(lǐng)域：XML樹模式查詢優(yōu)化。劉科，碩士。楊紅麗，副教授。廖湖聲，教授。

TP391

A

10.3969/j.issn.1000-386x.2017.03.008