余 寒，張晉津

(南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇 南京 210016)

0 引 言

在計(jì)算機(jī)科學(xué)領(lǐng)域，μ-演算是一種廣泛使用的邏輯[1-3]。命題μ-演算由Kozen[4]提出，通過(guò)帶不動(dòng)點(diǎn)算子的公式來(lái)表達(dá)轉(zhuǎn)移系統(tǒng)[5-7]的性質(zhì)，是一種表達(dá)能力很強(qiáng)的邏輯語(yǔ)言。并發(fā)加權(quán)μ-演算(concurrent weightedμ-calculus，CWC)，通過(guò)將不動(dòng)點(diǎn)操作符加入并發(fā)加權(quán)邏輯[8](concurrent weighted logic，CWL)擴(kuò)充而來(lái)，是一種帶有不動(dòng)點(diǎn)的多模態(tài)邏輯，能夠應(yīng)對(duì)組合性標(biāo)記加權(quán)轉(zhuǎn)移系統(tǒng)(labeled weighted transition system，LWS)。

為了處理CWC上的一致性內(nèi)插定理，引入二階量詞互模擬?；ツM量詞由Andrew M. Pitts提出[9]，隨后被用作工具來(lái)證明模態(tài)邏輯中一致性內(nèi)插定理，繼而延伸到模態(tài)μ-演算的一致性內(nèi)插定理的證明。一致性內(nèi)插定理能夠推出Craig內(nèi)插[10]，是它的加強(qiáng)版本，可以有效表達(dá)模塊化。

文中介紹了CWC的語(yǔ)法和語(yǔ)義模型，以及展開的概念，闡述了CWC上的一致性內(nèi)插定理，引入互模擬量詞并證明一致性內(nèi)插定理在CWC上成立。

1 預(yù)備知識(shí)

本節(jié)給出文中使用的一些符號(hào)和基本概念，介紹CWC的語(yǔ)法及LWS語(yǔ)義。

1.1 標(biāo)記加權(quán)轉(zhuǎn)移系統(tǒng)

定義1[8,11](標(biāo)記加權(quán)轉(zhuǎn)移系統(tǒng))：LWS是一個(gè)五元組W=(M,Σ,θ,l,ρ)，其中

(1)M是一個(gè)非空的狀態(tài)集；

(2)Σ是一個(gè)非空動(dòng)作集；

(3)θ:M×(Σ×)→2M是一個(gè)狀態(tài)轉(zhuǎn)移函數(shù)；

(4)l:M→是一個(gè)滿足下列條件的函數(shù)：如果m'∈θ(m,a,x)，則l(m')=l(m)+x。一般稱函數(shù)狀態(tài)l為標(biāo)記函數(shù)；

(5)ρ:Q→2M是一個(gè)關(guān)于命題變?cè)螿的解釋函數(shù)。對(duì)于p∈Q，N?M，解釋函數(shù)ρ[p|→N]滿足下列條件：如果p'=p，則ρ[p|→N](p')=N；如果p'≠p，則ρ[p|→N](p')=ρ(p')。

對(duì)于任意LWSW=(M,Σ,θ,l,ρ)，p∈Q，N?M，W[p|→N]表示這樣的LWS：W[p|→N]=(M,Σ,θ,l,ρ[p|→N])。W-q表示這樣的LWS：W-q=(M,Σ,θ,l,ρ-q)，其中ρ-q:Q{q}→2M是一個(gè)關(guān)于命題變?cè)螿{q}的解釋函數(shù)。定點(diǎn)LWS是一個(gè)二元組(W,m)，m是W中的一個(gè)狀態(tài)。

