并發加權μ-演算的若干性質*

余 寒

南京航空航天大學 計算機科學與技術學院，南京 211106

1 引言

在模型檢測領域，時間自動機[1]、加權自動機[2]和加權時間自動機[3]用于建模和分析數量層面的系統性質。進程代數用來模擬模塊化的性質，但它無法表達基本布爾操作符，達不到系統規范[4]要求。像空間邏輯[5-6]、分離邏輯[7-8]、概率邏輯[9]這類模塊化邏輯對于處理并發非確定性系統很有效，但在反映系統數量層面的各種性質上還有欠缺。

為了集中處理這些問題，Larsen等人提出了并發加權邏輯[10]（concurrent weighted logic，CWL），這種多模態的邏輯中包含了反映給定狀態的資源總量和限制轉移過程的模態詞，以及能夠應對組合性系統的二元模態詞，它可以表達標記加權轉移系統（label weighted transition system，LWS）的質化、量化和模塊化的性質。基于此，本文將不動點算子加入CWL，擴充后得到并發加權μ-演算（concurrentweightedμ-calculus，CWC），并給出了輪替樹自動機[11-12]與CWC間的內在聯系，借此證明了CWC的可判定性、小模型性。

本文組織結構如下：第2章介紹相關術語以及LWS；第3章提出CWC并給出其在LWS上的語義解釋；第4章引入輪替樹自動機，并闡述了輪替樹自動機與CWC公式間的內在聯系；第5章根據第4章的研究得出CWC的相關性質；第6章總結全文。

2 預備知識

本文采用如下一些記號：?表示實數集合；?表示有理數集合；采用集合論方式定義自然數，令n為任意自然數，則n={0,1,…,n-1}，ω表示自然數集合；Q={p,q,r…}表示命題變元的集合；M×S表示集合M和集合S的笛卡爾積；|S|表示集合S的基數；|?|表示公式?的子公式集合的大小。

集合M上的有限序列是函數n→M,其中n為一個自然數；集合M上的無限序列是函數ω→M；一個序列π是有限序列或者無限序列，其長度記作|π|。樹是一個二元組 (V,E),V是節點的集合，E是V×V的子集。樹中任意節點v∈V的后繼節點的集合記作Scc(v),如果樹中某節點v∈V滿足Scc(v)=?,則該節點稱為死點。

樹T=(V,E)上的一條路徑是V上的一個序列π，該序列滿足如下條件：對于任意的i+1< |π|,(π(i),π(i+1))∈E。樹T的一個分支是從根節點開始的最大的路徑，則一個分支是始于根節點終于某死點的有限路徑或者是始于根節點的無限路徑。T↓v表示以v為根節點T的子樹。

定義1[10,13]（標記加權轉移系統）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是一個解釋函數。對于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]表示這樣的標記加權轉移系統：W[p?N]=(M,Σ,θ,l,ρ[p?N])。而定點標記加權轉移系統是一個二元組(W,m)，其中W是LWS，m是W中的一個狀態，稱作定點標記加權轉移系統的標識狀態。對于一個定點標記加權轉移系統(W,m)，W↓m表示限制在狀態m上的W 的子模型。令W1和W2為任意 LWS，W1? W2表示 W1和 W2做不相交的并所得模型。

定義2[10,14]（加權互模擬）給定一個LWSW=(M,Σ,θ,l,ρ)，一個加權互模擬是一個等價關系R?M×M，使得對于任意(m,m′)∈R，如下條件成立：

（1）l(m)=l(m′)；

（4）對于任意q∈Q，m∈ρ(q)當且僅當m′∈ρ(q)。

如果存在一個加權互模擬關系R使得(m,m′)∈R,則稱m和m′是互模擬的，記作m～m′。可以將此定義擴展為不同LWSs間的加權互模擬：若Wi=(Mi,Σi,θi,li,ρi),mi∈Mi,i=0,1且m0和m1互模擬，則 (W0,m0)～(W1,m1)。

