基于模型檢查的XML樹模式優化動作生成

趙瑞芳 劉 科 楊紅麗 廖湖聲

(北京工業大學 北京 100124)

基于模型檢查的XML樹模式優化動作生成

趙瑞芳 劉 科 楊紅麗 廖湖聲

(北京工業大學 北京 100124)

針對XML數據查詢的核心操作-樹模式查詢，提出基于XML Schema約束來優化樹模式查詢的方法。該方法提出了統一的優化規則描述語言ORS的語法與語義。ORS描述的優化規則中包括對樹模式條件的描述、對XML Schema條件的描述以及在滿足前兩個條件下應該輸出的動作。根據ORS語言描述的優化規則以及待處理的樹模式，系統會自動輸出該樹模式的優化動作。該方法一方面簡化了樹模式優化的過程，另一方面把模型檢查技術運用到XML樹模式查詢優化上，利用時態邏輯公式描述優化規則中的約束條件，利用模型檢查的方法提取XML Schema的約束，對ORS語法和語義的嚴格定義確保了生成的優化動作的正確性。

樹模式優化 ORS XML Shema 模型檢查

0 引 言

XML以其簡單易用性，迅速在互聯網內得到了廣泛的應用。為了推動XML數據查詢和處理的標準化，國際萬維網組織W3C發展了XQuery語言作為XML數據的查詢語言。XQuery語言采用XPath表達式定位數據，它對于XML的作用類似于SQL對于關系數據庫的作用[1]。XQuery作為其查詢語言，近年來也受到了大量的關注。而樹模式查詢作為XQuery查詢的核心操作，樹模式查詢的優化也受到了廣大學者的關注。他們或是提出更加高效的算法，或是應用更加有效地數據結構來優化查詢。

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

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

1 樹模式定義

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

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

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

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

TNode：由樹模式中各個結點id所組成的集合，每個不同的id都標識樹模式中的唯一一個結點；

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

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

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

Root：表示樹模式的根結點，是TNode中的元素。

Return：是TNode的一個子集，代表樹模式中全部的返回結點。

下面我們將通過一個樹模式的例子以及該樹模式對應的GTP模型進行說明。

例如圖1中樹模式舉例，單線代表結點之間的父子(PC)關系，雙線代表結點之間的子孫后代關系，實線表示強綁定的關系，虛線表示弱綁定的關系即可有可無的約束，標注星號的結點表示樹模式查詢的返回結點，結點內的字符串表示對應結點的標識。圖2是圖1中樹模式所對應的GTP模型，其中結點旁邊的標識表示對應結點的ID。

圖1 樹模式舉例

圖2 樹模式對應的GTP

根據GTP的形式化定義可知圖1中樹模式對應的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}

我們將樹模式的優化方法描述為樹模式的優化規則，而每一條優化規則都包括：對XMLSchema特征的描述(稱之為schema條件)、對樹模式條件的描述(即樹模式子結構所滿足的條件稱之為樹條件)，以及對優化動作的描述，其中優化動作是在滿足schema條件和樹條件時所應執行的動作。為了更好地描述優化規則，我們在第3部分定義了優化規則的描述語言ORS，其中每條由ORS表達的優化規則都由以上的三部分組成，本文會在第3部分詳細介紹ORS的語法和語義。

2 樹模式優化動作生成框架

如圖3所示為優化動作生成框架，將優化規則，樹模式，XMLSchema文檔作為優化動作生成模塊的輸入，就會輸出優化動作列表。圖中實線箭頭表示數據的流向，虛線箭頭表示模塊間的調用關系，其中虛線箭頭的指向是被調用的模塊，菱形框表示輸入或輸出數據，曲線框表示XMLSchema文檔，可以看出該框架有三個輸入數據：優化規則、樹模式、XMLSchema文檔，輸出給定樹模式優化動作列表。XMLSchema約束檢查模塊主要是完成優化規則中的schema條件在XMLSchema中是否存在相應的約束。

圖3 樹模式優化動作生成框架

3 優化規則描述語言ORS

3.1ORS語法

ORS是我們定義的樹模式優化規則的描述語言，其中ORS的語法定義如下所示：

ors:=tree_conditionsche_conditionaction

(1)

一條用ORS描述的優化規則由tree_condition(樹條件)、sche_condition(schema條件)、action(動作)三部分組成。

