汪 國 武
(安徽工程大學(xué)計(jì)算機(jī)與信息學(xué)院 安徽 蕪湖 241000) (安徽工程大學(xué)計(jì)算機(jī)應(yīng)用技術(shù)重點(diǎn)實(shí)驗(yàn)室 安徽 蕪湖 241000)
?
帶空移動(dòng)的加權(quán)有限自動(dòng)機(jī)量化等價(jià)及其轉(zhuǎn)換
汪 國 武
(安徽工程大學(xué)計(jì)算機(jī)與信息學(xué)院安徽 蕪湖 241000) (安徽工程大學(xué)計(jì)算機(jī)應(yīng)用技術(shù)重點(diǎn)實(shí)驗(yàn)室安徽 蕪湖 241000)
在經(jīng)典的有限自動(dòng)機(jī)理論中,帶空移動(dòng)的有限自動(dòng)機(jī)與不帶空移動(dòng)的有限自動(dòng)機(jī)是等價(jià)的。取值于實(shí)數(shù)的加權(quán)有限自動(dòng)機(jī)是自動(dòng)機(jī)的一種推廣模型,它給經(jīng)典自動(dòng)機(jī)的每個(gè)轉(zhuǎn)換賦一個(gè)取值于實(shí)數(shù)的權(quán)值,這些權(quán)值表示執(zhí)行轉(zhuǎn)換的代價(jià)。為了研究帶空移動(dòng)的加權(quán)有限自動(dòng)機(jī)與不帶空移動(dòng)的加權(quán)有限自動(dòng)機(jī)是否具有等價(jià)性這一問題,提出量化等價(jià)的概念,并研究如何將一個(gè)帶空移動(dòng)的加權(quán)有限自動(dòng)機(jī)轉(zhuǎn)換為一個(gè)與之量化等價(jià)的不帶空移動(dòng)的加權(quán)有限自動(dòng)機(jī)。研究結(jié)果表明:這兩者是量化等價(jià)的。
量化等價(jià)不確定的有限狀態(tài)自動(dòng)機(jī)加權(quán)自動(dòng)機(jī)形式化驗(yàn)證
在計(jì)算機(jī)科學(xué)中,有限狀態(tài)自動(dòng)機(jī)[1,2]是自動(dòng)機(jī)理論的研究對象,廣泛地被應(yīng)用于神經(jīng)網(wǎng)絡(luò)、模式識(shí)別、密碼算法、形式化分析與驗(yàn)證等領(lǐng)域中。關(guān)于有限狀態(tài)自動(dòng)機(jī),一個(gè)有趣的結(jié)論是:帶空移動(dòng)和不帶空移動(dòng)的自動(dòng)機(jī)具有等價(jià)性,即如果一個(gè)正則語言能被一個(gè)帶空移動(dòng)的自動(dòng)機(jī)接受,那么該語言可被一個(gè)不帶空移動(dòng)的自動(dòng)機(jī)接受。
經(jīng)典的有限自動(dòng)機(jī)是一種對系統(tǒng)進(jìn)行定性的建模方法,它明確規(guī)定了所建模的系統(tǒng)所具有的性質(zhì)和不具有的性質(zhì)。為了對計(jì)算機(jī)系統(tǒng)的量化信息進(jìn)行建模,研究者提出了很多能描述量化信息的自動(dòng)機(jī)模型[3-7],模糊自動(dòng)機(jī)[8,9]是其中一個(gè)比較有代表性意義的自動(dòng)機(jī)的推廣模型。文獻(xiàn)[10]討論了帶空移動(dòng)的模糊自動(dòng)機(jī)和模糊自動(dòng)機(jī)等價(jià)的充分必要條件;文獻(xiàn)[11]證明了帶空移動(dòng)的不確定性模糊自動(dòng)機(jī)和不確定性模糊自動(dòng)機(jī)具有等價(jià)性。
取值于實(shí)數(shù)的加權(quán)有限自動(dòng)機(jī)[12-15]是自動(dòng)機(jī)的另一種推廣模型,該模型已經(jīng)被用于嵌入式系統(tǒng)的設(shè)計(jì)和驗(yàn)證[16,17]。取值于實(shí)數(shù)的加權(quán)有限自動(dòng)機(jī)的基本特點(diǎn)是:通過給經(jīng)典自動(dòng)機(jī)的每個(gè)轉(zhuǎn)換賦一個(gè)取值于實(shí)數(shù)的權(quán)值,這些權(quán)值表示執(zhí)行轉(zhuǎn)換的代價(jià),如花費(fèi)的時(shí)間或消耗的資源,或者表示為成功執(zhí)行的幾率等。對取值于實(shí)數(shù)的加權(quán)有限自動(dòng)機(jī)的研究已經(jīng)取得較大的進(jìn)展, 但前文提到的結(jié)論:帶空移動(dòng)和不帶空移動(dòng)的自動(dòng)機(jī)具有等價(jià)性,到目前為止還沒有在加權(quán)有限自動(dòng)機(jī)這種模型上進(jìn)行研究。
本文首先提出帶空移動(dòng)的加權(quán)有限自動(dòng)機(jī);接著為了描述帶空移動(dòng)的加權(quán)有限自動(dòng)機(jī)和不帶空移動(dòng)的加權(quán)有限自動(dòng)機(jī)的等價(jià)性,我們提出量化等價(jià)的概念;然后在量化等價(jià)的基礎(chǔ)上,研究和探討如何將一個(gè)帶空移動(dòng)的加權(quán)有限自動(dòng)機(jī)轉(zhuǎn)換為一個(gè)與之量化等價(jià)的不帶空移動(dòng)的加權(quán)有限自動(dòng)機(jī)。
首先介紹加權(quán)有限狀態(tài)自動(dòng)機(jī)、帶空移動(dòng)的加權(quán)有限狀態(tài)自動(dòng)機(jī)及其識(shí)別的語言和量化語言等,然后引入量化等價(jià)的概念。
設(shè)Q是一個(gè)集合,記P(Q)為Q的冪集。后文R+表示非負(fù)實(shí)數(shù)集。
定義1一個(gè)加權(quán)有限(狀態(tài))自動(dòng)機(jī)[14]WFA(weighted finite automaton)M是一個(gè)8元組:
M=(Q,Σ,δ,qI,F,γ,i,f)
其中:
(1) Q:非空有窮狀態(tài)集合。對于任意q∈Q,稱q是M的一個(gè)狀態(tài)。
(2) Σ:輸入有限字母表。
(3) δ:δ?Q×Σ×Q是一個(gè)轉(zhuǎn)換關(guān)系。
(4) qI:qI∈Q是一個(gè)初始狀態(tài)。
(5) F:F?Q是終止?fàn)顟B(tài)集合,對于任意q∈F,稱q為M的終止?fàn)顟B(tài)。
(6) γ:δ→R+是一個(gè)加權(quán)函數(shù)。如果轉(zhuǎn)換(q,a,q′)∈δ,相應(yīng)的權(quán)函數(shù)為γ(δ(q,a,q′)),表示M在狀態(tài)q讀入字母a后到達(dá)狀態(tài)q′時(shí),需要的代價(jià)為γ(δ(q,a,q′))。
(7) i:qI→R+是初態(tài)權(quán)函數(shù),初始狀態(tài)qI的權(quán)值為i(qI)。
(8) f:F→R+是終態(tài)權(quán)函數(shù),如果對于任意q∈F,則終態(tài)q的權(quán)值為f(q)。
我們常用q′∈δ(q,a)表示(q,a,q′)∈δ。另外,我們記δ(q,a)={q′:(q,a,q′)∈δ}。為了符號(hào)簡便,后文γ(δ(q,a,q′))記為γ(q,a,q′)。類似地,我們也將γ(δ(q,a))簡寫為γ(q,a),γ(q,a)={q′/γ(q,a,q′):q′∈δ(q,a)}是一個(gè)權(quán)函數(shù)的集合,其元素表示為q′/γ(q,a,q′),目的是清楚地表明權(quán)函數(shù)值γ(q,a,q′)對應(yīng)轉(zhuǎn)換到達(dá)的目標(biāo)狀態(tài)為q′。
加權(quán)有限自動(dòng)機(jī)與經(jīng)典的有限自動(dòng)機(jī)的區(qū)別是:加權(quán)有限自動(dòng)機(jī)對每個(gè)轉(zhuǎn)換定義了相應(yīng)的轉(zhuǎn)換代價(jià),稱為權(quán)函數(shù)。此外,對于每個(gè)初始狀態(tài)和接受狀態(tài)也都定義了權(quán)值。
為了定義加權(quán)有限自動(dòng)機(jī)的接受語言,將δ擴(kuò)充為δ?P(Q)×Σ×P(Q),對于P?Q,a∈Σ,定義:
進(jìn)一步將δ擴(kuò)充為δ?Q×Σ*×P(Q),對于任意q∈Q,w∈Σ*,a∈Σ,作如下定義:
δ(q,ε)={q}
定義2設(shè)M=(Q,Σ,δ,qI,F,γ,i,f)是一個(gè)WFA。M所接受(識(shí)別)的語言L(M)定義為:
L(M)={x:x∈Σ*且δ(qI,x)∩F≠?}
不難看出,加權(quán)自動(dòng)機(jī)的接受語言的定義與經(jīng)典的自動(dòng)機(jī)接受語言定義類似,然而加權(quán)自動(dòng)機(jī)不僅能描述所識(shí)別的字符串,而且還能給出每個(gè)識(shí)別字符串的權(quán)重。
同樣地,我們也對權(quán)函數(shù)γ進(jìn)行相應(yīng)的擴(kuò)展, 對于任意q∈Q,w∈Σ*,a∈Σ,定義:
γ(δ(q,ε,q))=0
(1)
γ(δ(q,wa,q′))=min{γ(δ(q,w,p))+
γ(δ(p,a,q′)):p∈δ(q,w)}
(2)
其中,式(2)表示:所有從狀態(tài)q出發(fā)先處理w后到達(dá)某一狀態(tài),然后經(jīng)由該狀態(tài)識(shí)別a到達(dá)狀態(tài)q′的運(yùn)行過程的權(quán)值之和組成的集合的最小元素值。
定義3設(shè)M=(Q,Σ,δ,qI,F,γ,i,f)是一個(gè)WFA,x∈L(M)。x被M接受的權(quán)值定義為:
W(M,x)=i(qI)+min{γ(δ(qI,x,qf))+f(qf):qf∈(δ(qI,x)∩F)}
下面我們用例子去闡述以上的定義。
例1如圖1所示,一個(gè)WFAM=({q0,q1,q2,q3},{a,b,c,d},δ,q0,{q3},γ,i,f),其中轉(zhuǎn)換關(guān)系δ表示如下:
δ(q0,a)={q0,q1,q2}δ(q0,b)={q1,q2}δ(q0,c)={q2}
δ(q0,d)={q3}δ(q1,b)={q1,q2}δ(q1,c)={q2}
δ(q1,d)={q3}δ(q2,c)={q2}δ(q2,d)={q3}
相應(yīng)的權(quán)函數(shù)γ表示如下:
γ(q0,a)={q0/7,q1/8,q2/11}γ(q0,b)={q1/9,q2/11}
γ(q0,c)={q2/11}γ(q0,d)={q3/13}
γ(q1,b)={q1/8,q2/10}γ(q1,c)={q2/11}
γ(q1,d)={q3/12}γ(q2,c)={q2/9}γ(q2,d)={q3/10}
初始狀態(tài)的權(quán)值:i(q0)=2,終態(tài)權(quán)函數(shù):f(q3)=1。
顯然,acd∈L(M),因?yàn)棣?q0,acd)∩F={q3}≠?。據(jù)此,我們有:
γ(q0,acd,q3)=min{γ(q0,ac,q2)+γ(q2,d,q3)}
=min{min{(γ(q0,a,q2)+γ(q2,c,q2)),
(γ(q0,a,q1)+γ(q1,c,q2))}+10}
=min{min{(11+9),(8+11)}+10}
=min{19+10}=29
根據(jù)定義3,我們可以得到:
W(M,acd)=i(q0)+min{γ(q0,acd,q3)+f(q3)}
=2+min{29+1}
=32
所以,acd被M接受的權(quán)值為32。
現(xiàn)在我們引入另一種加權(quán)有限自動(dòng)機(jī)模型,帶空移動(dòng)的加權(quán)有限狀態(tài)自動(dòng)機(jī),如圖1所示。
圖1 不帶ε移動(dòng)的WFA
定義4一個(gè)帶空移動(dòng)的加權(quán)有限自動(dòng)機(jī)ε-WFA(weighted finite automata with ε-moves)M′是一個(gè)8元組:
M′=(Q,Σ,δ,qI,F,γ,i,f)
其中,Q,Σ,qI,F,γ,i,f的意義與定義1相同,所不同的是轉(zhuǎn)換關(guān)系δ?Q×(Σ∪{ε})×Q。也就是說,對于q∈Q,允許q做一個(gè)空移動(dòng)(ε移動(dòng))而到達(dá)其他的狀態(tài)。
類似地,下面我們將δ擴(kuò)充為δ*?Q×Σ*×Q,對于P?Q,q∈Q,w∈Σ*,a∈Σ,定義:
ε-closure(q)={p:狀態(tài)q經(jīng)若干個(gè)ε可達(dá)p}
(3)
δ*(q,ε)=ε-closure(q)
(4)
(5)
δ*(q,wa)=δ*(δ(δ*(q,w),a),ε)
(6)
其中,式(6)表示:從狀態(tài)q出發(fā)先處理w后到達(dá)某一狀態(tài),然后經(jīng)由該狀態(tài)識(shí)別a到達(dá)的狀態(tài)集合。特別地,當(dāng)w=ε時(shí),我們有:δ*(q,a)=δ*(δ(δ*(q,ε),a),ε)。
定義5設(shè)M′=(Q,Σ,δ,qI,F,γ,i,f)是ε-WFA,則M′所識(shí)別的語言:
L(M′)={x:x∈Σ*且δ*(qI,x)∩F≠?}
同樣地,我們也對ε-WFA的權(quán)函數(shù)γ擴(kuò)展為γ*:δ*→R+, 對于任意q∈Q,w∈Σ*,a∈Σ,定義:
γ*(δ*(q,a,p))=min{γ(δ(q,a,p)):(q,a,p)∈δ*}
(7)
γ*(δ*(q,wa,q′))=min{γ*(δ*(q,wp))+
γ*(δ*(p,a,q′)):p∈δ*(q,w)}
(8)
其中,式(8)表示:從狀態(tài)q出發(fā)先處理w后到達(dá)某一狀態(tài),然后經(jīng)由該狀態(tài)識(shí)別a到達(dá)狀態(tài)q′的運(yùn)行過程的權(quán)值之和,包含了計(jì)算空字符ε的權(quán)值。相同的字符串有多個(gè)權(quán)值,取最小值。
例2如圖2所示,M′是一個(gè)ε-WFA,求γ*(δ*(q0,bd,q3))值。
圖2 帶ε移動(dòng)的WFA
由于:
δ*(q0,b)=δ*(δ(δ*(q0,ε),b),ε)
=δ*(δ({q0,q1,q2},b),ε)
=δ*({q1},ε)={q1,q2}
所以:
γ*(δ*(q0,b,q1))=min{γ(δ(q0,b,q1))}
=min{γ(q0,ε,q1)+γ(q1,b,q1)}
=min{1+8}=9
同理可得,γ*(δ*(q1,d,q3))=12,γ*(δ*(q0,b,q2))=11,γ*(δ*(q2,d,q3))=10。
因此:
γ*(δ*(q0,bd,q3))=min{(γ*(δ*(q0,b,q1))+γ*(δ*(q1,
d,q3))),(γ*(δ*(q0,b,q2))+
γ*(δ*(q2,d,q3)))}
=min{(9+12),(11+10)}=21
定義6設(shè)M′=(Q,Σ,δ,qI,F,γ,i,f)是一個(gè)ε-WFA,x∈L(M′)。x被M′接受的權(quán)值為:
W(M′,x)=i(qI)+min{γ*(δ*(qI,x,qf))+f(qf):
qf∈(δ*(qI,x)∩F)}
例3如圖2所示,M′是一個(gè)ε-WFA,顯然有:bd∈L(M′),因?yàn)棣?(q0,bd)∩F={q3}≠?,根據(jù)定義6,我們可知:
W(M′,bd)=i(q0)+min{γ*(δ*(q0,bd,q3))+f(q3)}
=2+min{21+1}
=24
因此,bd被M′接受的權(quán)值為24。
以下我們給出一個(gè)判斷兩個(gè)加權(quán)自動(dòng)機(jī)是否等價(jià)的標(biāo)準(zhǔn):
定義7設(shè)任意兩個(gè)WFAM和M′,如果有L(M)=L(M′)且當(dāng)x∈L(M)時(shí)有W(M,x)=W(M′,x),那么就稱M和M′量化等價(jià)。
在經(jīng)典有限自動(dòng)機(jī)理論中,對于任意一個(gè)帶空移動(dòng)的有限自動(dòng)機(jī),可以構(gòu)造一個(gè)等價(jià)的不帶空移動(dòng)的有限自動(dòng)機(jī),使得兩者識(shí)別的語言相同。那么,對于加權(quán)自動(dòng)機(jī)是否也有類似的結(jié)論。也就是說,對于任意一個(gè)ε-WFAA,是否存在一個(gè)與之量化等價(jià)的WFAB是下文將研究解決的問題。
為了解決這個(gè)問題,我們來探討WFAB的構(gòu)造過程。我們注意到,ε-WFAA和WFAB的區(qū)別在于前者允許有空移動(dòng),而對于一個(gè)語言的句子來說,除非ε單獨(dú)作為一個(gè)句子,否則空移動(dòng)ε不會(huì)影響句子本身。所以,考慮將A在識(shí)別句子過程中遇到類似于ε*aε*(a的前后各有若干個(gè)ε,a∈Σ)的字符串時(shí),在B中用一個(gè)輸入字符為a的非空轉(zhuǎn)換替換。此外,如果ε-WFA的語言中包含句子ε,則將B的初始狀態(tài)同時(shí)也設(shè)為終態(tài),讓B也可以識(shí)別句子ε,這樣可保證L(A)=L(B)成立。另一方面,在構(gòu)造B時(shí),使得B中的輸入字符a的權(quán)值等于A中串ε*aε*的權(quán)值之和,那么也可以保證W(A,x)=W(B,x)成立。也就是說,由于W(A,x)表示x在其運(yùn)行路徑上的所有轉(zhuǎn)換的權(quán)值之和,如果構(gòu)造WFAB,滿足使B的每一次轉(zhuǎn)換的輸入字符a(a≠ε)及其權(quán)函數(shù)γ的值都與A相同,那么必有L(A)=L(B)且W(A,x)=W(B,x)成立。
命題1設(shè)A=(Q,Σ,δA,qI,FA,γA,i,fA)是一個(gè)ε-WFA。我們構(gòu)造一個(gè)WFAB=(Q,Σ,δB,qI,FB,γB,i,fB)如下:
(1) 對于A中的Q,Σ,qI,i在B中保持不變。
(3) 終態(tài)集FB:如果ε∈L(A),F(xiàn)B=FA∪{qI},否則FB=FA。
(4) 終態(tài)權(quán)函數(shù)fB:如果ε∈L(A)時(shí),fB(qI)=W(A,ε)-i(qI),否則,對于所有q∈FA,使fB(q)=fA(q)。
那么,對于A和B有以下結(jié)論成立:
(1) L(A)=L(B);
(2) 對于任意x∈L(A),有W(A,x)=W(B,x)。
證明對于結(jié)論1的證明,參見文獻(xiàn)[3]。下面證明結(jié)論2成立。為此,我們需要先證明以下的結(jié)論1和結(jié)論2成立。
首先我們用數(shù)學(xué)歸納法證明結(jié)論1成立。
2) 假定|x|=n時(shí),上式成立。當(dāng)|x|=n+1時(shí),不妨設(shè)x=wa,這里|w|=n,a∈Σ,則有:
構(gòu)造步驟(2)
歸納假設(shè)
=δB(qI,wa)
因此當(dāng)|x|=n+1時(shí),結(jié)論1成立。
接下來,我們也用數(shù)學(xué)歸納法證明結(jié)論2成立。
γB(δB(qI,x,p))=γB(δB(qI,wa,p))
=min{γB(δB(qI,w,q′))+γB(δB(q′,a,p)):
q′∈δB(qI,w)}
=min{γB(δB(qI,w,q′))+γB(δB(q′,a,p)):
結(jié)論1
歸納假設(shè)
構(gòu)造步驟(2)
由1)、2)可得,結(jié)論2成立。
現(xiàn)在我們可以證明:對于任意x∈L(A),有W(A,x)=W(B,x)成立。同樣用數(shù)學(xué)歸納法證明。
1) 當(dāng)|x|=0時(shí),即當(dāng)x=ε的情況:
W(B,ε)=i(qI)+γ(δ(qI,ε,qI))+f(qI)
=i(qI)+f(qI)
=i(qI)+W(A,ε)-i(qI)
構(gòu)造步聚(4)
=W(A,ε)
所以,當(dāng)ε∈L(A)時(shí),結(jié)論W(A,ε)=W(B,ε)成立。
2) 當(dāng)|x|≥1時(shí),即當(dāng)x≠ε的情況:
=i(qI)+min{γB(δB(qI,x,p))+fA(p):p∈
結(jié)論2
=i(qI)+min{γB(δB(qI,x,p))+fA(p):p∈
(δB(qI,x)∩FA)}
結(jié)論1
=i(qI)+min{γB(δB(qI,x,p))+fA(p):p∈
(δB(qI,x)∩FB)}
步驟(3)
=i(qI)+min{γB(δB(qI,x,p))+fB(p):p∈
(δB(qI,x)∩FB)}
步驟(4)
=W(B,x)
定義3
所以,對于?x∈L(A)(x≠ε),有W(A,x)=W(B,x)成立。
綜合1)和2)得到:?x∈L(A),W(A,x)=W(B,x)成立。
根據(jù)以上結(jié)論,我們得到本文一個(gè)主要結(jié)論 。
定理1任意一個(gè)ε-WFA總存在一個(gè)與之量化等價(jià)的WFA。
表1 ε-WFA A中的δ*和γ*
前文介紹了如何將ε-WFA轉(zhuǎn)換成與之量化等價(jià)的WFA,下面探討轉(zhuǎn)換的算法實(shí)現(xiàn)。根據(jù)構(gòu)造過程可知,構(gòu)造WFA的主要任務(wù)是構(gòu)造步驟(2):對于ε-WFA中所有的(q,a)∈Q×Σ,計(jì)算出δ*(q,a)=δ*(δ(δ*(q,ε),a),ε)和相應(yīng)的γ*(δ*(q,a))值。據(jù)此,設(shè)計(jì)出相應(yīng)的轉(zhuǎn)換算法,如算法1所示:
算法1ε-WFA2WFA算法
輸入:ε-WFAA=(Q,Σ,δ,qI,F,γ,i,f)
輸出:WFAB=(Q,Σ,δ′,qI,F′,γ′,i,f′)
1:F′=F;f′=f;δ′=?;
2:γ′=?;
3:forall{q∈Q}
4:forall{a∈Σ}
5:InitQueue(W);InitQueue(W′);
6:Enqueue(W,);
//添加初始項(xiàng),使W≠?
7:while(W≠?)do
8:=Dequeue(W);
//這里α一定為ε
9:ifδ(q2,ε)≠?then
10:forall{q3∈δ(q2,ε)}
11:v=v+γ(q2,ε,q3);
12:Enqueue(W,);
13:ifq3∈Fthen
14:F′=F∪{qI};f′(qI)=v-i(qI);
15:else//δ(q2,ε)=?,即q2后不含空移動(dòng)
16:Enqueue(W′,);
17://此時(shí),W′中存放的元素,q2∈δ*(q,ε)
18:while(W′≠?)do
19:=Dequeue(W′);
20:ifα=ε&δ(q2,a)≠?then
21:forallq3∈δ(q2,a)
22:δ′=δ′∪{δ(q,a,q3)};v1=v1+γ(q2,a,q3);
23:γ′=γ′∪{v1=γ(q,a,q3)};
24:Enqueue(W,);
25://此時(shí),W中存放元素,q2∈δ(δ*(q,ε),a)
26:while(W≠?)do
27:=Dequeue(W);
28:ifδ(q2,ε)≠?then
29:forall{q3∈δ(q2,ε)}
30:v=v+γ(q2,ε,q3);Enqueue(W,);
31:δ′=δ′∪{δ(q,a,q3)};γ′=γ′∪{v=γ(q,a,q3)};
我們輪流使用2個(gè)工作隊(duì)列W和W′,隊(duì)列的每一個(gè)元素中存放轉(zhuǎn)換函數(shù)及相應(yīng)的權(quán)值,任一元素共有4個(gè)參數(shù)組成。其中前3個(gè)參數(shù)表示轉(zhuǎn)換函數(shù)(q,α,q2)∈δ,第4個(gè)參數(shù)為轉(zhuǎn)換的權(quán)值v=γ(q,α,q2),這里q,q2∈Q,α∈(Σ∪{ε})。
算法的第5行對隊(duì)列W和W′作初始化,第6行給W添加一個(gè)特殊元素,使得其后的循環(huán)條件W≠?成立。
算法的第7-16行,主要利用隊(duì)列W由q求算δ*(q,ε),存入W′。重復(fù)從隊(duì)列W中取出每一個(gè)元素(第8行):如果該元素(轉(zhuǎn)換)的后繼轉(zhuǎn)換仍為帶空移動(dòng)的轉(zhuǎn)換時(shí)(第9行),則將后繼入隊(duì)(第12行),在此過程中,若到達(dá)了終態(tài)(第13行)則將qI置為終態(tài)并設(shè)定終態(tài)權(quán)值(第14行),這段代碼對應(yīng)構(gòu)造過程的步驟(3)和(4);否則,意味著完成了δ*(q,ε)計(jì)算,則將元素轉(zhuǎn)移到W′中保存(第15、16行),循環(huán)結(jié)束后W′中存放的元素為:,滿足q2∈δ*(q,ε)。
算法的第18-24行,從W′中取出所有元素即轉(zhuǎn)換δ*(q,ε)(第19行),求算δ(δ*(q,ε),a),存入隊(duì)列W中。
算法的第25-31行,從W中取出所有元素即轉(zhuǎn)換δ(δ*(q,ε),a)(第27行),求算δ*(δ(δ*(q,ε),a),ε),結(jié)果存入隊(duì)列W中。
整個(gè)算法圍繞求算δ*(q,a)=δ*(δ(δ*(q,ε),a),ε)和γ*(δ*(q,a))之值,在這個(gè)過程中完成對F′、f′、δ′、γ′的構(gòu)造。
復(fù)雜度分析我們注意到算法主要是處理隊(duì)列中的元素,算法的復(fù)雜度主要由入隊(duì)的次數(shù)決定,即由語句Enqueue(W,)決定。該語句在算法中共出現(xiàn)4次,12行、16行、24行和30行。在不考慮外層循環(huán)(第3、4行)的情況下,第12行最多執(zhí)行|Q|2次,因?yàn)闈M足循環(huán)條件的狀態(tài)q3(第10行)最多有|Q|個(gè),而且這些元素中的任意一個(gè)也可能有|Q|個(gè)帶空移動(dòng)的轉(zhuǎn)換需要加入到隊(duì)列W中;第16行也最多執(zhí)行|Q|2次,因?yàn)樵撔兄皇菍中所有元素轉(zhuǎn)移至W′中;第24行最多執(zhí)行|Q|次,因?yàn)闈M足循環(huán)條件的狀態(tài)q3(第21行)最多有|Q|個(gè);第31行最多執(zhí)行|Q|2次,原因同第12行。共執(zhí)行3|Q|2+|Q|次,考慮外層循環(huán),總共|Q|·|Σ|·(3|Q|2+|Q|)次。所以時(shí)間復(fù)雜度為O(|Q|3·|Σ|)。
本文針對加權(quán)自動(dòng)機(jī)的等價(jià)性問題提出了量化等價(jià)的概念,研究和探討如何將一個(gè)帶空移動(dòng)的加權(quán)有限自動(dòng)機(jī)轉(zhuǎn)換為一個(gè)與之量化等價(jià)的不帶空移動(dòng)的加權(quán)有限自動(dòng)機(jī),研究結(jié)果表明轉(zhuǎn)換前后兩者是量化等價(jià)的。
[1] Hopcroft J E,Ullman J D.Introduction to Automata Theory,Languages,and Computation[M].MA:Pearson Education India,1979.
[2] 蔣宗禮.形式語言與自動(dòng)機(jī)理論[M].2版.北京:清華大學(xué)出版社,2007.
[3] 張晉津.轉(zhuǎn)換系統(tǒng)行為近似等價(jià)性的研究[D].南京航空航天大學(xué),2010.
[4] 潘海玉.狀態(tài)轉(zhuǎn)化系統(tǒng)的格值量化驗(yàn)證方法研究[D].上海:華東師范大學(xué),2012.
[5] Pan H Y,Cao Y Z,Zhang M,et al.Simulation for lattice-valued doubly labeled transition systems[J].International Journal of Approximate Reasoning,2014,55(3):797-811.
[6] Pan H Y,Zhang M,Wu H Y,et al.Quantitative analysis of lattice-valued Kripke structures[J].Fundamenta Informaticae,2014,135(3):269-293.
[7] Pan H Y,Li Y M,Cao Y Z.Lattice-valued simulations for quantitative transition systems[J].International Journal of Approximate Reasoning,2015,56(2):28-42.
[8] 李永明.模糊系統(tǒng)分析[M].北京:科學(xué)出版社,2005.
[9] Li Y M.Finite automata theory with membership values in lattices[J].Information Sciences,2011,181(5):1003-1017.
[10] Li Z H,Li P,Li Y M.The relationships among several types of fuzzy automata[J].Information Sciences,2006,176(15):2208-2226.
[11] Cao Y Z,Yoshinori E.Nondeterministic fuzzy automata[J].Information Sciences,2012,191(15):86-97.
[12] Chatterjee K,Doyen L,Henzinge T.Quantitative languages[J].ACM Transactions on Computational Logic,2010,11(4):1-38.
[13] Chatterjee K,Doyen L,Henzinger T A.Expressiveness and closure properties for quantitative languages[J].Logical Methods in Computer Science,2010,6(3):199-208.
[14] Aminof B,Kupferman O,Lampert R.Rigorous approximated determinization of weighted automata[J].Theoretical Computer Science,2013,480(8):104-117.
[15] Boker U,Henzinger T.Exact and approximate determinization of discounted-sum automata[J].Logical Methods in Computer Science,2014,10(1):1-33.
[16] 黃明璋,李國強(qiáng).基于模型檢測的并發(fā)程序分析綜述[J].計(jì)算機(jī)應(yīng)用與軟件,2014,31(12):1-6,24.
[17] 袁志斌.Büchi自動(dòng)機(jī)的優(yōu)化綜述[J].計(jì)算機(jī)應(yīng)用與軟件,2010,27(6):32-34,88.
QUANTITATIVE EQUIVALENCE OF WEIGHTED FINITE AUTOMATA WITH ε-MOVES AND ITS TRANSITION
Wang Guowu
(SchoolofComputerandInformation,AnhuiPolytechnicalUniversity,Wuhu241000,Anhui,China) (KeyLaboratoryofComputerApplicationTechnology,AnhuiPolytechnicUniversity,Wuhu241000,Anhui,China)
In classical finite automaton theory, the finite automaton with ε-moves and normal finite automaton are equivalent. The weighted finite automaton valued in real numbers is an extension model of automaton, it assigns one weight valued in real numbers to every transition of classical automaton, these weights denote the cost of transitions execution. To study whether the finite automaton with ε-moves and the normal finite automaton are equivalent, we introduce the concept of quantitative equivalence, and give a method of how to transform a weighted finite automaton with ε-moves to a normal weighted finite automaton in quantitative equivalence with the former. Study result shows that these two are quantitatively equivalent.
Quantitative equivalenceNondeterministic finite automataWeighted automataFormal verification
2015-01-23。國家自然科學(xué)基金項(xiàng)目(61300170);安徽省教育廳自然科學(xué)基金項(xiàng)目(KJ2013B020);安徽省優(yōu)秀青年人才基金重點(diǎn)項(xiàng)目(2013SQRL034ZD)。汪國武,講師,主研領(lǐng)域:形式化分析與驗(yàn)證。
TP301.1
A
10.3969/j.issn.1000-386x.2016.08.005