魏秀娟 , 李永明,2

1(陜西師范大學 數(shù)學與信息科學學院,陜西 西安 710119)

2(陜西師范大學 計算機科學學院,陜西 西安 710119)

非確定性在計算理論中有著重要意義[1?5].從邏輯層面看,非確定計算只涉及存在量詞,而作為非確定的推廣,“交替”在存在量詞的基礎上又增加了全稱量詞.Chandra將交替的概念與自動機相結(jié)合,提出了交替自動機的概念[6],隨后,這一類型的自動機在形式化證明中被作為一種有用的模型普遍使用[7?14].

Zhou[15]在原有交替ω-有窮自動機接受條件的基礎上定義了6種新形式的接受條件,并研究了交替ω-有窮自動機在這些條件下接受語言的能力.Vardi在研究線性時序邏輯[14]時,給出了用自動機理論方法來研究模型檢測的新思路,即,把模型檢測的可滿足性問題轉(zhuǎn)化為判斷自動機語言是否為空的問題來討論.Vardi運用Muller等人給出的交替(Büchi)自動機與非確定型(Büchi)自動機的等價性,為任意給定的線性時序邏輯公式構(gòu)造相應的交替Büchi自動機,使得該自動機接受的語言恰好等于滿足原線性時序邏輯公式的計算的全體.

Kupferman等人[16,17]定量地對交替自動機展開研究,提出了實數(shù)集上加權交替自動機的概念,并討論了特殊語義(如Max,Sum,Sup,Lim sup語義)下加權交替(Büchi)自動機的表達能力,同時研究了特殊語義下加權交替(Büchi)自動機的代數(shù)封閉性.鑒于權值取值和語義選取的局限性,實數(shù)集上加權交替自動機的討論較為特殊.另外,終止狀態(tài)的影響并未考慮在內(nèi),這也體現(xiàn)了Kupferman等人[16,17]討論的局限性.基于這些問題,Wei等人提出了格值交替自動機的概念[18],概念的創(chuàng)新性體現(xiàn)于權值的設置.文獻[18]將轉(zhuǎn)移的權值作為運行樹葉子節(jié)點的標記,使得樹語言計算簡潔化,同時保證了對轉(zhuǎn)移取對偶運算、終止權重取補后所得的自動機與原自動機接受語言互補這一性質(zhì);此外,Wei等人比較了格值交替自動機與格值非確定型自動機的表達能力.

樹作為重要的非線性數(shù)據(jù)結(jié)構(gòu),在計算機科學中應用非常廣泛.在編譯源程序時,樹可被用來表示源程序的語法結(jié)構(gòu);在數(shù)據(jù)庫系統(tǒng)中,樹可作為信息的重要組織形式.因此,關于輸入為樹結(jié)構(gòu)的自動機研究也是非常有意義的.但到目前為止,針對交替樹自動機的研究僅有較少學者涉及[11,19].Muller等人在文獻[10,11]中針對經(jīng)典情形下的交替(Büchi)(樹)自動機展開討論時指出:對交替(Büchi)(樹)自動機的轉(zhuǎn)移函數(shù)取對偶運算,并將終止狀態(tài)和非終止狀態(tài)互換所得的自動機與原自動機接受的語言互補;同時討論了交替(Büchi)(樹)自動機與非確定型(Büchi)(樹)自動機的表達能力.

量化情形下輸入為樹(k元Σ-樹)結(jié)構(gòu)的交替自動機暫未有人展開討論,針對此類計算模型是否有如上結(jié)論,本文即從此初衷展開研究且僅考慮有限輸入樹的情形.這里將Muller等人提出的交替樹自動機的概念[10,11]和Wei等人在格值交替自動機[18]上的權值設置方式相結(jié)合,引入了格值交替樹自動機的概念,討論了其代數(shù)封閉性和表達能力.特別地,將狀態(tài)轉(zhuǎn)移函數(shù)取對偶運算,終止權重取補之后即可得到與原自動機接受語言互補的格值交替樹自動機.此外,討論了格值交替樹自動機與格值樹自動機之間的表達能力,說明了二者的等價性.最后指出可用格值非確定型自動機來模擬格值交替樹自動機.

1 預備知識

首先介紹本文的預備知識,更多詳細內(nèi)容參見文獻[18?21].

1.1 樹的相關概念

定義1[20].元素組(Σ,rk)稱為一個分級的字母表,其中,Σ為有限集合,rk為Σ到自然數(shù)集合N上的一個映射(在這里稱為級映射).

在不引起混淆的情況下,通常用Σ表示(Σ,rk),簡稱字母表.對任意的k≥0,Σ(k)={σ∈Σ|rk(σ)=k}.

定義2[20].設H∩Σ=?.H上Σ-項(Σ-樹或簡稱樹)構(gòu)成的集合TΣ(H)為滿足下面兩個條件的最小的集合T:

(1)Σ(0)∪H?T;

(2) 如果k≥1,σ∈Σ(k),且ξ1,…,ξk∈T,則σ(ξ1,…,ξk)∈T.