樹條件的語法定義如下：

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描述樹模式中具有的某種特定的子結構，通常由基本謂詞通過布爾連接詞和存在量詞所組成，樹條件描述的是樹模式中的子結構應該滿足的約束條件。

(4)

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

(5)

sche_condition是CTL公式的一個子集，這些CTL表達式用來描述XMLSchema中的約束，即文獻[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都滿足的條件下應執行的優化動作，到目前的研究為止，我們的工具所支持的動作有：delLeaf(literal)刪除樹模式中由literal表示的葉子結點；updateChild(p,x,y)即將樹模式中結點p的后繼結點x用結點y替換，并且要求y必須為x的唯一孩子(pc)或后代(ad)結點，即刪除x并用x的唯一孩子或是后代y來統替換x；addPcChild(p,x,i)在樹模式中結點p的第i個位置增加結點孩子結點x。addAdChild(p,x,i)在樹模式結點p的第i個位置增加后代結點x，并且要求x結點是從樹模式中的其他位置裁剪下來的分枝的根結點。strongBoundPc(A,B): 將B強綁定連接到A上，A、B之間是單線。strongBoundAd(A,B): 將B強綁定連接到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是構成tree_condition的基本謂詞，根據謂詞變元個數的不同，本文中將謂詞分為一元(SinglePred)謂詞和二元謂詞(BinaryPred)兩種類型。一元謂詞主要用來判斷樹模式中相應結點的屬性，例如邏輯結點、元素結點、返回結點等。例如isAnd謂詞用來判斷樹模式中的結點是否為and結點，isOr謂詞用來判斷樹模式中的結點是否是or結點，我們將and結點和or結點稱為邏輯結點；isElem謂詞用來判斷當前結點是否是元素結點，即除邏輯結點以外的剩余元素結點；isRoot謂詞用來判斷給定的結點是否為樹模式的根結點，isReturn謂詞用來判斷樹模式中的結點是否為返回的結點等。二元謂詞則通常被用來判斷結點間的連接邊的類型。例如謂詞pcEdge用來判斷給定樹模式中的兩個結點之間的連接邊是否是強綁定的pc關系，即用單實線表示的連接邊。而adEdge謂詞則用來判斷樹模式中給定的兩個結點之間的連接邊是否為強綁定的ad類型的邊，即用實雙線表示的邊。pcEdgeD謂詞是判斷樹模式中給定的兩個結點之間的連接邊是否是弱綁定的pc邊關系，即用單虛線表示的連接邊。而adEdgeD謂詞用來判斷弱綁定的ad類型的邊，即用虛雙線表示的連接邊。

3.2ORS語義

優化規則描述語言ORS的語義是以優化規則中出現的元變量中的自由變量(不受存在量詞約束的變量)進行正確綁定為基礎的，即將優化規則中的自由變量和樹模式中的某些特定結點進行綁定。為了方便定義語義，我們用V表示自由變量和樹模式中的結點的綁定過程，用M表示給定XMLSchema的MCSG模型[2]，用TP表示樹模式的GTP模型，下面是根據ORS語言中不同的語法成分分別對ORS語言的語義進行詳細定義。

(1)sche_condition(Schema條件)語義

sche_condition是由擴展標準CTL后的時態邏輯公式所表示的，我們可以通過待檢查的模型來驗證標準意義上的CTL公式的真假。但是本文中的schema條件是帶有變量的，代表樹模式中的結點，所以要判斷一個schema條件的真假需要依賴我們所使用的MCSG模型M[2]。將schema條件中出現的變量映射為相應的樹模式中的結點，這個過程依賴于求值映射Vs以及樹模式TP。考慮能夠方便地定義schema條件的語義，在定義schema條件的語義之前先定義如下的語義函數，此語義函數描述對于MCSG中特定結點的語義函數。

我們首先給出在給定模型中對應于一個狀態s的語義函數。

定義2 對于某個特定的狀態，其語義函數如下：

「·?: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,Φ,Ψ)成立,當且僅當對于MCSG中的路徑p=n0n1n2…nk，sche_condition公式Φ,Ψ：

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

(10)

Schema條件的語義函數如下：

定義3 sche_condition的語義函數：

「·?: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的語義

優化規則中的樹條件部分是用來描述樹模式子結構的謂詞邏輯公式，由于樹條件中也包含自由變量，因此樹條件的語義會依賴于求值映射Vt和樹模式模型TP，樹條件的語義函數如下。

定義4 tree_condition的語義函數：

