基于不動(dòng)點(diǎn)邏輯的混成系統(tǒng)性能評價(jià)語言

李 晴，曹子寧,2,3，黃 濤

(1.南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇 南京 211106;2.光電控制技術(shù)重點(diǎn)實(shí)驗(yàn)室，河南 洛陽 471023;3.軟件新技術(shù)與產(chǎn)業(yè)化協(xié)同創(chuàng)新中心，江蘇 南京 210023)

0 引 言

混成系統(tǒng)[1](Hybrid System，HS)通常由離散組件和連續(xù)組件組成，二者互相影響、互相依賴[2]。并且隨著混成系統(tǒng)的設(shè)計(jì)越來越復(fù)雜，二者之間的交互越來越緊密。目前，它已廣泛應(yīng)用在智能電網(wǎng)、自動(dòng)公路系統(tǒng)和醫(yī)療機(jī)器人等各種安全關(guān)鍵領(lǐng)域[3]。它們對系統(tǒng)的安全性有極高的要求，然而通過模型檢測等常用的形式化方法保障其安全性是很有限的。因此，需要將模型檢測與性能評價(jià)相結(jié)合[4]，利用各自的優(yōu)點(diǎn)，在保證驗(yàn)證系統(tǒng)效率的同時(shí)，描述更多系統(tǒng)的屬性。

文獻(xiàn)[5]提出PLTL用于描述“系統(tǒng)最終不會到達(dá)死鎖狀態(tài)的概率是否小于等于0.9？”等系統(tǒng)性質(zhì)。文獻(xiàn)[6]提出了計(jì)算樹度量語言CTML，用于評價(jià)系統(tǒng)與實(shí)數(shù)計(jì)算相關(guān)的性質(zhì)，如概率、平均期望等。文獻(xiàn)[7]在CTML、ZIA的基礎(chǔ)上，提出了PZIA，用于描述系統(tǒng)與數(shù)據(jù)相關(guān)的性質(zhì)和行為的概率性質(zhì)等。

基于μ演算[8-9]的模型檢測可用于設(shè)計(jì)與驗(yàn)證并發(fā)系統(tǒng)[10]，通過使用不動(dòng)點(diǎn)算子刻畫系統(tǒng)的性質(zhì)。文獻(xiàn)[11-12]在不動(dòng)點(diǎn)算子的基礎(chǔ)上分別提出并發(fā)加權(quán)μ演算和廣義可能性μ演算以增強(qiáng)經(jīng)典μ演算的表達(dá)能力。此外，目前已有一些較為高效的算法用于評價(jià)μ演算的公式[10,13]，并且很多時(shí)序邏輯可以轉(zhuǎn)換為μ演算，比如CTL。

因此，結(jié)合CTML和μ演算，該文提出了基于不動(dòng)點(diǎn)的性能評價(jià)語言MLBoF。由于MLBoF公式包含不動(dòng)點(diǎn)，而不動(dòng)點(diǎn)的存在不是必然的，因此給出其語義存在的合理性證明。為了簡化CTML子邏輯的計(jì)算步驟，給出與其語義等價(jià)的MLBoF公式及相應(yīng)的證明過程。最后，給出MLBoF公式的性能評價(jià)算法。

1 性能評價(jià)語言MLBoF

為了提出能夠描述實(shí)值計(jì)算相關(guān)性質(zhì)的性能評價(jià)語言，通過對經(jīng)典Kripke結(jié)構(gòu)中的標(biāo)簽函數(shù)進(jìn)行擴(kuò)展，將標(biāo)簽函數(shù)L的值域從{0,1}擴(kuò)展為[m,n]，其中m

定義1(狀態(tài)標(biāo)簽函數(shù))：狀態(tài)標(biāo)簽函數(shù)f表示從狀態(tài)空間S到閉區(qū)間[m,n]的一個(gè)映射，它可以表示為：f:S→[m,n]。其中，m和n的取值取決于具體實(shí)例。

狀態(tài)標(biāo)簽函數(shù)也可稱為原子函數(shù)或狀態(tài)函數(shù)，帶有原子函數(shù)的Kripke結(jié)構(gòu)定義如下：