當H=?,TΣ(?)簡記為TΣ.

定義3[20].樹的高度Height和位置集Pos是從集合TΣ分別到自然數(shù)集N和由自然數(shù)集生成的幺半群的冪集P(N*)上的映射,遞歸定義如下.

(1) 對任意的α∈Σ(0),Pos(α)={ε},Height(α)=0;

(2) 對任意的ξ=σ(ξ1,…,ξk)∈TΣ,k≥1:

定義4[20].設ξ∈TΣ,w∈Pos(ξ),ξ(w)表示ξ在w處的標記,遞歸定義如下.

(1) 對任意的α∈Σ(0),α(ε)=α;

(2) 對任意的ξ=σ(ξ1,…,ξk)∈TΣ,k≥1,ξ(ε)=σ;且對于任意的1≤i≤k和v∈Pos(ξi),ξ(iv)=ξi(v).

規(guī)定位置w所在的層數(shù)稱為樹的第|w|層(這里的|w|表示串w的長度).

1.2 格的相關概念

定義5[21].集合X上的二元關系≤如果滿足以下條件,則稱≤為集合X上一個序關系,同時稱X為一個偏序集.

(1) 對任意的x∈X,有x≤x成立;

(2) 對任意的x,y∈X,若x≤y和y≤x成立,則有x=y成立;

(3) 對任意的x,y,z∈X,若x≤y和y≤z成立,則有x≤z成立.

基于集合X上的序關系≤,可以定義X的子集X′的上(下)界:設x∈X,如果對任意的y∈X′都有y≤x(x≤y),則稱x為X′的一個上界(下界).

X′的上確界(下確界)指的是X′的最小(大)上界(下界),用sup(X′)(inf(X′))表示.特別地,X作為自身的一個子集,若X存在上確界(下確界),則用1(0)表示sup(X)(inf(X)),并稱其為X的最大(小)元.

對任意的x,y∈X,可以用∨,∧運算表示上下確界:x∨y表示sup{x,y};x∧y表示inf{x,y}.

定義6[21].設L為一個非空的偏序集,若對任意的x,y∈L,x∨y和x∧y同時存在,則稱L為一個格.若格L有上下確界(同樣用1,0表示),則稱L為有界格.若格L中的任意元素x,y,z滿足x∧(y∨z)=(x∧z)∨(y∧z),則稱L為分配格.

例如,L={0,1,b1,b2,b3}(如圖1所示),滿足:b1∨b2=b1;b1∨b3=1;b2∨b3=b3;b1∧b2=b2;b1∧b3=b2;b2∧b3=b2.對任意的x∈L,有x∨1=1,x∧1=x,x∨0=x,x∧0=0成立.

Fig.1 Lattice L圖1 格L

容易驗證,L為一個有界分配格.通常情況下,用符號1⊕22來表示上述格結(jié)構(gòu).

1.3 格值樹自動機

定義7[20].L上的格值樹自動機是一個四元組(Q,Σ,μ,ν),其中,Q是有限狀態(tài)集;Σ是一個分級的字母表;μ=(μk|k∈N)是一簇狀態(tài)轉(zhuǎn)移函數(shù),;ν是格值根權向量,ν∈LQ,即ν:Q→L.格值樹自動機接受的樹語言(樹級數(shù))是從TΣ到格L上的映射r,對任意的ξ∈TΣ:

這里的hμ為從TΣ到LQ上唯一的Σ-代數(shù),即hμ為從TΣ到LQ上的映射且滿足:對任意的σ(ξ1,…,ξk)∈TΣ和q∈Q,

例如,A=(Q,Σ,μ,ν)為L=1⊕22上的一格值樹自動機,其中,Q={q1,q2};Σ={σ,α},σ∈Σ(2),α∈Σ(0);非零的狀態(tài)轉(zhuǎn)移函數(shù)如下:

則A所對應的樹語言r接受樹σ(α,α)的程度如下:

1.4 交替樹自動機的相關概念

對于給定的集合X,設B+(X)為X上所有正布爾公式(即X中的元素通過∨,∧運算生成的布爾公式)構(gòu)成的集合,此外,要求公式true,false也在B+(X)中.

令Y?X,θ∈B+(X).將公式θ中屬于Y的元素賦值為真,將X/Y中元素賦值為假,如果將所有元素賦值之后,最終結(jié)果為真,則稱Y滿足公式θ.進一步地,若Y的任意子集都不滿足公式θ,則稱Y以極小方式滿足θ.

定義8[19].Σ上的交替樹自動機是一個四元組(Q,Σ,I,Δ),其中,Q,Σ分別為有限狀態(tài)集和輸入字母表;I為初始狀態(tài)集;Δ:Q×Σ→B+(Q×N)為狀態(tài)轉(zhuǎn)移函數(shù),且對任意的q∈Q,σ∈Σ,有Δ(q,σ)∈B+(Q×{1,…,rk(σ)})成立.B+(Q×N)中的N為自然數(shù)集.