?·」: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是用來描述樹模式中的特定子結構的謂詞，這些謂詞會含有參數，我們根據參數的個數(1個，2個，…n個)將謂詞分為一元謂詞，二元謂詞，…，n元謂詞。謂詞把由自由變量所代表樹模式結點和樹模型TP以及相應的求值映射Vt映射為布爾值，因此n元謂詞的語義函數可以用下面的公式來表示：

‖·‖: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的語義

優化規則的action部分是用來表達在滿足schema條件和樹條件的情況下，樹模式是如何被優化的。同理，action以求值映射Va為基礎，優化給定的樹模式TP，優化樹模式之后會產生新的樹模式，因此我們定義action的語義函數如下：

定義6action的語義函數：

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

(16)

目前，優化規則描述語言ORS支持如下幾種的對于樹模式上的優化操作，即刪除由某個literal代表的葉子結點，在某個結點的特定位置上增加結點，以及更新結點，強綁定連接和弱綁定連接(都分別包含PC關系和AD關系的綁定)。

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

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

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

strongBoundPc(A,B): 將結點B強綁定連接到結點A上，A、B之間是單線即父子關系。strongBoundAd(A,B): 將結點B強綁定連接到結點A上，A、B之間是雙線即子孫后代關系。weakBoundPc(A,B): 將結點B弱綁定連接到結點A上，A、B之間是單線，即父子關系。weakBoundAd(A,B): 將B弱綁定連接到A上，A、B之間是雙線。

(4)ors規則語義

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

定義7ors的語義函數：

「·?: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表示的是求值函數σ在部分求值函數P的定義域上的函數值與P保持一致。

3.3ORS優化規則舉例

以下將每條優化規則用ORS語言進行描述的實例，其中的每一條實例都是按照優化規則的定義即將tree_condition，sche_condition，action的形式分成了三部分分別表示。

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

用ORS語言所表達的上述規則如下：

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)])

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

ORS表示如下：

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

RPC(A,B)

delLeafB

規則3 與規則2相似，不同點在于A與B之間的邏輯結點替換為“or”：

ORS表示如下：

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

RPC(A,B)

delLeafB

規則4 該規則與1類似，不同的是樹模式的A、B兩個結點之間是后代關系，并且A、B的名字間在Schema中滿足必然的后代關系：

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)])

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

ORS表示如下：

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

PRAD(A,B)

UpdateChild(C,A,B)

規則6 樹模式中的A、B、C三個結點，A和B、B和C，兩對結點之間都滿足pc關系，A、B、C三個結點為元素結點，且C結點是樹模式中的葉子結點；如果在XML Schema中，所有由A的所代表的結點所能到達的B結點都有必然有孩子結點C的話，那么我們可以將C結點刪除。

ORS表示如下：

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

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

RPCPATH(A,B,C)

delLeafC

規則7 同規則6，不同的是用ad關系替換其中的pc關系。

ORS表示如下：

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

RADPATH(A,B,C)

delLeafC

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

ORS表示如下：

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

∧isReturn(B)

RPC(A,B)

strongBoundPc(A,B)

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

4 工具實現

4.1 系統實現流程

樹模式優化動作生成的實現流程如圖4所示。

流程中，平行四邊形表示輸入或輸出數據，矩形框表示流程中的處理模塊，實線箭頭表示數據的流向，虛線箭頭表示模塊間的調用關系，箭頭的指向是被調用的模塊。每個處理模塊左上角的文字是該模塊用到的輔助工具包。

根據圖4所示的流程，下面對幾個主要的模塊進行介紹：

(1) 樹模式優化模塊

即最后會輸出優化動作列表的子模塊。此模塊接受變量映射的結果和schema條件的語法樹形式，調用特征提取模塊完成優化動作列表輸出的任務。

(2) 約束檢查模塊

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

(3) 變量映射模塊

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

(4) 詞法分析模塊

是對由ORS表達的優化規則進行詞法分析的子模塊。詞法分析模塊的實現是以開源的Flex工具為基礎的。

(5) 語法分析模塊

此模塊是對ORS表達的優化規則進行語法分析的子模塊。此模塊的實現借助了工具Bison，通過建立ORS的語法樹，該模塊實現依賴詞法分析子模塊。

(6) Schema圖轉換模塊

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

總的來看，工具的輸入為XML Schema文檔，由ORS表示的優化規則，待查詢的樹模式GTP，經過一系列操作之后輸出對應樹模式在特定優化規則下的優化動作列表。

