格值交替樹自動機(jī)?

魏秀娟 , 李永明,2

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

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

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

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

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

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

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

1 預(yù)備知識

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

1.1 樹的相關(guān)概念

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

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

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

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

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

當(dāng)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].設(shè)ξ∈TΣ,w∈Pos(ξ),ξ(w)表示ξ在w處的標(biāo)記,遞歸定義如下.

(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 格的相關(guān)概念

定義5[21].集合X上的二元關(guān)系≤如果滿足以下條件,則稱≤為集合X上一個序關(guān)系,同時稱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上的序關(guān)系≤,可以定義X的子集X′的上(下)界:設(shè)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,可以用∨,∧運(yùn)算表示上下確界:x∨y表示sup{x,y};x∧y表示inf{x,y}.

定義6[21].設(shè)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

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

1.3 格值樹自動機(jī)

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

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

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

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

1.4 交替樹自動機(jī)的相關(guān)概念

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

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

定義8[19].Σ上的交替樹自動機(jī)是一個四元組(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].設(shè)ξ∈TΣ,A為Σ上的一個交替樹自動機(jī).A在ξ上的一個運(yùn)行定義為一棵節(jié)點(diǎn)標(biāo)記屬于Q×N*的樹t且滿足:

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

如果運(yùn)行樹根節(jié)點(diǎn)的標(biāo)記為(q,ε)且q∈I,則稱該運(yùn)行是可被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é)果.設(shè)θ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.

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

2 格值交替樹自動機(jī)

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

2.1 格值交替樹自動機(jī)的概念

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

定義10.k元Σ-樹上的格值交替樹自動機(jī)(簡稱格值交替樹自動機(jī))是一個五元組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.格值交替樹自動機(jī)A在給定輸入樹ξ(∈TΣ)上的運(yùn)行為一棵節(jié)點(diǎn)標(biāo)記屬于L∪(Q×K*)的樹t,且滿足:

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

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

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

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

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

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

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

例1:令L=1⊕22(如圖1所示).設(shè)A=(Q,Σ,I,δ,K),其中,Q={q0,q1,q2},Σ={σ,α},K={1,2}.其中,σ∈Σ(2),α∈Σ(0),初始權(quán)重為: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可知ξ上的接受運(yùn)行樹有兩棵,記為t1,t2,如圖2所示.

Fig.2 All accepting runs of A on ξ圖2 A 在ξ上的接受運(yùn)行樹

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

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

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

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

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

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

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

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

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

定理1.k元Σ-樹上的格值交替樹自動機(jī)關(guān)于交、并運(yùn)算封閉.

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

定理2.k元Σ-樹上的格值交替樹自動機(jī)關(guān)于補(bǔ)運(yùn)算封閉.

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

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

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

定義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.設(shè)A為一格值交替樹自動機(jī),ξ為給定的輸入樹,遞歸定義A在ξ上的格值計算樹T(A,ξ)如下.

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

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

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

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

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

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

2.3 格值交替樹自動機(jī)的表達(dá)能力

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

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

下面給定理3對應(yīng)的算法表示.

算法1.

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

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

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

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

對任意的輸入樹ξ,只需證明A在ξ上的接受運(yùn)行與A′在ξ上的接受運(yùn)行一一對應(yīng),且二者權(quán)重相等.

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

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

令A(yù)′=(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在ξ上的接受運(yùn)行記為t1,t2,t3,相應(yīng)地,A′在ξ上的接受運(yùn)行為(如圖4所示).

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

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

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

同樣地,這里僅考慮具有唯一初始狀態(tài)的格值交替樹自動機(jī)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在ξ上的任意接受運(yùn)行t按下列方法轉(zhuǎn)化為t′的形式.

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

(2) 將第1層所有非格值元素按第2個指標(biāo)分類,指標(biāo)一致的放在一起,且將不同組的元素按第2指標(biāo)的字典序從左到右排列.將排列好的每組中元素位置指標(biāo)省去,形成新的多元狀態(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單獨(dú)為一組.令(q2,q4)和q1為t′(ε)的后繼狀態(tài),且

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

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

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

將C在ξ上的接受運(yùn)行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在給定的輸入樹ξ上的某一接受運(yùn)行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所對應(yīng)的將給定的格值交替樹自動機(jī)轉(zhuǎn)化為與之等價的格值樹自動機(jī)的算法表示.

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

算法2.

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

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

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

文獻(xiàn)[19]中交替樹自動機(jī)到樹自動機(jī)的轉(zhuǎn)換,構(gòu)造的樹自動機(jī)的狀態(tài)集為初始輸入的交替樹自動機(jī)狀態(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為初始輸入的交替樹自動機(jī)狀態(tài)集的冪集的子集.上述算法2的構(gòu)造,格值樹自動機(jī)的狀態(tài)集是以初始格值交替樹自動機(jī)的狀態(tài)為基礎(chǔ)的n(1≤n≤|Q|)元元素組構(gòu)成的集合,且構(gòu)造轉(zhuǎn)移函數(shù)過程中需要考慮每個這樣的元素組.

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

事實(shí)上,對于A′的任意運(yùn)行樹t′,與t′等價的A的運(yùn)行樹t滿足:

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

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

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

例4:設(shè)L=[0,1],A=(Q,Σ,I,q0,K)是一格值交替樹自動機(jī),其中,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等價的格值樹自動機(jī)A′如下.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

可以證明,格值交替樹自動機(jī)和完備的格值交替樹自動機(jī)有如下關(guān)系.

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

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

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

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

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

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

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

按照上述做法得到的另一格值樹自動機(jī)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.

ξ上的接受運(yùn)行如圖9所示.

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

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

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

例6:令L=1⊕22.設(shè)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的所有接受運(yùn)行樹有4棵,記為t1,t2,t3,t4,它們分別是在輸入樹ξ1,ξ1,ξ2,ξ3上的接受運(yùn)行(如圖10所示).

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

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

3 總結(jié)

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