定義9[19].設ξ∈TΣ,A為Σ上的一個交替樹自動機.A在ξ上的一個運行定義為一棵節(jié)點標記屬于Q×N*的樹t且滿足:

設t(w)=(q,w′),ξ(w′)=σ并且δ(q,σ)=θ,若存在Q×{1,…,rk(σ)}的子集{(q1,i1),…,(qn,in)}滿足θ,則w在t中有后繼位置w1,…,wn,且這些位置的標記依次為(q1,w′i1),…,(qn,w′in).

如果運行樹根節(jié)點的標記為(q,ε)且q∈I,則稱該運行是可被A接受的.

1.5 格值正布爾公式

對于給定的集合X,B+(L∪X)表示X上所有格值正布爾公式(即L∪X上的正布爾公式)構(gòu)成的集合.此外,要求公式true,false在B+(L∪X)中.

任給集合Y?X,θ∈B+(L∪X).定義格值元素v(θ,Y):將公式θ中屬于Y的元素賦值為1,將X/Y中的元素賦值為0,令v(θ,Y)為θ賦值后的結(jié)果.設θ1,θ2∈B+(L∪X),若對任意的Y?X,都有v(θ1,Y)=v(θ2,Y)成立,則稱θ1與θ2等價,記為θ1≡θ2.例如,θ1=(0.5∨(0.3∧(0.8∨x1)))∧0.2,θ2=0.2∧x1,按定義易證θ1≡θ2.

由文獻[18]可知:對于任意的格值正布爾公式θ而言,均可以找到與其等價的最簡終展開式,用θS表示.這里的最簡終展開式意味著公式的析取范式中,析取連接詞連接的任意兩項不能存在包含關系,即:任意的兩項,不能有l(wèi)≤l′和J≤I同時成立.若為θ的最簡終展開式中的一項,則稱集合{xs|s∈S}以極小方式滿足θ的權重為l″.對于上述θ1,θ2,可知二者有相同的最簡終展開式0.2∧x1.事實上,θ1≡θ2當且僅當θ1和θ2有相同的最簡終展開式.特別地,true≡1,false≡0.

2 格值交替樹自動機

本節(jié)引入格值交替樹自動機的概念,討論其閉包性質(zhì)以及格值交替樹自動機與格值樹自動機、格值非確定自動機之間的表達能力.

2.1 格值交替樹自動機的概念

下文中,如果沒有特別說明,L均為分配格,且包含最大元1和最小元0.

定義10.k元Σ-樹上的格值交替樹自動機(簡稱格值交替樹自動機)是一個五元組A=(Q,Σ,I,δ,K),其中,Q,Σ分別為有限狀態(tài)集和輸入字母表,I為格值初始狀態(tài)集,δ是從Q×Σ到B+(L∪(Q×K))上的映射.Q×K是所有形如(q,i)的元素構(gòu)成的集合,q∈Q,i∈K,K={1,…,k}是方向集.

定義11.格值交替樹自動機A在給定輸入樹ξ(∈TΣ)上的運行為一棵節(jié)點標記屬于L∪(Q×K*)的樹t,且滿足:

(1) 如果t(ε)=(q,ε),則I(q)≠0.

(2) 設t(w)=(q,w′),ξ(w′)=σ(σ∈Σ(k))且δ(q,σ)=θ(θ≠true).若存在Q×{1,…,rk(σ)}的某個子集{(q1,i1),…,(qs?1,is?1)}以極小方式滿足θ的權重為l(l≠1),則w在t中的后繼位置有w1,…,ws,且這些位置的標記分別為l,(q1,w′i1),…,(qs?1,w′is?1).若存在集合{(q1,i1),…,(qs?1,is?1)}以極小方式滿足θ的權重為1,則w在t中有后繼位置w1,…,w(s?1),且這些位置的標記分別為(q1,w′i1),…,(qs?1,w′is?1)(后一種情形下相當于l=1,從下文格值交替樹自動機接受語言的定義可以看出,此處的1并不影響接受語言的程度,為了計算方便略去不標).

(3) 如果t(w)=(q,w′),ξ(w′)=σ(σ∈Σ(k))且δ(q,σ)=true,則w在t中只有1個后繼位置w1,節(jié)點標記為1(此處的1不省略是為了使所有葉子節(jié)點都有格值標記).

(4) 如果t(w)=l,則w沒有后繼位置.

設A為格值交替樹自動機,A所接受的語言rA為從TΣ到格L上的映射,定義如下:對任意的ξ∈TΣ,

其中,RA(ξ)表示A在給定輸入樹ξ上的所有運行樹構(gòu)成的集合,(q,ε)為運行樹t的根節(jié)點的標記.wt(t)表示運行樹t的權重,該值等于t的所有葉子節(jié)點標記的合取值.根據(jù)運行樹的定義可知,t的所有葉子節(jié)點的標記均為格值元素,即wt(t)等于t中出現(xiàn)的所有格值元素的合取值.

