陳云云，陳 哲

(南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，南京 211106) (軟件新技術(shù)與產(chǎn)業(yè)化協(xié)同創(chuàng)新中心，南京 211106) (高安全系統(tǒng)的軟件開發(fā)與驗(yàn)證技術(shù)工業(yè)和信息化部重點(diǎn)實(shí)驗(yàn)室，南京 211106)

1 引 言

運(yùn)行時(shí)驗(yàn)證技術(shù)是一種輕量級的軟件驗(yàn)證技術(shù)，它通過驗(yàn)證系統(tǒng)產(chǎn)生的有限行為序列是否滿足某種約束來間接地驗(yàn)證系統(tǒng)的正確性[1,2].由于運(yùn)行時(shí)驗(yàn)證技術(shù)不但可以有效地監(jiān)測系統(tǒng)運(yùn)行中的異常行為，而且可以在發(fā)現(xiàn)異常時(shí)發(fā)出警告或作出反應(yīng)，因此，越來越多的學(xué)者對運(yùn)行時(shí)驗(yàn)證進(jìn)行了深入地探討和研究[19-22].

軟件驗(yàn)證領(lǐng)域常用線性時(shí)序邏輯(Linear Temporal Logic,LTL)這一形式化語言來描述系統(tǒng)需要滿足的約束[23].然而，并不是所有的LTL公式都適合用于運(yùn)行時(shí)驗(yàn)證.經(jīng)過多年的研究，學(xué)者們常用可監(jiān)控性和弱可監(jiān)控性來衡量一個LTL公式在運(yùn)行時(shí)驗(yàn)證領(lǐng)域的可用性.

可監(jiān)控性最初是由Pnueli和Zaks提出的[3]，后來，Bauer對可監(jiān)控性提出了一個更完善的定義并論述了在不同ω語言下可監(jiān)控性判定問題的復(fù)雜度[5].2011年，Bauer和Leucker等人又基于LTL3[5]提出了監(jiān)控器的概念，并概念性地給出了LTL公式對應(yīng)監(jiān)控器的構(gòu)造方法[6].2014年，Diekert從拓?fù)鋵W(xué)的角度闡述了可監(jiān)控性問題，并證明了可監(jiān)控性的判定問題是PSPACE完全問題[7].2018年，國內(nèi)學(xué)者Chen Z.和Wu Y.指出在實(shí)際的運(yùn)行時(shí)驗(yàn)證過程中，可監(jiān)控性的要求過于嚴(yán)格，提出了弱可監(jiān)控性[8]的概念，并結(jié)合Bauer等人提出的基于監(jiān)控器的可監(jiān)控性判定思想，提出了基于監(jiān)控器的弱可監(jiān)控性判定算法.

目前，關(guān)于可監(jiān)控性和弱可監(jiān)控性的判定算法主要有三種：基于監(jiān)控器的判定算法[6]、基于公式重寫的判定算法[9]和基于無限義務(wù)[9]的判定算法.其中，前兩種算法是完備的算法，而第三種尚且不是一個完備的判定算法，但其可以和其他兩種算法復(fù)合使用，起到加速的作用.

然而，在實(shí)際的運(yùn)行時(shí)驗(yàn)證過程中，可監(jiān)控性的要求過于嚴(yán)格，其要求對于任意的有限序列都能通過有限步的擴(kuò)展使驗(yàn)證給出滿足或違反的輸出，這就導(dǎo)致一部分有價(jià)值的公式得不到應(yīng)用.弱可監(jiān)控性的提出避免了這一問題，但我們應(yīng)該考慮到弱可監(jiān)控性解決的僅僅是一個存在問題.因?yàn)槠鋬H要求存在一條有限序列能通過有限步的擴(kuò)展使驗(yàn)證給出滿足或違反的輸出即可.因此，我們無法得知一個弱可監(jiān)控的公式中究竟存在多少條這樣的有限序列.

