基于模型检查的XML树模式优化动作生成

2017-04-14赵瑞芳杨红丽廖湖声

计算机应用与软件 2017年3期

关键词：谓词结点语义

赵瑞芳刘科杨红丽廖湖声

(北京工业大学北京 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)

(5)

sche_condition是CTL公式的一个子集，这些CTL表达式用来描述XMLSchema中的约束，即文献[2,13]中所使用的的RPC(必然父子)、RAD(必然后代)等Schema约束。

(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之间是双线。

(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

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