若運行t使得t(ε)=(q,ε)且I(q)∧wt(t)≠0成立,則稱t為可被A接受的運行.

例1:令L=1⊕22(如圖1所示).設A=(Q,Σ,I,δ,K),其中,Q={q0,q1,q2},Σ={σ,α},K={1,2}.其中,σ∈Σ(2),α∈Σ(0),初始權重為:I(q0)=b1,I(q1)=I(q2)=0.狀態(tài)轉(zhuǎn)移函數(shù)為:δ(q0,σ)=(b1∧(q1,1)∧(q1,2))∨(b2∧(q2,1))∨b3;δ(q0,α)=true;δ(q1,σ)=b2∧(q2,1);δ(q1,α)=true;δ(q2,σ)=b1∧(q1,2);δ(q2,α)=false.

給定輸入樹ξ=σ(σ(α,α),α),由定義11可知ξ上的接受運行樹有兩棵,記為t1,t2,如圖2所示.

Fig.2 All accepting runs of A on ξ圖2 A 在ξ上的接受運行樹

格值交替樹自動機A接受ξ的程度為

為了下文敘述方便,將t中非葉子節(jié)點的標記(狀態(tài)和位置構(gòu)成的二元對)中的第1分量稱為狀態(tài)指標,第2分量稱為位置指標.

2.2 格值交替樹自動機的閉包性質(zhì)

從代數(shù)角度研究各種不同類型的自動機[22?25],討論其是否構(gòu)成一個封閉的代數(shù)系統(tǒng)是對自動機本身性質(zhì)的探討,也是保證其運算合理性的前提.這一節(jié)針對本文提出的格值交替樹自動機的封閉性問題進行研究.

對于經(jīng)典的交替樹自動機而言,文獻[10]借助計算樹的概念和Game-理論證明了對交替樹自動機的轉(zhuǎn)移函數(shù)取對偶運算,將終態(tài)和非終態(tài)互換即可得到與原交替自動機互補的另一交替自動機.本節(jié)旨在文獻[10]的基礎上研究格值交替樹自動機的補運算,并證明其封閉性.由于要考慮補運算,所以這一節(jié)中用到的格含有補運算記作c,即c是格L上的一元運算且滿足:對任意的l,l1,l2∈L,有l(wèi)=c(c(l))和l1≤l2?c(l2)≤c(l1)成立[21].

引理1.對于任意的格值交替樹自動機,均存在與其等價的且具有唯一初始狀態(tài)的格值交替樹自動機.

證明:設A為格值交替樹自動機(Q,Σ,I,δ,K)構(gòu)造A′=(Q∪{q0},Σ,q0,δ′,K):A′在A的狀態(tài)集基礎上添加一個額外狀態(tài)q0,作為A′的唯一初始狀態(tài);對任意的σ∈Σ,添加轉(zhuǎn)移函數(shù);對任意的q∈Q,σ∈Σ,令δ′(q,σ)=δ(q,σ).

由A′的構(gòu)造可知,初始自動機A與目標自動機A′在任意給定的輸入樹上的運行樹一一對應:事實上,A在任意的輸入樹ξ上的運行樹t,其中,t(ε)=q′且I(q′)≠0,對應于A′在ξ上的運行樹t′,其中,t′(ε)=q0且wt(t′)=I(q0)∧wt(t),因此A與A′等價:

有引理1的保證,在接下來的討論中如果沒有特殊說明,則僅考慮具有唯一初始狀態(tài)的格值交替樹自動機.

定理1.k元Σ-樹上的格值交替樹自動機關于交、并運算封閉.

定義k元Σ-樹上的格值交替樹自動機:

定理2.k元Σ-樹上的格值交替樹自動機關于補運算封閉.

為了證明定理2,需要借鑒參考文獻[10]的記號和定義而引入一些新的概念.在介紹新概念之前,首先介紹Q×K上的格值正布爾公式(L∪(Q×K)上的正布爾公式)的對偶運算.

對于Q×K上的格值正布爾公式,定義對偶運算:

對格值交替樹自動機A的所有轉(zhuǎn)移函數(shù)取對偶運算、終止權重用其補元代替,即可得到一個新的格值交替樹自動機,用表示.定理2可等價表述為是一個與A互補的k元Σ-樹上的格值交替樹自動機.

定義12.格值的n步ID(n≥0),記作FHn,為所有形如h1,h2的元素構(gòu)成的集合,其中,

·h1=(q0,ε)k1(q1,k1)k2(q2,k1k2)…kn(qn,k1…kn);

·h2=(q0,ε)k1(q1,k1)k2(q2,k1k2)…kt(qt,k1…kt)k′(l),t≤n?1,ki∈K(i=1,…,n),k′=0.

這里的0表示自然數(shù)0,并非格中的零元),l∈L.

注意到,FHn∩FHn+1≠?.

定義13.對于FHn中的任意元h以及L∪(Q×K)中的任意元g,定義h,g的連接.

下面引入格值計算樹的概念.

定義14.設A為一格值交替樹自動機,ξ為給定的輸入樹,遞歸定義A在ξ上的格值計算樹T(A,ξ)如下.

