并發加權μ-演算的一致性內插

余 寒，張晉津

(南京航空航天大學 計算機科學與技術學院，江蘇 南京 210016)

0 引 言

在計算機科學領域，μ-演算是一種廣泛使用的邏輯[1-3]。命題μ-演算由Kozen[4]提出，通過帶不動點算子的公式來表達轉移系統[5-7]的性質，是一種表達能力很強的邏輯語言。并發加權μ-演算(concurrent weightedμ-calculus，CWC)，通過將不動點操作符加入并發加權邏輯[8](concurrent weighted logic，CWL)擴充而來，是一種帶有不動點的多模態邏輯，能夠應對組合性標記加權轉移系統(labeled weighted transition system，LWS)。

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

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

1 預備知識

本節給出文中使用的一些符號和基本概念，介紹CWC的語法及LWS語義。

1.1 標記加權轉移系統

定義1[8,11](標記加權轉移系統)：LWS是一個五元組W=(M,Σ,θ,l,ρ)，其中

(1)M是一個非空的狀態集；

(2)Σ是一個非空動作集；

(3)θ:M×(Σ×)→2M是一個狀態轉移函數；

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

(5)ρ:Q→2M是一個關于命題變元集合Q的解釋函數。對于p∈Q，N?M，解釋函數ρ[p|→N]滿足下列條件：如果p'=p，則ρ[p|→N](p')=N；如果p'≠p，則ρ[p|→N](p')=ρ(p')。

對于任意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是一個關于命題變元集合Q{q}的解釋函數。定點LWS是一個二元組(W,m)，m是W中的一個狀態。

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

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

如果存在一個加權互模擬關系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改為“對于q∈P?Q，m∈ρ(q)當且僅當m'∈ρ(q)”，則對應關系變為P-互模擬，記作～P。

定義3(LWSs乘積)：給定同步函數[13]*:Σ×Σ→Σ,以及任意兩個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→是滿足以下條件的函數：如果(m0,m1)∈M，則l((m0,m1))=l0(m0)+l1(m1)；

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

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

容易驗證W0?W1是個LWS。

1.2 并發加權μ-演算

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

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

在形如μp?,νp?這樣的公式中，要求變量p在?中正出現(也即，p不出現)。不動點操作符是量詞，free(?)是所有出現在?中的自由變元的集合。如果?中的每個命題變元p只被限制一次并且每個p在其限制量詞的轄域內，則?是范式形式。對于范式形式公式?中的受限變元p，?的唯一的子公式ηp?(η∈{μ,ν})記作?p。每個公式可以通過重命名受限變元形成等價的范式形式。下文中的CWC公式均指其范式形式。CWC公式在LWS上的解釋見圖1。

1.3 輪替樹自動機

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

(1)S是一個有限的狀態集合；

(2)s0∈S是一個初始狀態；

(3)Ω:S→ω是一個優先級函數；

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

圖1 CWC的LWS語義解釋

輪替樹自動機的計算行為用執行(run)的概念來解釋。輪替樹自動機W=(S,s0,δ,Ω)在(W,m0)上的一次執行是樹R=(V,E,λ)，其中(V,E)是定義樹的二元組，而λ:V→M×S是一個雙標記函數。該樹的根節點標記為(m0,s0),帶有雙標記(m,s)的節點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'')。

對于每一個R的無限分支π,將優先級函數Ω應用到每個節點上，對于所得到的自然數序列，當其中無限次出現的最大自然數是偶數，這個分支能夠被接收。如果R的每個無限分支是可接收的，則R是可接收的。當一個定點LWS上存在一個關于W可接收的執行，則這個系統是能夠被W接收的。

1.4 展 開

2 CWC上的一致性內插

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

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

(1)?|=θ；

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

一致性內插定理在CWC上成立，意味著當適當條件成立時，可以為每個CWC公式找到一個一致性插值。

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

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

3 互模擬量詞

互模擬量詞在LWS上具有獨特的語義，結合互模擬量詞和輪替樹自動機，可以證明CWC上一致性內插定理成立。

定義10(互模擬量詞)：給定一個命題變元q，互模擬量詞?q是具有以下LWS語義的操作符：W,m|=?q?當且僅當存在定點LWS(W',m')使得(W,m)～q(W',m')并且W',m'|=?。

其中～q是互模擬關系除去q，即不考慮命題變元q，等價于～Q/{q}。

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

引理1的證明需要借助輪替樹自動機。

定義11(輪替樹自動機?qA)：A=(S,s0,δ,Ω)表示一個輪替樹自動機，則?qA是這樣一個輪替樹自動機?qA=(S,s0,δ-q,Ω)，其中δ-q:S→TC-q是轉移函數，TC-q=TC{q}。

引理2：令A為一個輪替樹自動機，那么對于任意定點LWS(W-q,m)，?qA接收(W-q,m)當且僅當存在定點LWS(W',m'),使得A接收(W',m')并且(W-q,m)～(W',m')-q。

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

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

4 結束語

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