圖4 樹模式優化動作生成實現流程

4.2 優化動作輸出舉例

對于前文中如圖2所示的GTP模型：

其中橢圓內的字符串為結點的名字，結點附近的數字是結點的編號，結點之間的單線表示結點之間的PC關系，雙線代表結點之間的祖先后代關系，標星號的結點為返回結點。

如果我們能從對應XML Schema文檔中得到如下結果：結點3和結點6、結點3和結點7之間、結點4和結點8之間存在必然的父子約束，結點3和結點5之間存在必然的子孫后代約束。那么我們對樹模式進行如下的幾步優化，會得到相應結果。

針對規則1：

工具輸出截圖如下：

上述截圖中的結果表示刪除結點編號為8和結點編號為6的結點，即刪除title結點和city結點。因為從XML Schema文檔中可知結點4和結點8、結點3和結點6之間存在必然的父子關系，根據必然父子關系的描述[2]，我們可以知道，在符合這個XML Schema文檔定義的XML文檔中，所有的shipto元素都必然會有city孩子元素，所有的item元素必然會有title子元素。而我們的GTP所示要求shipto結點有city子節點，item結點有title子節點，并且shipto結點和city結點之間以及item結點和title結點之間存在必然的父子關系，因此可以將shipto結點的孩子結點city結點以及item的孩子結點title結點裁剪掉。因為在例子中的GTP中根本就是冗余的查詢。

GTP模型在進行上述優化后變為如圖5所示。

圖5 采用規則1優化后的GTP模型

如果繼續采用規則4對上述GTP進行優化，工具會得到如下結果：

此次優化的分析同采用優化規則1的優化，只不過將結點之間的父親孩子關系轉換為子孫后代關系，因為在XML Schema中結點3和結點5之間存在必然的子孫后代的關系[2]。即在符合此XML Schema的XML文檔中shipto元素必會有country后代元素，此GTP查詢中要求shipto元素必須有country子孫元素也同樣為冗余查詢，故在這個GTP查詢中可刪除country結點。

GTP模型優化為如圖6所示。

圖6 采用規則4優化后的GTP

對上述的GTP繼續采用優化規則8進行優化：工具會給出如下的輸出結果：

在樹模式查詢中一個XML文檔實例中的元素應該滿足GTP的所有的強綁定，而不要求必須滿足弱綁定。強綁定可以有過濾更多的結點，使結果集更小，從而有利于提高查詢效率。盡可能地把弱綁定轉化為強綁定，是XML查詢處理中一個很大的優化點[14]。

優化后的樹模型如圖7所示。

圖7 采用規則8優化后的GTP

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

工具的實現環境：硬件環境：ThinkVision，軟件環境：操作系統：RedHat Linux，編譯器和編輯器：GCC、Vim。

5 結 語

針對一種算法只解決一種具有某種特定特點的樹模式優化方案的缺陷，本文提出了一個完整的、統一的解決樹模式優化動作的生成問題的方案。本文所提出的方案以時態邏輯、謂詞邏輯、模型檢查等形式化的方法為基礎，實現了基于優化規則的樹模式優化動作自動生成工具。

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

本文的方案是基于優化規則的優化動作自動生成。由于本文將多種類的樹模式的優化統一于同一個優化框架之下，較之前一個算法只能優化一種類型的樹模式的方法增加了通用性，此種方案增加了預處理的成本，與專門針對特定的schema約束的算法相比，存在性能下降的問題；另外，在描述優化規則中的schema條件時，到目前僅支持判斷名字的謂詞。后續工作中，我們打算在現在方案的基礎上，擴充其他schema條件中可能涉及到的謂詞，例如，孩子順序的謂詞、孩子結點個數的謂詞、有關Schema元素結點的屬性謂詞等，那么可能對樹模式進行更徹底的優化。并且繼續擴充時態邏輯公式，以支持更多的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中國計算機大會,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數據中Twig查詢處理與優化技術研究綜述[J].計算機科學與探索,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].計算機科學,2015,42(11A):438-443.

[14] 孟小峰,羅道鋒,蔣瑜,等.QreintXA:一種有效的XQuery查詢代數[J].軟件學報,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。趙瑞芳，碩士生，主研領域：XML樹模式查詢優化。劉科，碩士。楊紅麗，副教授。廖湖聲，教授。

TP391

A

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