例2:設A=(Q,Σ,q0,δ,K)為一個具有唯一初始狀態(tài)的格值交替樹自動機,Q,Σ,δ,K的定義與例1一致.求A在輸入樹ξ上的格值計算樹.根據(jù)定義14可得T(A,ξ),如圖3所示.

Fig.3 Computation tree of A on ξ圖3 A 在給定的輸入樹ξ上的格值計算樹

除了按照定義11求格值交替樹自動機接受的語言rA(ξ)外,可以根據(jù)A在ξ上的格值計算樹T(A,ξ)的最后一層節(jié)點的標記得到rA(ξ),只需將T(A,ξ)每條分支上標記結(jié)尾處的格值合取,然后再將不同分支上所得結(jié)果取析取運算.對例2用這種方法,有結(jié)果(b2∧b1∧1)∨b3=b3.

設T(A,ξ)是A在ξ上的格值計算樹.取任意的i(0≤i≤Height(t)+1),且h′,…,h(k)分別為T(A,ξ)第i層的k個節(jié)點的標記,則稱h′∨…∨h(k)為T(A,ξ)第i層的總表達式.借助該定義可將求證定理2轉(zhuǎn)化為求證T(A,ξ)第Height(ξ)+1層的總表達式與第Height(ξ)+1層的總表達式互為對偶關系.

現(xiàn)在來證明該結(jié)論.

證明:設hi為T(A,ξ)第i層的總表達式,0≤i≤Height(ξ)+1.由定義14可得到hi與hi+1有關系δi(hi)=hi+1.

2.3 格值交替樹自動機的表達能力

這一節(jié)主要討論格值交替樹自動機、格值樹自動機以及格值非確定自動機之間的表達能力.首先證明格值交替樹自動機和格值樹自動機有相同的表達能力.

定理3.對于任意的格值樹自動機,存在與其等價的格值交替樹自動機.

下面給定理3對應的算法表示.

算法1.

輸入:格值樹自動機A=(Q,Σ,q0,μ);

輸出:格值交替樹自動機A′=(Q,Σ,q0,δ,K).

算法1的時間復雜度完全取決于δ的構(gòu)造,而δ的構(gòu)造同時取決于q,σ以及q1,…,qk的選取,則該算法的時間復雜度為O(|Q|×|Σ|×|Q|m),即O(|Q|m+1×|Σ|),其中m=max{rk(σ)|σ∈Σ}.

下面說明算法1輸出的自動機即為與輸入的格值樹自動機等價的格值交替樹自動機.

對任意的輸入樹ξ,只需證明A在ξ上的接受運行與A′在ξ上的接受運行一一對應,且二者權重相等.

事實上,將A在ξ上的任意接受運行的葉子(格值標記)節(jié)點和非葉子節(jié)點標記的第2指標去掉(只留狀態(tài)指標)后,即得到A′在ξ上的一個接受運行,且二者權重相等.反之,將A′在ξ上的任意接受運行的每個非葉子節(jié)點標記換成元素對,令元素對的第1指標等于該位置的原始標記,第2指標等于該節(jié)點的位置,并將每步轉(zhuǎn)移的權重標出.即將轉(zhuǎn)移標在(q,w)的下一行的最左端,作為葉子節(jié)點標記,與同行的節(jié)點標記從左至右依次為(q1,w1),…,(qk,wk).經(jīng)過上述轉(zhuǎn)化,即得到A在ξ上的一個接受運行,且與A′在ξ上的接受運行權值相同.

例 3:設A=(Q,Σ,q1,μ)為格值樹自動機,其中,L=1⊕22,Q={q1,q2},Σ={σ,α},σ∈Σ(2),α∈Σ(0);.下面構(gòu)造與A等價的格值交替樹自動機A′.

令A′=(Q,Σ,q1,δ,K),其中,K={1,2};δ(q1,σ)=(b1∧(q1,1)∧(q2,2))∨(b1∧(q2,1)∧(q1,2));δ(q2,σ)=b3∧(q2,1)∧(q2,2);δ(q1,α)=b2;δ(q2,α)=1.

取ξ=σ(σ(α,α),α),A在ξ上的接受運行記為t1,t2,t3,相應地,A′在ξ上的接受運行為(如圖4所示).

Fig.4 All accepting runs of A,A′ on the input tree ξ圖4 A,A′在給定的輸入樹ξ上的所有接受運行

定理4.對于任意的格值交替樹自動機,存在與其等價的格值樹自動機.

由于定理4的證明并不直觀,故在給出其算法和形式化證明之前先用例子來說明構(gòu)造思路.

同樣地,這里僅考慮具有唯一初始狀態(tài)的格值交替樹自動機C=(Q,Σ,q2,δ,K).其中,L=[0,1];Q={q1,q2,q3,q4,q5},Σ={σ,α,β},σ∈Σ(2),α,β∈Σ(0),K={1,2}.狀態(tài)轉(zhuǎn)移函數(shù)見表1.