定義2(KripkeAF)：KripkeAF結(jié)構(gòu)是一個(gè)四元組MAF=(S,S0,AF,R)，其中，S是一個(gè)有限狀態(tài)集合；S0是一個(gè)有限初始狀態(tài)集合；AF是原子函數(shù)的有限集合；R是一個(gè)遷移關(guān)系，R?S×S，R滿足?s∈S,?s'∈S，使(s,s')∈R。

KripkeAF為提出可以描述系統(tǒng)實(shí)值計(jì)算相關(guān)性質(zhì)的新的性能評價(jià)語言奠定了基礎(chǔ)。

1.1 MLBoF語法

MLBoF作為CTML和μ演算部分結(jié)合的產(chǎn)物，其語法定義如下所述：

定義3(MLBoF語法)：AF為原子函數(shù)集合，令fp表示由原子命題轉(zhuǎn)換而來的狀態(tài)函數(shù)，AF由一般的狀態(tài)函數(shù)f和fp組成。令VAR={φ1,φ2,φ3,…}，表示函數(shù)變量集合，其中每個(gè)φ∈VAR可被賦值為G(S)的一個(gè)元素，G(S)是所有可能的狀態(tài)函數(shù)組成的集合。MLBoF公式按如下規(guī)則構(gòu)造：

(1)若fAF∈AF，則fAF是一個(gè)公式；

(2)一個(gè)函數(shù)變量φ是一個(gè)公式；

(3)若f和g是公式，則f·g,f∨g,f∧g也是公式；

(4)如果f是公式，那么MXf是公式；

(5)若φ∈VAR是一個(gè)公式且f是一個(gè)公式，又f在φ上是單調(diào)的(由于MLBoF公式的構(gòu)造中去除了否定算子，即f中出現(xiàn)的所有函數(shù)變量φ，在公式f中其外面嵌套的否定算子個(gè)數(shù)為0)，則μφ·f和νφ·f都是公式。

1.2 MLBoF語義

經(jīng)典的μ演算公式表示一個(gè)狀態(tài)集合，而MLBoF的公式表示一個(gè)函數(shù)。MLBoF的語義定義如下所示：

定義4(MLBoF語義)：公式f可以解釋為一個(gè)狀態(tài)映射函數(shù)f:S→[m,n]，并將其記為[[f]]Me，其中M是變遷系統(tǒng)，e:VAR→G(S)是環(huán)境。函數(shù)[[f]]Me的遞歸定義如下所示：

(1)若h=[[fAF]]Me，則存在兩種情況：若fAF=f，則對于?s∈S，存在h(s)=f(s)；若fAF=fp，則對于?s∈S，存在：

(2)[[φ]]Me=e(φ)。

(3)若h=[[f·g]]Me，則對?s∈S，有h(s)=f(s)·g(s)；需要注意，使用·算子的前提是公式f和g滿足f:S→[0,1]和g:S→[0,1]，并且[0,1]?[m,n]。

(4)若h=[[MXf]]Me，則對?s∈S，有：

其中，Ts={t|s→t,且s≠t}，ps,t是由狀態(tài)s到狀態(tài)t的遷移概率。

(5)若h=[[f∧g]]Me，則對?s∈S，有h(s)=min{f(s),g(s)}。

(6)若h=[[f∨g]]Me，則對?s∈S，有h(s)=max{f(s),g(s)}。

(7)若h=[[μφ.f]]Me，則[[μφ.f]]Me是變換τ:G(S)→G(S)的最小不動(dòng)點(diǎn)，其中τ(W)=[[f]]Me[φ←W]。

(8)若h=[[νφ.f]]Me，則[[νφ.f]]Me是變換τ:G(S)→G(S)的最大不動(dòng)點(diǎn)，其中τ(W)=[[f]]Me[φ←W]。

2 MLBoF語義合理性

由于性能評價(jià)語言MLBoF的語義涉及到不動(dòng)點(diǎn)，而不動(dòng)點(diǎn)是否存在并不是顯然的。因此，MLBoF語義的合理性依賴于不動(dòng)點(diǎn)的存在，進(jìn)而下文對不動(dòng)點(diǎn)的存在性進(jìn)行論述。