綜上，本文提出了概率可監(jiān)控性的概念，然后重點(diǎn)研究了概率可監(jiān)控性的求解算法，并在這些研究的基礎(chǔ)上借助開源工具和C++語言進(jìn)行了代碼實(shí)現(xiàn)，并通過實(shí)驗(yàn)證明了算法的正確性.

2 理論知識

2.1 可監(jiān)控性、弱可監(jiān)控性

監(jiān)控器M的輸入是一條有限序列u∈Σ*，輸出是B3集合中的一個值.對于給定的LTL公式φ，一定可以構(gòu)造一個與其等價(jià)的監(jiān)控器Mφ=(Q,Σ,δ,q0,λ)，使得對于?u∈Σ*，都有[uφ]=λ(δ(q0,u))成立.

定義 2.可監(jiān)控性[8](Monitorability).給定一個LTL公式φ，我們稱φ是可監(jiān)控的，當(dāng)且僅當(dāng)，對于?u∈Σ*，都?v∈Σ*，使得uvΣω?L(φ)或uvΣω∩L(φ)=?成立.

定義 3.弱可監(jiān)控性[8](Weak-Monitorability).給定一個LTL公式φ，我們稱φ是弱可監(jiān)控的，當(dāng)且僅當(dāng)，?u,v∈Σ*，使得uvΣω?L(φ)或uvΣω∩L(φ)=?成立.

從好前綴和壞前綴的角度來講，如果對于任意的有限序列，其都能通過有限擴(kuò)展成為公式φ的好前綴或壞前綴，那么φ是可監(jiān)控的.例如，Xp∧Fq是可監(jiān)控的，因?yàn)閷τ谀切┑诙€符號為p的有限序列，只要其在未來延伸的某時(shí)刻滿足了q，那么延伸后的序列就一定是Xp∧Fq的好前綴；而對于那些第二個符號為!p的有限序列，其已經(jīng)是Xp∧Fq的壞前綴.如果存在一條有限序列能夠通過有限擴(kuò)展成為公式φ的好前綴或壞前綴，那么φ是弱可監(jiān)控的.例如，Xp∧GFp是不可監(jiān)控但弱可監(jiān)控的，其等價(jià)的監(jiān)控器如圖1所示.

圖1 公式Xp∧GFp的等價(jià)監(jiān)控器Fig.1 Monitor of formula Xp∧GFp

對于那些第二個符號是p的有限序列，其已到達(dá)狀態(tài)2，無論未來對其如何擴(kuò)展都不可能使其成為公式的(好)壞前綴；但是，對于那些第二個符號是!p的有限序列，其就是公式的一個壞前綴，監(jiān)控器可以快速地給出一個違反的判定.

2.2 馬爾可夫鏈

定義 4.馬爾可夫鏈[10](Markov Chain).馬爾可夫鏈可以用一個五元組M=(Q,P,ιinit,AP,L)來表示，其中，Q是一個可數(shù)且非空的狀態(tài)集合；P:Q×Q→[0,1]是遷移概率函數(shù)，且對于所有的q∈Q，有∑q′∈QP(q,q′)=1；ιinit:Q→[0,1]是初始分布，且有∑q∈Qιinit(q)=1；AP是原子命題的集合；L:Q→2AP是標(biāo)簽函數(shù).

定義 5.σ-代數(shù)[10].σ-代數(shù)可以用一個集合對(Outc,E)來表示，其中，Outc是一個可數(shù)且非空的集合；?∈E，E?2Outc，且E在補(bǔ)運(yùn)算和可數(shù)個并(交)運(yùn)算下是閉包的.

一般將Outc中的元素稱作結(jié)果(outcome)，E中的元素稱作事件(event).

定義 6.概率測度[10].概率測度是定義在σ-代數(shù)上的一個函數(shù)Pr:E→[0,1]，我們用Pr(E)表示事件E的概率測度，或簡稱事件E的概率.