定義3[10]（LWS乘積）給定一個同步函數[15]?:Σ×Σ→Σ以及兩個 LWSWi=(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∈ ?,則θ(m,a,x)={(m0′,

（5）ρ:Q→2M是滿足下列條件的函數：如果q∈Q，則ρ(q)={(m0,m1)∈M|m0∈ρ0(q),m1∈ρ1(q)}。

易證W0?W1是LWS。

例1圖1中展 示的是 LWSW1和 W2和其乘積W0?W1。假設a*c,a*d,b*c在同步函數中已有合法定義（b*d不合法）。狀態(m0,n0)的實數標記是m0和n0的實數標記之和。m0經動作a轉移到m2，n0經動作c轉移到n1，而a*c是轉移過程的同步，故(m0,n0)到(m2,n1)的轉移帶動作標記a*c，并且帶實數標記2，此實數標記是兩個子轉移過程的代價之和。p在m0,m1上成立，q在m0,n0上成立，r在m2,n0上成立，則在W0?W1中，q在(m0,n0)上成立。

Fig.1 LWSs and their products圖1 LWS和其乘積

3 并發加權 μ-演算

CWC能夠反映LWS的特點，并包含了不動點算子，相較CWL具有更強的表達能力。

定義4（基本公式）CWC的公式由以下BNF范式定義：

其中r∈?，a∈Σ，p∈Q，?∈{≤,≥}。在形如μp?、νp?這樣的公式中，要求變元p在?中正出現（也即，?p不出現）。

Fμ指以μ開頭的不動點公式集合，Fν則是以ν開頭的不動點公式集合。Fη是不動點公式集合，由Fμ和Fν組成。在CWC公式中，不動點操作符優先級高于組合模態詞“|”，組合模態詞優先級高于一元模態詞 [?r]a，?ra。當一個CWC公式?中的每個命題變元p最多只被限制一次并且每個p在其限制量詞的轄域內，則?是范式形式。對于一個出現在范式形式CWC公式?中的受限變元p，?的唯一的子公式ηpφ(η∈{μ,ν})記作?p。顯然，每個CWC公式可以通過在必要時重命名受限變元形成等價的范式形式。下文中的CWC公式均指其范式形式。

將CWC公式在LWS上進行解釋，對于給定LWS W=(M,Σ,θ,l,ρ)和CWC公式?，集合 ||?||W?M按歸納方式定義，見圖2。

Fig.2 LWS semantics of CWC圖2 CWC的LWS語義解釋

例2對于公式?=μq(p|(≥ 2)∨[≤ 5]aq)，在LWS W 中，||?||W表示這樣的狀態的集合，從該狀態出發，在有限步內（可能是0步），可以到達一個使得公式p|(≥2)成立的狀態。

能夠滿足公式?的定點標記加權轉移系統集合，記作||?||，則：

對于每一個CWC上的模態操作符及不動點操作符，其在||?||上的相關操作見圖3。

首先對于連接符，易知，對于任意CWC公式φ、ψ：

另外，據圖3易知，對于任意CWC公式φ、ψ：

Fig.3 Some operations on||?||圖3 ||?||上相關操作

4 輪替樹自動機與CWC的聯系

定義5[12]（輪替樹自動機）輪替樹自動機是一個四元組 A=(S,s0,δ,Ω),其中：

（1）S是一個有限的狀態集合。

（2）s0∈S是一個初始狀態。

（3）Ω:S→ω是一個優先級函數，為每個狀態指派一個自然數優先級標記。

（4）δ:S→TC是轉移函數，將每個狀態映射到集合TC上，集合TC是滿足下列條件的最小的集合：0,1 ∈TC；如果r∈ ? ，則r∈ ?,(?r),?(?r)∈TC；如果q∈Q，則q,?q∈TC；如果s∈S，則s,?ras,[?r]as∈TC；如果s,s′∈S，則s∧s′,s∧s′,s|s′∈TC。

輪替樹自動機的計算行為用執行（run）[12]的概念來解釋。令 A=(S,s0,δ,Ω)為一個輪替樹自動機，(W,m0)是個定點標記加權轉移系統，其中W=(M,Σ,θ,l,ρ)。 A在(W,m0)上的一次執行是樹R=(V,E,λ)，其中(V,E)是定義樹的二元組，而λ:V→M×S是一個雙標記函數。該樹的根節點標記為(m0,s0)，并且每個帶有雙標記(m,s)的節點v滿足下列條件：

（1）δ(s)≠ 0 。

（2）如果δ(s)=q,則m∈ρ(q)；如果δ(s)≠q，則m?ρ(q)。

（3）如果δ(s)=(?r),則l(m)?r；如果δ(s)= ?(?r),則l(m)?r。

（4）如果δ(s)=s′,則存在v′∈Scc(v),使得λ(v′)=(m,s′)。

（5）如果δ(s)= ?ras,則存在v′∈Scc(v)，m′∈M并且使得λ(v′)=(m′,s′)。

（6）如果δ(s)=[?r]as,則對于所有x?r,存在v′∈Scc(v),使得λ(v′)=(m′,s′)。

（7）如 果δ(s)=s′∨s″，則 存 在v′∈Scc(v) 使 得λ(v′)=(m,s′)或者λ(v″)=(m,s″)。

（8）如果δ(s)=s′∧s″，則存在v′,v″∈Scc(v)使得λ(v′)=(m,s′)并且λ(v″)=(m,s″)。

（9）如果δ(s)=s′|s″，則存在v′,v″∈Scc(v)和m′,m″∈M使得λ(v′)=(m′,s′)并且λ(v″)=(m″,s″)。

當一次執行R的每一個無限分支上的狀態優先級標記滿足由Ω確定的奇偶接收條件，這個執行R能夠被接收。確切地說，對于每一個R的無限分支π,將優先級函數Ω應用到每個節點上，對于所得到的自然數序列，當其中無限次出現的最大自然數是偶數，這個分支能夠被接收。如果R的每個無限分支是可接收的，則R是可接收的。

當一個定點標記加權轉移系統上存在一個關于A可接收的執行，則這個系統是能夠被A接收的。能夠被A接收的語言，記作||A||，它包含了所有能夠被A接收的定點標記加權轉移系統。

接下來為每個CWC公式構建一個輪替樹自動機用以接收此公式定義的定點標記加權轉移系統。這種從CWC到輪替樹自動機的翻譯過程容易創建，關鍵是其正確性的證明。

令?為一個CWC公式，輪替樹自動機A(?)=(S,s0,δ,Ω)，其中：

（1）S是個包含?的所有子公式φ（記作φ）的集合。

（2）s0=?是初始狀態。

（3）δ是轉移函數，具體定義見圖4。

(4）Ω是優先級函數，定義方式同文獻[16]。

Fig.4 Definition of transform functionδ圖4 轉移函數δ定義

例3對于例2公式?=μq(p|(≥ 2)∨[≤ 5]aq)，構建其輪替樹自動機 A(?)，初始狀態為μq(p|(≥2)∨[≤5]aq)，轉移函數如下：

按照文獻[16]中優先級定義方式，除了狀態μq(r∨ [≤ 3]aq|(≤ 5)的優先級為1，其余狀態優先級均為0。

下面證明幾個定理，用以說明CWC的操作符和連接詞是如何用自動機來建模的。

定理1[12]令A和A′為兩個輪替樹自動機，則：

定理2[12]令A為一個輪替樹自動機，則：

定理3[12]令p為命題變元，A是輪替樹自動機，則：

定理1～3中涉及的自動機 A+A′，A?A′和 ?raA(φ)，[?r]aA(φ)以及μpA，νpA的定義見文獻[12]。

定義6令A和A′為兩個輪替樹自動機，s0為某個新的狀態，則A|A′定義為：

令φ和ψ為CWC公式，則容易看出A(φ|ψ)=A(φ)|A(ψ)。

基于定義6，可以得到定理4。

定理4令A和A′為兩個輪替樹自動機，則：

其中，M′是W′的狀態集，另一方面：

其中，M是W的狀態集。

證明對于任意兩個自動機A和A′，令A=(SA,首先證明本定理第一部分，假設 (W,m)∈ ||A|||||A′||，則存在 LWSs Wi=(Mi,Σi,θi,li,ρi),mi∈Mi,i=1,2使得 (W,m)～ (W1? W2,(m1,m2))并且以下條件成立：(W1,m1)∈||A||,(W2,m2)∈||A′||。令R1為A在(W1,m1)上的一次可接收執行，R2為A′在(W2,m2)上的一次可接收執行。考慮這樣的樹，它的根節點標記為(m,s0)（s0為某個新狀態）且恰有兩個后繼v1和v2，以v1為根節點的子樹與R1相同，以v2為根節點的子樹與R2相同，則這棵樹是 A|A′在(W?W1?W2,m)上的可接收執行。此時，(W?W1?W2,m)∈ ||A|A′||。

接著證明本定理第二部分。假設(W,m)∈||A|A′||，則A|A′在(W,m)上存在一個可接收執行R，且R的根節點有且僅有兩個后繼節點v1和v2，標記分別為。顯然，R↓v1和R↓v2分別是A和 A′在定點標記加權轉移系統(W↓m1,m1)，(W↓m2,m2)上的可接收執行。那么(W↓m1,m1)∈||A||且 (W↓m2,m2)∈ A′。令 (W′,m′)=(W↓m1? W↓m2,(m1,m2))，則有 (W′,m′)∈ ||A|||||A′||。 □

當 |A||||A′||與 ||A|||||A′||間具有定理 4 所述關系，則||A|A′||? ||A|||||A′||，稱二者互模擬等價。

這一章主要的定理是正確性的證明，即滿足?的定點標記加權轉移系統與自動機 A(?)能接收的語言是互模擬等價的。

定理5令?為任意CWC公式，則當?中包含模態詞 |時，||?||? ||A(?)||，否則 ||?||=||A(?)||。

證明按照公式?的復雜度歸納證明。當?為p,?p,(?r),?(?r)時，顯然 ||?||=||A(?)||成立。否則分情況討論，若?的最外層連接詞是析取和合取，定理1說明此情況成立；若最外層操作符是一元模態詞[?r]a和 ?ra，定理2說明此情況成立；若最外層操作符是不動點操作符，定理3說明此情況成立；若最外層操作符是二元模態詞|，定理4說明此情況成立。□

5 相關結論

5.1 可判定性

有了上一章的等價性，關于CWC的可滿足性判定可歸結到自動機的非空問題上。

定理6[12,16]輪替樹自動機的非空問題在指數時間內可判定。

根據定理5和定理6可直接得出定理7。

定理7CWC的可滿足性問題在指數時間內可判定。

5.2 小模型性

CWC的小模型性也可以利用上一章的等價性來證明。

定理8[17]如果一個輪替樹自動機A=(S,s0,δ,Ω)所接收的語言非空，那么它可以接收一個狀態集不超過2Ο(|S|4lg|S|)的定點標記加權轉移系統。

定理9一個CWC公式?能夠被某些定點標記加權轉移系統滿足，則存在一個狀態集不超過2Ο(|?|4lg|?|)的定點標記加權轉移系統滿足它。

證明根據定理5和定理8可知，對于一個CWC公式?，如果 A(?)=(S,s0,δ,Ω)所接收的語言非空，那么它可以接收一個狀態集不超過2Ο(|S|4lg|S|)的定點標記加權轉移系統，由A(?)的構造過程可知，該定點標記加權轉移系統的狀態集不超過 2Ο(|?|4lg|?|)。根據定理 5可知,若公式?中不包含組合模態詞 |，則存在一個狀態集不超過 2Ο(|?|4lg|?|)的定點標記加權轉移系統滿足它。否則，根據定理4，令L(?)表示公式?的長度，可得到結論，存在一個狀態集不超過 (2Ο(|?|4lg|?|))L(?)（i.e.2Ο(|?|4lg|?|)）的定點標記加權轉移系統滿足?。 □

6 結束語

本文在CWL的基礎上，提出了CWC，給出了它在LWS上的語義，并闡述了輪替樹自動機與CWC之間內在的聯系。這種聯系在探討CWC的可滿足性及小模型性等問題上起到重要作用。而如何使用輪替樹自動機探索CWC的公理系統，驗證其可靠性和完備性還有待進一步研究。