根據(jù)Tarski不動(dòng)點(diǎn)定理，若MLBoF公式的語義解釋環(huán)境構(gòu)成完備格以及映射函數(shù)τ是單調(diào)的，那么可證得不動(dòng)點(diǎn)是存在的。

下面給出基于MLBoF公式語義的G(S)上的二元關(guān)系定義，以及該二元關(guān)系是偏序關(guān)系的證明過程，具體如下：

定義5(二元關(guān)系?)：給定一個(gè)KripkeAF結(jié)構(gòu)M=(S,S0,AF,R)，S上所有的狀態(tài)函數(shù)構(gòu)成集合G(S)，G(S)上存在一個(gè)二元關(guān)系?：對于函數(shù)f1,f2∈G(S)，若對?s∈S，f1(s)≤f2(s)成立，則稱f1?f2成立。

命題1：G(S)上的二元關(guān)系集合(G(S),?)是偏序集。

證明：根據(jù)?和偏序的定義，可證得?滿足自反性、反對稱性和傳遞性。因此，命題1成立，具體的證明過程見文獻(xiàn)[14]。

命題2：偏序集(G(S),?)構(gòu)成一個(gè)完備格。

證明：根據(jù)完備格[11]和(G(S),?)的定義，取G(S)中任一子集A(S)。考慮A(S)的最小上界分別是A(S)和G(S)A(S)中的元素兩種情況，可證得G(S)的任意子集A(S)存在最小上界和最大下界。具體的證明過程見文獻(xiàn)[14]。

在此基礎(chǔ)上，可以利用結(jié)構(gòu)歸納法證明G(S)上的映射函數(shù)τ:G(S)→G(S)的單調(diào)性。而τ函數(shù)的單調(diào)性證明可轉(zhuǎn)化為MLBoF公式的單調(diào)性證明，進(jìn)而可轉(zhuǎn)化為MLBoF公式中出現(xiàn)的所有算子的單調(diào)性證明。

命題3：MLBoF公式中出現(xiàn)的所有算子都是單調(diào)的。

證明：根據(jù)基礎(chǔ)算子·、MX、∧和∨的語義及利用其構(gòu)造的MLBoF公式語義，可證得基礎(chǔ)算子·、MX、∧和∨的是單調(diào)的。因此，命題3成立，具體的證明過程見文獻(xiàn)[14]。

因此，由上述算子構(gòu)造的MLBoF的任何公式也是單調(diào)的。由于不動(dòng)點(diǎn)算子中的公式是·、∧、∨和MX算子構(gòu)成的，所以出現(xiàn)在不動(dòng)點(diǎn)算子中的每一個(gè)可能的公式也是單調(diào)的。根據(jù)結(jié)構(gòu)歸納法，不動(dòng)點(diǎn)算子構(gòu)成的MLBoF公式也是單調(diào)的。而G(S)上的映射函數(shù)τ是由·、∧、∨和MX和不動(dòng)點(diǎn)算子構(gòu)成的，因此，根據(jù)結(jié)構(gòu)歸納法，若構(gòu)成τ函數(shù)的基礎(chǔ)算子是單調(diào)的，那么τ函數(shù)也是單調(diào)的。

由Tarski不動(dòng)點(diǎn)定理，可知MLBoF存在最小和最大不動(dòng)點(diǎn)。所以其語義是合理的。