定義 7.概率空間[10].概率空間可以用一個三元組(Outc,E,Pr)來表示，其中，(Outc,E)是一個σ-代數(shù)，Pr是定義在σ-代數(shù)上的概率測度.

PrM(Cyl(q0q1…qn))=ιinit(q0)·P(q0q1…qn)

(1)

其中，

(2)

特殊地，若有限路徑的長度為0，則令P(q0)=1.

3 概率可監(jiān)控性

為了確保對系統(tǒng)進(jìn)行運(yùn)行時(shí)驗(yàn)證時(shí)所使用的約束公式是合理的，需要對約束公式的可監(jiān)控性和弱可監(jiān)控性進(jìn)行判定.但是，可監(jiān)控性的要求過于嚴(yán)格，而弱可監(jiān)控性又僅僅解決了“存在”的問題.

圖2 監(jiān)控器的結(jié)構(gòu)圖Fig.2 Structure diagram of monitor

弱可監(jiān)控性僅僅解決了“存在”的問題.這里的“存在”問題指的是存在一條有限序列可以擴(kuò)展為公式的好前綴或壞前綴，無論其存在一條、多條還是所有條.即只要不可監(jiān)控的公式存在可監(jiān)控的部分即可，不論其可監(jiān)控部分的大小.

然而，通過研究，我們發(fā)現(xiàn)不同的弱可監(jiān)控公式，其可擴(kuò)展為公式的好前綴或壞前綴的有限序列的比例是不一樣的，且可擴(kuò)展為公式的好前綴或壞前綴的有限序列所占比例越大，其在運(yùn)行時(shí)驗(yàn)證中就越有可能給出確定的判定結(jié)果，其利用價(jià)值也越大.但目前我們卻無法計(jì)算出這些有限序列的比例.因此，為了量化公式的可監(jiān)控性，我們提出了概率可監(jiān)控性.

注意，上述定義中的有限序列就是有限符號序列，后文若無特殊說明，均遵循這個原則.

定義 9.概率可監(jiān)控性. 給定公式φ及其等價(jià)監(jiān)控器Mφ=(Q,Σ,δ,q0,λ)，我們稱Mφ中可監(jiān)控的有限序列條數(shù)占所有有限序列條數(shù)的比例為公式φ的可監(jiān)控性概率，記為:

(3)

當(dāng)公式是可監(jiān)控的時(shí)，其可監(jiān)控性概率是1；當(dāng)公式是弱不可監(jiān)控的時(shí)，其可監(jiān)控性概率是0；當(dāng)公式是不可監(jiān)控但弱可監(jiān)控的時(shí)，其可監(jiān)控性概率的取值范圍是(0,1).

4 概率可監(jiān)控性的求解算法

4.1 直接求解的不可行性

當(dāng)我們根據(jù)定義對可監(jiān)控性概率進(jìn)行計(jì)算時(shí)，個別公式的PrM(φ)可以直接地計(jì)算出來.例如，對于公式Xp∧GFp，其AP={p}，|AP|=2，其等價(jià)監(jiān)控器(如圖1)中長度為1的有限(符號)序列有=(2|AP|)1=2條，分別為?和{p}，其對應(yīng)監(jiān)控器中的標(biāo)簽序列{true}，都是可監(jiān)控的；長度為2的有限序列共有|Σ|2=4條，分別為??、{p}?、?{p}和{p}{p}，其中，前兩條對應(yīng)監(jiān)控器中的標(biāo)簽序列{true}{!p}，是可監(jiān)控的，后兩條對應(yīng)監(jiān)控器中的標(biāo)簽序列{true}{p}，是不可監(jiān)控的；后面依此類推.經(jīng)過我們上述的分析，我們發(fā)現(xiàn)當(dāng)有限序列的長度大于等于2時(shí)，其有限序列被明顯地分為兩部分，一部分是那些第二個符號是{p}的有限序列，另一部分是那些第二個符號是?的有限序列，因此，PrM(Xp∧GFp)可表示為：