Table 1 Transition functions表1 狀態(tài)轉(zhuǎn)移表

對于給定的輸入樹ξ,將C在ξ上的任意接受運行t按下列方法轉(zhuǎn)化為t′的形式.

(1) 令t′(ε)等于t(ε)二元組中的狀態(tài)指標q2.

(2) 將第1層所有非格值元素按第2個指標分類,指標一致的放在一起,且將不同組的元素按第2指標的字典序從左到右排列.將排列好的每組中元素位置指標省去,形成新的多元狀態(tài)組P1,…,Prk(ξ(ε)),并將這些多元狀態(tài)組作為t′(ε)的后繼狀態(tài).令等于第1層出現(xiàn)的格值元素;若沒有格值元素出現(xiàn)則令其為1,其中,Pi為新形成的第i個狀態(tài)組(i=1,…,rk(ξ(ε))).即將q2,q4放在一起為一個二元狀態(tài)組,記為(q2,q4);q1單獨為一組.令(q2,q4)和q1為t′(ε)的后繼狀態(tài),且

(3) 將t第1層中同屬于第i個狀態(tài)組的元素全部拿來,把它們的非格值后繼按步驟(2)中的方法分類合并排列,略去第2指標,并將這些新的多元狀態(tài)組作為t′(i)的后繼.令轉(zhuǎn)移權重等于第i個狀態(tài)組的所有格值后繼的合取值;若沒有格值后繼,令權重為1.即(q2,q4)的后繼從左至右為(q1,q3,q4)和(q2,q3),且等于其格值后繼.

(4) 對每層元素重復過程(3),直到t的第Height(t)層元素全部按照步驟(3)轉(zhuǎn)化后立即停止(結(jié)果如圖5、圖6所示).

若某個狀態(tài)組僅有格值后繼,例如節(jié)點標記(q1,2),則令

將C在ξ上的接受運行t轉(zhuǎn)化為t′的過程中所構(gòu)造的狀態(tài)轉(zhuǎn)移函數(shù)有:

Fig.5 An accepting run of C on input tree ξ,denoted by t圖5 C在給定的輸入樹ξ上的某一接受運行t

Fig.6 A run corresponding to t圖6 將t 按上述方法轉(zhuǎn)化而得的t′

注意到,第(2)步形成的新的元素組個數(shù)不大于rk(ξ(ε)).若個數(shù)小于rk(ξ(ε)),則需引入額外狀態(tài),使得加入額外狀態(tài)之后總的后繼個數(shù)等于rk(ξ(ε)).同理,第(3)步、第(4)步兩個步驟中也可能遇到這樣的情況,也要做相同的處理,具體做法見算法2.算法中提到的q*即為引入的額外狀態(tài).算法2為定理4所對應的將給定的格值交替樹自動機轉(zhuǎn)化為與之等價的格值樹自動機的算法表示.

注:下文中出現(xiàn)的δS(q,σ)為δ(q,σ)的最簡終展開式,相同的表示不再贅述.

算法2.

輸入:格值交替樹自動機A=(Q,Σ,q0,δ,K);

輸出:格值樹自動機A′=(Q′,Σ,q0,μ).

算法的時間復雜度完全取決于μ的構(gòu)造,而μ的構(gòu)造同時取決于狀態(tài)、字母表元素和項u1,…,un的選取.在構(gòu)造Ai的過程中要進行|K|?|Q|次比對,故該算法的時間復雜度為O((|K||Q|+1)|Q|×|Q|×|Σ|×|K|).

文獻[19]中交替樹自動機到樹自動機的轉(zhuǎn)換,構(gòu)造的樹自動機的狀態(tài)集為初始輸入的交替樹自動機狀態(tài)集的冪集,轉(zhuǎn)移函數(shù)為f(S1,…,Sn)→{q∈Q|S1×{1}∪…∪Sn×{n}滿足Δ(q,f)}.構(gòu)造過程要考慮任意的n(1≤n≤max{rk(f)|f∈Σ})元狀態(tài)組的轉(zhuǎn)移.這里,狀態(tài)組中的每個分量Si為初始輸入的交替樹自動機狀態(tài)集的冪集的子集.上述算法2的構(gòu)造,格值樹自動機的狀態(tài)集是以初始格值交替樹自動機的狀態(tài)為基礎的n(1≤n≤|Q|)元元素組構(gòu)成的集合,且構(gòu)造轉(zhuǎn)移函數(shù)過程中需要考慮每個這樣的元素組.

由算法2可得:對于A的任意一棵運行樹t,對應地可找到A′的若干棵運行樹t1,…,tp,使得wt(t1)∨…∨wt(tp)=wt(t);反過亦有類似結(jié)論.

事實上,對于A′的任意運行樹t′,與t′等價的A的運行樹t滿足:

(1)t(ε)=(t′(ε),ε).