定義2[8,12](加權(quán)互模擬)：給定一個(gè)LWSW=(M,Σ,θ,l,ρ)，一個(gè)加權(quán)互模擬是關(guān)系R?M×M,其中任意(m,m')∈R滿足下列條件：

(1)l(m)=l(m')；

如果存在一個(gè)加權(quán)互模擬關(guān)系R使得(m,m')∈R，則m和m'是互模擬的，記作m～m'。若Wi=(Mi,Σi,θi,li,ρi),mi∈Mi,i=0,1且m0和m1互模擬，則(W0,m0)～(W1,m1)。

將上述條件4改為“對(duì)于q∈P?Q，m∈ρ(q)當(dāng)且僅當(dāng)m'∈ρ(q)”，則對(duì)應(yīng)關(guān)系變?yōu)镻-互模擬，記作～P。

定義3(LWSs乘積)：給定同步函數(shù)[13]*:Σ×Σ→Σ,以及任意兩個(gè)LWS，Wi=(Mi,Σi,θi,li,ρi)，i=0,1。W=(M,Σ,θ,l,ρ)是W0和W1的乘積，記W=W0?W1，其中:

(1)M=M0×M1；

(2)Σ=Σ0*Σ1={a0*a1|a0∈Σ0,a1∈Σ1}；

(3)l:M→是滿足以下條件的函數(shù)：如果(m0,m1)∈M，則l((m0,m1))=l0(m0)+l1(m1)；

(4)θ:M×(Σ×)→2M是滿足以下條件的函數(shù)：如果(m0,m1)∈M,a∈Σ,x∈,則x=x0+x1,a=a0+a1}；

(5)ρ:Q→2M是滿足以下條件的函數(shù)：ρ(q)={(m0,m1)∈M|m0∈ρ0(q),m1∈ρ1(q)}。

容易驗(yàn)證W0?W1是個(gè)LWS。

1.2 并發(fā)加權(quán)μ-演算

定義4(基本公式)：CWC的公式由以下BNF范式定義，其中r∈{,≥}，

?::=p|?∨?|?∧???|?|?|μp?|νp?。

在形如μp?,νp?這樣的公式中，要求變量p在?中正出現(xiàn)(也即，p不出現(xiàn))。不動(dòng)點(diǎn)操作符是量詞，free(?)是所有出現(xiàn)在?中的自由變?cè)募?。如?中的每個(gè)命題變?cè)猵只被限制一次并且每個(gè)p在其限制量詞的轄域內(nèi)，則?是范式形式。對(duì)于范式形式公式?中的受限變?cè)猵，?的唯一的子公式ηp?(η∈{μ,ν})記作?p。每個(gè)公式可以通過(guò)重命名受限變?cè)纬傻葍r(jià)的范式形式。下文中的CWC公式均指其范式形式。CWC公式在LWS上的解釋見圖1。

1.3 輪替樹自動(dòng)機(jī)

定義5[15-16](輪替樹自動(dòng)機(jī))：輪替樹自動(dòng)機(jī)是一個(gè)四元組W=(S,s0,δ,Ω),其中:

(1)S是一個(gè)有限的狀態(tài)集合；

(2)s0∈S是一個(gè)初始狀態(tài)；

(3)Ω:S→ω是一個(gè)優(yōu)先級(jí)函數(shù)；

(4)δ:S→TC是轉(zhuǎn)移函數(shù)。集合TC是滿足下列條件的最小的集合：如果r∈，則如果q∈Q,則q,q∈TC；如果s∈S，則如果s,s'∈S，則s∧s',s∧s',s|s'∈TC。

圖1 CWC的LWS語(yǔ)義解釋

輪替樹自動(dòng)機(jī)的計(jì)算行為用執(zhí)行(run)的概念來(lái)解釋。輪替樹自動(dòng)機(jī)W=(S,s0,δ,Ω)在(W,m0)上的一次執(zhí)行是樹R=(V,E,λ)，其中(V,E)是定義樹的二元組，而λ:V→M×S是一個(gè)雙標(biāo)記函數(shù)。該樹的根節(jié)點(diǎn)標(biāo)記為(m0,s0),帶有雙標(biāo)記(m,s)的節(jié)點(diǎn)v滿足下列條件：

(1)如果δ(s)=q,則m∈ρ(q)；如果δ(s)≠q，則m?ρ(q)；

(3)如果δ(s)=s',則存在v'∈Scc(v),使得λ(v')=(m,s')；

(6)如果δ(s)=s'∨s''，則存在v'∈Scc(v)，使得λ(v')=(m,s')或者λ(v'')=(m,s'')；

(7)如果δ(s)=s'∧s''，則存在v',v''∈Scc(v)，使得λ(v')=(m,s')并且λ(v'')=(m,s'')；

(8)如果δ(s)=s'|s''，存在v',v''∈Scc(v)和m',m''∈M，使λ(v')=(m',s')并且λ(v'')=(m'',s'')。

對(duì)于每一個(gè)R的無(wú)限分支π,將優(yōu)先級(jí)函數(shù)Ω應(yīng)用到每個(gè)節(jié)點(diǎn)上，對(duì)于所得到的自然數(shù)序列，當(dāng)其中無(wú)限次出現(xiàn)的最大自然數(shù)是偶數(shù)，這個(gè)分支能夠被接收。如果R的每個(gè)無(wú)限分支是可接收的，則R是可接收的。當(dāng)一個(gè)定點(diǎn)LWS上存在一個(gè)關(guān)于W可接收的執(zhí)行，則這個(gè)系統(tǒng)是能夠被W接收的。