但是，對于大多數(shù)的LTL公式，其可監(jiān)控性概率是無法直接計(jì)算出來的.例如，對于計(jì)算機(jī)領(lǐng)域中常用的一個約束公式φ2=G((r1∧(u1U r2))→F(n2 U n1))∧((r→(t U u))U(t∨Gt))，其等價(jià)監(jiān)控器M2如圖3所示.

圖3 公式φ2的等價(jià)監(jiān)控器M2Fig.3 Monitor of formula φ2

圖3中的每個狀態(tài)都帶有自身到自身的遷移，且圖中還存在不同狀態(tài)間互為后繼的情況(狀態(tài)0和1).在這樣的情況下，隨著有限序列長度n的增大，可監(jiān)控的有限序列的情況就越復(fù)雜.例如，當(dāng)n為1時(shí)，標(biāo)簽((!r& !t)|(!t&u))和(r& !t& !u)對應(yīng)的有限序列是可監(jiān)控的；當(dāng)n為2時(shí)，標(biāo)簽((!r& !t)|(!t&u))2、(r& !t& !u)(t& !u)、(r& !t& !u)(!t& !u)、(r& !t& !u)(!t&u)和((!r& !t)|(!t&u))(r& !t& !u)對應(yīng)的有限序列是可監(jiān)控的.當(dāng)有限序列的長度趨于無窮大時(shí)，可監(jiān)控的有限序列就有無窮多種情況，無法計(jì)算.

4.2 概率可監(jiān)控性問題的補(bǔ)問題

定義 10.ugly狀態(tài).給定一個監(jiān)控器M=(Q,Σ,δ,q0,λ)，如果q∈Q滿足λ(q)=?且對于?r∈Post*(q)，都有λ(r)=?，則稱狀態(tài)q為ugly狀態(tài).

對于所有的公式，其不可監(jiān)控的有限序列占有限序列的比例PrNM(φ)都可以表示為：

(4)

我們觀察到，公式(3)和公式(4)中的分子分母有一定的特點(diǎn)，即其分母都是一個以|Σ|為公比的等比數(shù)列的和，隨著長度n的增大，分母也不斷增大，且當(dāng)長度n趨于正無窮大時(shí)，分母也趨于正無窮大.這一特點(diǎn)與數(shù)學(xué)領(lǐng)域中的施托爾茲定理(The O′Stolz theorem)[11]非常契合.施托爾茲定理常用于處理數(shù)列不定式的極限問題，根據(jù)施托爾茲定理可得：

(5)

(6)

即公式φ的PrM(φ)(或PrNM(φ))就等于長度n趨于無窮大時(shí)的有限序列中，(不)可監(jiān)控的有限序列的占比.

證明：首先，我們介紹數(shù)學(xué)領(lǐng)域中的施托爾茲定理[11]，該定理的具體描述如下：給定數(shù)列{an}、{bn}，若其滿足：

下面，我們使用這一定理對公式(5)、公式(6)進(jìn)行證明.首先，我們證明公式(5)的正確性.

所以，數(shù)列{An}、{Bn}滿足條件③.

至此，公式(5)證明完畢.另外，關(guān)于公式(6)的證明方法與公式(5)的證明思想類似，此處不再贅述.

4.3 基于馬爾可夫鏈的求解算法

通過分析，我們注意到不可監(jiān)控的有限序列條數(shù)和監(jiān)控器中每個邊上標(biāo)簽對應(yīng)的符號占比相關(guān).例如，對于公式Xp∧GFp，長度為1的有限序列共2條，標(biāo)簽?對應(yīng)的符號集合占比0，不可監(jiān)控的有限序列共2×0=0條；長度為2的有限序列共4條，標(biāo)簽{true}{p}對應(yīng)的符號集合占比1×1/2=1/2，不可監(jiān)控的有限序列2條；以此類推，長度為n的有限序列共2n條，標(biāo)簽{true}{p}{true}n-2對應(yīng)的符號集合占比1×1/2×1n-2=1/2，不可監(jiān)控的有限序列條數(shù)為2n×1/2=2n-1條.