(2) 設t′的第1層的標記從左至右依次為P1,…,Ps,若P1,…,Ps中沒有等于q*的,則(q,i)為t(ε)的后繼節(jié)點的標記,其中,q∈Pi(i=1,…,s),為t的第1層中唯一的格值標記,且放置在第1層的最左端;若P1,…,Ps中存在Pj等于q*,則(q,i)為t(ε)的后繼節(jié)點的標記,其中,q∈Pi(對于任意的i≠j),同樣地,為t的第1層中唯一的格值標記,且放置在第1層最左端.

(3) 對于t的第1層中任意的(q,i),找到δS(q,σ)中項,使得任意的處在t′的第ii″個位置的多元狀態(tài)集中,則為(q,i)的一個后繼節(jié)點標記,lj為(q,i)的后繼節(jié)點中唯一的格值標記,且放置在(q,i)所有后繼節(jié)點的最左端.依次考慮其他狀態(tài),直到全部狀態(tài)均滿足上述條件完畢,得到t.

例4:設L=[0,1],A=(Q,Σ,I,q0,K)是一格值交替樹自動機,其中,Q={q0,q1},Σ={σ,α},σ∈Σ(2),α∈Σ(0K={1,2},狀態(tài)轉(zhuǎn)移函數(shù)為δ(q0,σ)=(0.2∧(q0,1)∧(q1,1)∧(q1,2))∨(0.3∧(q0,2));δ(q0,α)=true;δ(q1,σ)=0.5∧(q0,2);δ(q1,α)=false.

按定理4方法構(gòu)造與A等價的格值樹自動機A′如下.

A′=(Q′,Σ,q0,μ),其中,Q′=Q∪Q2∪{q*};轉(zhuǎn)移函數(shù)定義如下:

其他沒有提到的轉(zhuǎn)移權重為0.

以輸入樹ξ=σ(σ(α,α),σ(α,α))為例說明A在ξ上的運行與A′在ξ上運行的對應關系,如圖7、圖8所示.

Fig.7 All accepting runs of A on input tree ξ,denoted by t1,t2圖7 A 在給定的輸入樹ξ上的所有接受運行t1,t2

Fig.8 All accepting runs of A′ on input tree ξ,t1,t2 denoted by 圖8 A′在給定的輸入樹ξ上的所有接受運行

A接受ξ與A′接受ξ的程度分別為:

其中,ξ1=ξ2=σ(α,α).

接下來討論如何利用格值非確定自動機來模擬格值交替樹自動機.這里的模擬是指:對于格值交替樹自動機的任意輸入樹,存在格值非確定自動機中的輸入字符串使得前者的接受程度等于后者;同樣地,對于格值非確定自動機的任意輸入字符串,存在格值交替樹自動機的輸入樹,使得二者被接受的程度相等.這里的模擬包含著“等價”的含義,但并非實質(zhì)上的等價,因為前者接受的是樹,后者接受的是字符串.

定理5.設A是一格值交替樹自動機,則可找到格值非確定自動機來模擬A.

類似地,在給出定理5的形式化證明前,先通過一個例子來說明構(gòu)造思想.

這里仍然采用定理4證明前的例子.將ξ上的運行t轉(zhuǎn)化成串w上的路徑P,方法如下.

(1) 將ξ=σ(σ(β,σ(α,β)),β)每層字符按照其位置的字典序排列,并將其位置標于該字符右下角處.將每層所得到的字符串依次連接,得到新的字符串w=σε(σ1β2)(β11σ12)(α121β122).每個字符組可看作單個字符屬于的情況,例如

(2) 將{(q2,ε)}作為路徑P的初始狀態(tài);把t的第1層的非格值元素放在一起作為一個整體,將其作為{(q2,ε)}經(jīng)過字符σε輸入后可能到達的后繼狀態(tài),并令轉(zhuǎn)移權重為該層出現(xiàn)的所有格值元素的合取值.{(q2,ε)}經(jīng)過σε輸入,可能到達狀態(tài){(q2,1),(q4,1),(q1,2)},且轉(zhuǎn)移權重δn({(q2,ε)},σε,{(q2,1),(q4,1),(q1,2)})=0.3.對每層元素重復過程(2),直到t的第Height(t)+1層停止.

將t按上述方法轉(zhuǎn)化得到路徑P(P可看作某一格值非確定自動機的運行路徑):

另外,在定理5證明之前需引入完備的格值交替自動機的概念,該概念在證明中有重要作用.

定義15.若格值交替樹自動機滿足:對任意的q∈Q,σ∈Σ,當δ(q,σ)≠true且δ(q,σ)≠false時,對于δS(q,σ)中的任意一項,任取0≤k≤rk(σ),均存在第2指標為k的元素對出現(xiàn)在該項中,則稱該格值交替樹自動機是完備的.

注意到,例1中提到的格值交替樹自動機不是完備的,比如對于δS(q0,σ)的第2項b2∧(q2,1),該項缺少第2指標為2的元素對;對于第3項b3,該項既缺少第2指標為1又缺少指標為2的元素對.

可以證明,格值交替樹自動機和完備的格值交替樹自動機有如下關系.

命題5.對于任意的格值交替樹自動機,存在與其等價的完備的格值交替樹自動機.

證明:設A=(Q,Σ,q0,δ,K)為任意的格值交替樹自動機.構(gòu)造A′=(Q∪{qΔ},Σ,q0,δ′,K):

(1) 將破壞A完備性的轉(zhuǎn)移全部取出,做如下處理:若δS(q′,σ)中存在某項使得u中不存在第2指標為j(j∈{1,…,rk(σ)})的元素對,則將(qΔ,j)添加到u中.重復上述過程,直到最后得到的u′中存在第2指標為j′(j′=1,…,rk(σ))的元素對時結(jié)束.將δS(q′,σ)中每一項進行改造得到δ′(q′,σ);

(2) 增加轉(zhuǎn)移:對任意的σ∈Σ,令δ′(qΔ,σ)=true.

從構(gòu)造中不難看出,步驟(1)、步驟(2)兩步之后使得某些運行樹僅增加了一些葉子節(jié)點為1的分支,故不改變整體權重,從而A和A′等價.□

例5:將例2中的格值交替樹自動機轉(zhuǎn)化為與其等價的完備的格值交替樹自動機.

δS(q0,σ)中第2項b2∧(q2,1)缺少第2指標為2的元素對,將第2項中添加(qΔ,2),使其變?yōu)閎2∧(q2,1)∧(qΔ,2);同理,第3項0.2既缺少第2指標為1又缺少指標為2的元素對,則添加(qΔ,1)和(qΔ,2),使其變?yōu)閎3∧(qΔ,1)∧(qΔ,2).令添加過后的公式等于δ′(q0,σ).