1.4 展 開

2 CWC上的一致性內(nèi)插

定義8 (局部后承)：給定兩個(gè)CWC公式?和ψ，ψ是?的局部后承(記作?|=ψ)，那么對(duì)于任意定點(diǎn)LWS(W,m)，如W,m|=?，則W,m|=ψ。

定義9(一致性插值)：令?為任意CWC公式，并且O?free(?)。那么?關(guān)于O的一致性插值是滿足如下條件的公式θ：

(1)?|=θ；

(2)如果?|=ψ并且free(?)∩free(ψ)?O，那么θ|=ψ；free(θ)?O。

一致性內(nèi)插定理在CWC上成立，意味著當(dāng)適當(dāng)條件成立時(shí)，可以為每個(gè)CWC公式找到一個(gè)一致性插值。

定理1(一致性內(nèi)插定理)：任意CWC公式都有一個(gè)一致性插值。

證明定理1，需要借助互模擬量詞。

3 互模擬量詞

互模擬量詞在LWS上具有獨(dú)特的語(yǔ)義，結(jié)合互模擬量詞和輪替樹自動(dòng)機(jī)，可以證明CWC上一致性內(nèi)插定理成立。

定義10(互模擬量詞)：給定一個(gè)命題變?cè)猶，互模擬量詞?q是具有以下LWS語(yǔ)義的操作符：W,m|=?q?當(dāng)且僅當(dāng)存在定點(diǎn)LWS(W',m')使得(W,m)～q(W',m')并且W',m'|=?。

其中～q是互模擬關(guān)系除去q，即不考慮命題變?cè)猶，等價(jià)于～Q/{q}。

引理1：給定一個(gè)命題變?cè)猶，存在映射關(guān)系?q:L→L，使得對(duì)于任意CWC公式?∈L，?q?滿足定義10，并且free(?q?)=free(?){q}。

引理1的證明需要借助輪替樹自動(dòng)機(jī)。

定義11(輪替樹自動(dòng)機(jī)?qA)：A=(S,s0,δ,Ω)表示一個(gè)輪替樹自動(dòng)機(jī)，則?qA是這樣一個(gè)輪替樹自動(dòng)機(jī)?qA=(S,s0,δ-q,Ω)，其中δ-q:S→TC-q是轉(zhuǎn)移函數(shù)，TC-q=TC{q}。

引理2：令A(yù)為一個(gè)輪替樹自動(dòng)機(jī)，那么對(duì)于任意定點(diǎn)LWS(W-q,m)，?qA接收(W-q,m)當(dāng)且僅當(dāng)存在定點(diǎn)LWS(W',m'),使得A接收(W',m')并且(W-q,m)～(W',m')-q。

斷言1：令(T,τ,t)為一個(gè)ω展開樹，其中τ:T→W-q并且(T,τ,t)能夠被?qA接收。那么存在映射τ+:T→W,使得τ=(τ+)-q并且A接收(T,τ+,t)。

定理1的證明：固定CWC公式?和集合O，令q1,…,qn為?中不在O中的自由變?cè)?，也即{q1,…,qn}=free(?)O。易證?q1,…,?qn.?就是?關(guān)于O的一致性插值。

4 結(jié)束語(yǔ)

CWL在模塊化系統(tǒng)建模方面效果明顯，為了進(jìn)一步增強(qiáng)CWL的表達(dá)能力，提出了CWC。該邏輯系統(tǒng)中包含不動(dòng)點(diǎn)算子，同時(shí)也包括了類似于時(shí)態(tài)邏輯中的模態(tài)操作符和組合模態(tài)詞。關(guān)于Craig內(nèi)插定理和一致性內(nèi)插定理，不同的邏輯采用不同的證明方法[17-19]。證明CWC上的一致性內(nèi)插定理時(shí)，引入互模擬量詞，再結(jié)合LWS上的ω展開和ω展開樹，可為CWC中的每個(gè)公式找到一致性插值。借助輪替樹自動(dòng)機(jī)和互模擬量詞，CWC上的一致性內(nèi)插被證明成立。CWC在表達(dá)能力與復(fù)雜性之間具有良好的平衡性，在處理很多問(wèn)題時(shí)表現(xiàn)出了一定優(yōu)勢(shì)。關(guān)于CWC和輪替樹自動(dòng)機(jī)，還有更多值得探究的方向，如CWC的模型檢測(cè)算法，以及輪替樹自動(dòng)機(jī)與CWC公理化間的聯(lián)系等，有待進(jìn)一步研究。