此外，我們還注意到監(jiān)控器本身就是一個特殊的確定性有限自動機(jī)，且其是完全的(complete)，即對于監(jiān)控器中的任意狀態(tài)，以該狀態(tài)為源點(diǎn)出發(fā)的所有邊上的標(biāo)簽對應(yīng)的公式的析取等價(jià)于true(對應(yīng)符號集合的并為Σ)，且任意兩條邊上標(biāo)簽對應(yīng)的公式的合取等價(jià)于false(對應(yīng)符號集合的交集為空集).而監(jiān)控器和馬爾科夫鏈的不同主要在于：一、馬爾可夫鏈的遷移是通過概率分布選擇的，而監(jiān)控器的遷移是通過符號選擇的；二、馬爾可夫鏈的初始狀態(tài)是根據(jù)其初始分布來確定的，而監(jiān)控器中只有唯一的初始狀態(tài).下面，我們將解決上述兩個問題，并給出將一個監(jiān)控器描述為一個馬爾可夫鏈的辦法.

定義 11.給定一個監(jiān)控器M=(Q,Σ,δ,q0,λ)，我們可以將其描述為一個馬爾可夫鏈Mr=(Qr,Pr,ιinitr,APr,Lr)，其中，Qr=Q；Pr:Qr×Qr→[0,1]，對于所有的q∈Qr，有∑q′∈QrPr(q,q′)=1；ιinitr:Qr→[0,1]，ιinitr(q0)=1，對于任意的q∈Qr∧q≠q0，ιinitr(q0)=0，滿足∑q∈Qrιinitr(q)=1；APr=AP；Lr:Qr→(2AP,λ)，λ:Q→B3.

在上述的定義中，我們解決了前面提的兩個問題.第一個問題，由于監(jiān)控器中的每個狀態(tài)與其直接后繼之間的遷移上的標(biāo)簽對應(yīng)的符號的并集是符號全集2AP，且任意兩條遷移對應(yīng)的符號集合沒有交集.因此，我們用每條遷移上標(biāo)簽對應(yīng)的符號集合占符號全集Σ=2AP的比例來表示遷移概率.第二個問題，由于監(jiān)控器是一個確定性的有限自動機(jī)，所以，其只有一個初始狀態(tài)q0.因此，我們令ιinitr(q0)=1，且令其它的q∈Qr∧q≠q0，ιinitr(q)=0，這滿足∑q∈Qrιinitr(q)=1.除此之外，我們將監(jiān)控器中的狀態(tài)輸出添加到馬爾科夫鏈的標(biāo)簽函數(shù)Lr中去(在圖中，我們將狀態(tài)輸出和狀態(tài)放在一起)，這是因?yàn)樵诤罄m(xù)算法的設(shè)計(jì)中，狀態(tài)輸出信息必不可少.通過上述定義，我們可以將監(jiān)控器描述為一個標(biāo)準(zhǔn)馬爾可夫鏈.

例如，圖3的監(jiān)控器M2可以描述為圖4所示的馬爾可夫鏈.

圖4 監(jiān)控器M2對應(yīng)的馬爾可夫鏈Fig.4 Markov chain of monitor M2

(7)

x=Ax+b或(I-A)·x=b

(8)

根據(jù)上述方程組，可求得x的唯一解，而xq0的值就是監(jiān)控器中不可監(jiān)控的有限序列的概率.所以，當(dāng)xq0=0時(shí)，公式是可監(jiān)控的；當(dāng)xq0=1時(shí)，公式是弱不可監(jiān)控的；當(dāng)0

下面，我們將證明公式(8)中x的解的唯一性.

證明：根據(jù)馬爾科夫鏈的性質(zhì)[12,13]可知，矩陣A的特征值λ滿足|λ|<1，因此，I+A+A2+…=∑n≥0An是收斂的，而：