按照上述做法得到的另一格值樹自動機A′=(Q∪{qΔ},Σ,q0,δ′,K)的轉(zhuǎn)移函數(shù)如下.

·δ′(q0,σ)=(b1∧(q1,1)∧(q1,2))∨(b2∧(q2,1)∧(qΔ,2))∨(b3∧(qΔ,1)∧(qΔ,2));

·δ′(q0,α)=true;δ′(q1,σ)=b2∧(q2,1)∧(qΔ,2);

·δ′(q1,α)=true;δ′(q2,σ)=b1∧(qΔ,1)∧(q1,2);

·δ′(q2,α)=true;δ′(q*,σ)=true;δ′(q*,α)=true.

ξ上的接受運行如圖9所示.

Fig.9 All accepting runs of A′ on input tree ξ,denoted by 圖9 A′在給定的輸入樹ξ上的所有接受運行

下面來證明定理5,這里只需考慮完備的格值交替樹自動機即可.

An的狀態(tài)個數(shù)跟K*的基數(shù)有關,所以定理5構(gòu)造的格值非確定自動機的“有用”狀態(tài)可能無限.由于定理5的研究是為了在理論上揭示交替樹自動機和非確定自動機的內(nèi)部聯(lián)系,故即使出現(xiàn)無限狀態(tài),也并不會到影響二者的聯(lián)系和轉(zhuǎn)化過程.

例6:令L=1⊕22.設A=(Q,Σ,q1,δ,K),其中,K={1,2};δ(q1,σ)=(b2∧(q2,1)∧(q3,2))∧(b3∧(q3,1)∧(q2,2));δ(q2,σ)=b1∧(q3,1)∧(q3,2);δ(q3,σ)=false;δ(q1,α)=false;δ(q2,α)=true;δ(q3,α)=true.

A的所有接受運行樹有4棵,記為t1,t2,t3,t4,它們分別是在輸入樹ξ1,ξ1,ξ2,ξ3上的接受運行(如圖10所示).

Fig.10 All accepting runs of A,denoted by t1,t2,t3,t4圖10 A 的所有接受運行t1,t2,t3,t4

綜上所述,A在W1中任意串上的路徑p1∈P1(p2∈P2)模擬A′在ξ1上的運行t1(t2),A在W2中任意串上的路徑p3∈P3模擬A′在ξ2上的運行t3,A在W3中任意串上的路徑p4∈P4模擬A′在ξ3上的運行t4.

3 總結(jié)

本文引入格值交替樹自動機的概念并對其閉包性質(zhì)和表達能力展開研究.證明了格值交替樹自動機關于交、并、補運算封閉,特別地,利用格值計算樹的概念證明了只需對狀態(tài)轉(zhuǎn)移函數(shù)取對偶運算、將終止權重取補即可得到與原格值交替樹自動機互補的另一格值交替樹自動機.此外,證明了格值交替樹自動機與格值樹自動機的等價性.這為格值樹自動機的補問題提供了另一思路.進一步地,本文指出,可以利用格值非確定型自動機來模擬格值交替樹自動機.這一結(jié)論體現(xiàn)了非確定型自動機和交替樹自動機這兩類不同模型之間的內(nèi)在聯(lián)系.如何將這些結(jié)論推廣到無限樹上,且如何利用這些自動機理論的結(jié)果去討論計算樹邏輯模型檢測問題,有待于進一步探討.