利用結(jié)構(gòu)歸納法的思想，可將μ演算中謂詞變換滿足∪連續(xù)和∩連續(xù)定義和性質(zhì)[15]推廣到MLBoF上的映射函數(shù)τ(W)=[[f]]Me[φ←W]，因此τ(W)=[[f]]Me[φ←W]也是∪連續(xù)和∩連續(xù)的。而根據(jù)MLBoF的語法和語義可知，μφ.f和νφ.f的語義(即[[μφ.f]]Me和[[νφ.f]]Me分別表示映射函數(shù)τ(W)=[[f]]Me[φ←W]的最小不動(dòng)點(diǎn)和最大不動(dòng)點(diǎn)。

因此，根據(jù)Tarski不動(dòng)點(diǎn)定理可知，若τ是∪連續(xù)的，則[[μφ.f]]Me=∪i(τi(MIN))；若τ是∩連續(xù)的，則[[νφ.f]]Me=∩i(τi(MAX))。假設(shè)G(S)中的所有函數(shù)映射的值都位于實(shí)數(shù)區(qū)間[m,n],那么MIN表示fmin:S→{m}，MAX表示fmax:S→{n}。

3 CTML子邏輯的MLBoF公式表示

3.1 CTML簡介

CTML是一個(gè)可用于描述系統(tǒng)的概率和期望等實(shí)值屬性的性能評價(jià)語言，它的某些子邏輯可以用MLBoF表示，該文將它們命名為SLoCTML(Sub-Logic of CTML)。它的語法和語義具體如下：

定義6(SLoCTML語法)：SLoCTML的語法定義如下：

(1)φ::=one|zero|r|φ·φ|Mδ；

(2)δ::=φU×φ|Xφ；

由于SLoCTML代表CTML的某些子邏輯，其更加具體的語法解釋和語義定義可見文獻(xiàn)[6]。

根據(jù)二者的語義，可知MLBoF公式可以表示SLoCTML，如MX、·、MU×，而且SLoCTML的原子狀態(tài)函數(shù)可以用MLBoF的原子狀態(tài)函數(shù)fp表示。

根據(jù)SLoCTML的語義可知，SLoCTML的MU×算子描述的系統(tǒng)屬性相對復(fù)雜，具有較大的實(shí)際意義。所以下文以MU×為例，給出與其語義等價(jià)的MLBoF公式表示以及證明過程。

3.2 與MU×公式語義等價(jià)的MLBoF公式

由于性能評價(jià)語言MLBoF的公式涉及到不動(dòng)點(diǎn)，表達(dá)形式比較抽象，不利于理解和描述性質(zhì)。根據(jù)二者公式語義，可知M(fU×g)與μφ.[g∨(f·MXφ)]語義等價(jià)，且τ(φ)=g∨(f· MXφ)。若狀態(tài)s滿足M(fU×g)，則使用上述語義等價(jià)的MLBoF公式計(jì)算；否則，對于不滿足路徑公式的狀態(tài)s，令其函數(shù)值為0。

在證明語義等價(jià)前，需要進(jìn)行一些說明：

(1) 將SLoCTML的MU×公式中出現(xiàn)的原子命題f和g看作MLBoF中的原子函數(shù)，并且它們的值域?yàn)閷?shí)數(shù)區(qū)間[m,n]中，其中m=0，n=1。

(2)令最大的狀態(tài)函數(shù)和最小的狀態(tài)函數(shù)分別為MAX:S→{n}和MIN:S→{m}。

下面給出二者語義等價(jià)的具體證明過程：

命題4：τ(φ)=g∨(f· MXφ)是單調(diào)的。

證明：假設(shè)f1?f2，根據(jù)函數(shù)τ(φ)=g∨ (f· MXφ)的語義，給出τ(f1)和τ(f2)各自可能的兩種語義。并在此基礎(chǔ)上，根據(jù)偏序關(guān)系?的定義、τ(f1)和τ(f2)每種可能語義之間的依賴關(guān)系，進(jìn)而證得τ(f1)?τ(f2)成立。具體的證明過程見文獻(xiàn)[14]。

命題5：M(fU×g)的語義和τ(φ)=g∨(f·MXφ)的不動(dòng)點(diǎn)的語義等價(jià)。

證明：綜合考慮M(fU×g)可能的兩種語義h(s)=g(s)和h(s)=(f· MX (MfU×g))(s)，利用公式轉(zhuǎn)換和具體的公式語義可證得命題5成立，具體的證明過程見文獻(xiàn)[14]。

命題6：CTML的M(fU×g)公式的語義和MLBoF的μφ.[g∨ (f·MXφ)]公式語義等價(jià)，即M (fU×g)=[[μφ.[g∨ (f·MXφ)]]]Me。

證明：在分析公式μφ.[g∨ (f· MXφ)]和M(fU×g)的語義之后，利用歸納法，依次證得∪i(τi(MIN))?M(fU×g)和M(fU×g)?∪i(τi(MIN))成立。因此，命題6成立。具體的證明過程見文獻(xiàn)[14]。