(I-A)·(I+A+A2+…)
=(I+A+A2+A3…)-(A+A2+A3…)=I

算法 1.MPMC算法

輸入：LTL公式φ

輸出：公式φ的可監(jiān)控性概率

1.begin

2.構(gòu)造公式φ的等價(jià)監(jiān)控器Mφ

4.if(U=?)

5. return 1;

6.end if

7.if(U=Qr)

8. return 0;

9.end if

11.求解方程組的唯一解x

12.return (1-xq0)

13.end

MPMC算法的復(fù)雜度.首先，MPMC算法中構(gòu)造公式φ的等價(jià)監(jiān)控器Mφ的復(fù)雜度是雙指數(shù)級的[6].在遍歷監(jiān)控器后，若集合U=?或U=Qr，則可直接返回求解結(jié)果，無需進(jìn)行后續(xù)步驟的求解，此時(shí)，算法的復(fù)雜度是O(22n)，否則，需進(jìn)行線性方程組的求解，而求解方程組的時(shí)間復(fù)雜度是多項(xiàng)式級的，所以，算法的復(fù)雜度也是O(22n).綜上，MPMC算法的復(fù)雜度是O(22n).

因此，根據(jù)x=Ax+b可列出方程組：

解上面的方程組可得：x0=13/14，x1=9/14.因此，PrM(φ2)=1-PrNM(φ2)=1-x0=1/14，即公式φ2的可監(jiān)控性概率為1/14.此算法較之前的計(jì)算方法相比，避免了對無限多項(xiàng)進(jìn)行相加的計(jì)算，表示簡單，計(jì)算亦簡單.

5 實(shí)驗(yàn)與分析

根據(jù)MPMC算法，我們設(shè)計(jì)并實(shí)現(xiàn)了原型系統(tǒng)工具monic.monic是在Linux環(huán)境下基于Spot[14]，并使用C++語言和shell腳本語言共同進(jìn)行開發(fā)的，可通過命令行的方式運(yùn)行.考慮到算法的性能會受到公式規(guī)模大小的影響，因此，我們利用Spot工具進(jìn)行隨機(jī)用例公式集合的生成.Spot工具可以通過設(shè)置LTL公式的原子命題個數(shù)及語法樹大小(公式長度)來隨機(jī)生成不同的公式，每個用例集合為一百個LTL公式，用例公式的參數(shù)設(shè)計(jì)如表1所示,表中的ap_nums表示原子命題個數(shù)，length表示公式的長度.本次實(shí)驗(yàn)的機(jī)器配置為8G內(nèi)存，雙核CPU，實(shí)驗(yàn)使用Ubuntu16.04的64位Linux操作系統(tǒng)，gcc 5.4.0編譯器.

表1 實(shí)驗(yàn)用例參數(shù)Table 1 Experimental use case parameters

在monic中，概率可監(jiān)控性求解器分為兩種類型，其算法原理都是基于馬爾可夫鏈的，只是一種是基于概率模型檢測器PRISM[15]實(shí)現(xiàn)的，一種是基于SMT[16]求解器實(shí)現(xiàn)的，而基于SMT求解器的又可以分為基于Z3[17]和基于CVC4[18]的兩種.