4 MLBoF公式的性能評價(jià)算法

該算法是對Emerson和Lei提出的用于評價(jià)μ演算公式的算法[15]的一個(gè)擴(kuò)展，其不同之處在于在計(jì)算外層不動(dòng)點(diǎn)的新的近似值時(shí)，不必使用MIN或MAX重新初始化內(nèi)層不動(dòng)點(diǎn)的計(jì)算，只需從這個(gè)不動(dòng)點(diǎn)下的任何已知的近似值開始迭代計(jì)算即可。此外，通過引入人為設(shè)置的誤差值α，避免算法進(jìn)行無終止地計(jì)算。所以，該算法能夠在保證效率的同時(shí)，盡可能地計(jì)算出較為接近真正不動(dòng)點(diǎn)的近似不動(dòng)點(diǎn)。

MLBoF公式的性能評價(jià)算法輸入MLBoF公式、系統(tǒng)模型KripkeAF和誤差值α，輸出一個(gè)狀態(tài)函數(shù)h。該算法的偽代碼如下所示：

1:Function eval (h,e)

2:if (h=fp)

3: forsinS

4:if (p∈L(s))h(s)=1;

5:Elseh(s)=0;

6: returnh;

7:if (h=f)

8: forsinSh(s)=f(s);

9: returnh;

10:if (h=φ) returne(φ);

11:if (h=g1·g2)

12:g1=eval(g1,e);g2= eval(g2,e);

13: forsinSh(s)=g1(s)·g2(s);

14: returnh;

15:if(h=g1∧g2)

16:g1=eval(g1,e);g2= eval(g2,e);

17: forsinSh(s)=min{g1(s),g2(s)};

18: returnh;

19:if (h=g1∨g2)

20:g1= eval(g1,e);g2=eval(g2,e);

21: forsinSh(s)=max{g1(s),g2(s)};

22: returnh;

23:if(h= MXg)

24:g=eval(g,e);

25: forsinS

27: Elseh(s)=g(s);

28: returnh;

29:if (h=μφi.f(φi))

30: for top-level greatest fixpoint subformulasυφj.f'(φj) inf

31:F[j]=MAX;

32: while ?s∈S,F[j](s)-φold(s)>α

33:φold=F[i];

34:F[i]= eval(f,e[φi←F[i]]);

35:h=F[i]；

36: returnh;

37:if (h=νφi.f(φi))

38: for top-level least fixpoint subformulasμφj.f'(φj) inf

39:F[j]=MIN;

40: while ?s∈S,F[i](s)-φold(s)>α

41:φold=F[i];

42:F[i]=eval(g,e[φi←F[i]]);

43:h=F[i]；

44: returnh;

45:end function eval;

5 MLBoF性能評價(jià)公式實(shí)例

本節(jié)以飛機(jī)起飛控制系統(tǒng)[16]為例，使用MLBoF和CTML公式分別描述與其本身相關(guān)的系統(tǒng)性質(zhì)，并使用MLBoF公式的性能評價(jià)算法計(jì)算MLBoF公式的值。

它的整個(gè)起飛過程由停止、滑行、起飛、爬升、平飛等階段組成，并且前四個(gè)階段有可能進(jìn)入故障狀態(tài)。它的自動(dòng)機(jī)模型如圖1所示。

圖1 飛機(jī)控制系統(tǒng)

(1)對于性質(zhì)“飛機(jī)從Stop開始，最終發(fā)生異常即到達(dá)Error狀態(tài)的概率是多少”， CTML描述為：(Mone U×fError) (Stop)， MLBoF公式描述為：μφ.[fError∨ (one · MXφ)]，τ(φ)=fError∨ (one · MXφ)。需要注意的是，下面公式中的S的元素依次為狀態(tài)Stop、Taxi、Take_off、Climb、Error和Cruise。

其中，MLBoF公式分別由CTML中的原子命題one和fError轉(zhuǎn)換而來。因此，其映射的實(shí)數(shù)區(qū)間為[0,1]，并且MIN:S→{0}。根據(jù)性能評價(jià)算法，令誤差α=0.001，有：

τ(MIN)(S)=(0,0,0,0,1,0)；

τ2(MIN)(S)=(0.1, 0.1, 0.1, 0.1, 1, 0)；

τ3(MIN)(S)=(0.19, 0.19, 0.19, 0.1, 1, 0)；

τ4(MIN)(S)=(0.271, 0.271, 0.19,0.1,1,0)；

τ5(MIN)(S)=(0.343 9,0.271,0.19,0.1,1,0)；

τ6(MIN)(S)=τ5(MIN) (S)。

此時(shí)算法終止，可知飛機(jī)從Stop開始，最終發(fā)生異常即到達(dá)Error狀態(tài)的概率是0.343 9。

(2)對于性質(zhì)“飛機(jī)從Stop開始，最終成功巡航即到達(dá)Cruise狀態(tài)的概率是多少”，CTML描述為：(M oneU×fCruise)(Stop)， MLBoF公式描述為：μφ.[fCruise∨ (one · MXφ)]，τ(φ) =fCruise∨ (one · MXφ)。

根據(jù)性能評價(jià)算法，令誤差α=0.001，有：

τ(MIN)(S) = (0, 0, 0, 0, 0, 1)；

τ2(MIN)(S) = (0, 0, 0, 0.9, 0,1)；

τ3(MIN)(S) = (0, 0, 0.81, 0.9, 0, 1)；

τ4(MIN)(S) = (0, 0.729, 0.81, 0.9, 0, 1)；

τ5(MIN)(S)=(0.656 1, 0.729,0.81, 0.9,0,1)；

τ6(MIN)(S) =τ5(MIN)(S)；

此時(shí)算法終止，可知飛機(jī)從Stop開始，最終成功巡航即到達(dá)Cruise狀態(tài)的概率是0.656 1。

通過上述應(yīng)用實(shí)例可知，MLBoF公式的性能評價(jià)算法的效率體現(xiàn)在以下兩個(gè)層面：

(1)由于MU×公式的計(jì)算依賴于涉及矩陣方程等復(fù)雜計(jì)算的線性系統(tǒng)求解[6]，計(jì)算復(fù)雜，且時(shí)間復(fù)雜度為O(Poly(|S|)。其中Poly(|S|)表示|S|大小的多項(xiàng)式時(shí)間，|S|表示系統(tǒng)模型中的狀態(tài)個(gè)數(shù)。而與MU×公式語義等價(jià)的MLBoF公式的計(jì)算依賴于計(jì)算不動(dòng)點(diǎn)的思想，該過程無需進(jìn)行復(fù)雜的數(shù)學(xué)計(jì)算。因此，從這個(gè)層面上講，該算法的效率體現(xiàn)在算法思想和計(jì)算步驟的簡單。

(2)由于MLBoF公式的性能評價(jià)算法的提出基于對需要進(jìn)行O(nd)次迭代的計(jì)算不動(dòng)點(diǎn)的算法的擴(kuò)展，相對于擴(kuò)展需要進(jìn)行O(nk)次迭代的簡單直接的遞歸算法，該算法的效率更高。其中，n表示系統(tǒng)模型的狀態(tài)個(gè)數(shù)，k表示不動(dòng)點(diǎn)嵌套深度，d表示公式的交替深度[15]。因此，從這個(gè)層面上，該算法的效率也得到了一定的改善。

6 結(jié)束語

由于混成系統(tǒng)廣泛應(yīng)用于各種安全關(guān)鍵領(lǐng)域，通過一般的形式化方法保障其安全性有一定的局限性。因此，提出一種面向混成系統(tǒng)的性能評價(jià)語言MLBoF，用于描述系統(tǒng)行為的概率屬性等。同時(shí)，為了簡化SLoCTML的計(jì)算步驟以及提高M(jìn)LBoF公式的理解性，給出與SLoCTML語義等價(jià)的MLBoF公式。最后，通過擴(kuò)展計(jì)算不動(dòng)點(diǎn)的算法，提出一個(gè)MLBoF公式的性能評價(jià)算法。與傳統(tǒng)的基于μ演算的模型檢測[15]相比，MLBoF可以描述系統(tǒng)行為的概率屬性。在以后的工作中，可以嘗試往MLBoF公式中引入更多的算子如+算子，使其能夠描述完整的CTML邏輯。