對于MPMC算法的三種實(shí)現(xiàn)，我們使用表1設(shè)計(jì)的用例集合分別對其進(jìn)行了實(shí)驗(yàn)，實(shí)驗(yàn)表明MPMC算法的三種實(shí)現(xiàn)的求解結(jié)果是一樣的.為了驗(yàn)證算法結(jié)果的正確性，我們使用文獻(xiàn)[9]中的算法工具對表1設(shè)計(jì)的用例集合進(jìn)行了可監(jiān)控性和弱可監(jiān)控性的判定求解，并根據(jù)弱不可監(jiān)控公式的可監(jiān)控性概率為0，可監(jiān)控公式的可監(jiān)控性概率為1，不可監(jiān)控但弱可監(jiān)控公式的可監(jiān)控性概率取值范圍為(0,1)的原則，通過bash腳本將MPMC算法的實(shí)驗(yàn)結(jié)果與可監(jiān)控性和弱可監(jiān)控性的判定結(jié)果進(jìn)行了對比.從對比結(jié)果可以看出，所有弱不可監(jiān)控的公式通過MPMC算法計(jì)算得到的可監(jiān)控性概率都等于0，所有可監(jiān)控的公式通過MPMC算法計(jì)算得到的可監(jiān)控性概率都等于1，所有不可監(jiān)控但弱可監(jiān)控的公式通過MPMC算法計(jì)算得到的可監(jiān)控性概率的取值范圍都是(0,1).因此，我們可以判斷MPMC算法的實(shí)驗(yàn)結(jié)果是正確的.

此外，為了對比三種實(shí)現(xiàn)的性能差異，我們對其進(jìn)行了對比實(shí)驗(yàn)，實(shí)驗(yàn)結(jié)果如圖5所示.

圖5 MPMC算法的實(shí)驗(yàn)結(jié)果對比圖Fig.5 Comparison of experimental results of MPMC algorithm

圖5中x軸表示原子命題個數(shù)，y軸表示公式長度，z軸表示求解時(shí)間的對數(shù)(對數(shù)的底取10)，圖中的正三角圖標(biāo)表示基于PRISM實(shí)現(xiàn)的實(shí)驗(yàn)結(jié)果，圓型圖標(biāo)表示基于Z3實(shí)現(xiàn)的實(shí)驗(yàn)結(jié)果，倒三角圖標(biāo)表示基于CVC4實(shí)現(xiàn)的實(shí)驗(yàn)結(jié)果.通過圖中實(shí)驗(yàn)結(jié)果的對比，我們發(fā)現(xiàn)，兩種基于SMT求解器實(shí)現(xiàn)的算法，其求解效率明顯高于基于PRISM實(shí)現(xiàn)的算法，而基于SMT求解器實(shí)現(xiàn)的兩種算法中，基于CVC4實(shí)現(xiàn)的算法的求解效率亦高于基于Z3實(shí)現(xiàn)的算法.這是因?yàn)榛赑RISM實(shí)現(xiàn)的算法，其在利用PRISM進(jìn)行求解的過程中，需要花費(fèi)大量的時(shí)間先進(jìn)行建模，然后求解；而基于SMT求解器實(shí)現(xiàn)的算法，由于近年來SMT求解器已經(jīng)發(fā)展地相當(dāng)成熟，且其無需進(jìn)行復(fù)雜的建模，只需求解即可.然而值得注意的是，無論是基于PRISM實(shí)現(xiàn)的算法，還是基于SMT求解器實(shí)現(xiàn)的算法，其求解能力都是相同的，即不管求解速度如何，只要其中一種實(shí)現(xiàn)(不)能解得結(jié)果，其余兩種都(不)能解得結(jié)果.這是因?yàn)镸PMC算法是基于監(jiān)控器的，因此，其都會出現(xiàn)隨著公式規(guī)模的增大，出現(xiàn)監(jiān)控器無法被成功構(gòu)造的情況，即無法求解的情況.例如，當(dāng)公式中原子命題的個數(shù)為9，公式長度為100時(shí)，對于這種情況，圖中未給出求解結(jié)果.

6 結(jié)束語

本文根據(jù)運(yùn)行時(shí)驗(yàn)證的需求，在可監(jiān)控性和弱可監(jiān)控性的基礎(chǔ)上提出了概率可監(jiān)控性的概念，然后重點(diǎn)研究了概率可監(jiān)控性的求解算法，并對算法中用到的定理進(jìn)行了理論證明.此外，本文還對所提算法進(jìn)行了代碼實(shí)現(xiàn)，并通過實(shí)驗(yàn)證明了算法的正確性.