線性時序邏輯公式的可監(jiān)控性量化算法

陳云云，陳 哲

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

1 引 言

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

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

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

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

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

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

2 理論知識

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

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

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

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

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

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

對于那些第二個符號是p的有限序列，其已到達狀態(tài)2，無論未來對其如何擴展都不可能使其成為公式的(好)壞前綴；但是，對于那些第二個符號是!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是標簽函數(shù).

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

一般將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)進行運行時驗證時所使用的約束公式是合理的，需要對約束公式的可監(jiān)控性和弱可監(jiān)控性進行判定.但是，可監(jiān)控性的要求過于嚴格，而弱可監(jiān)控性又僅僅解決了“存在”的問題.

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

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

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

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

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

(3)

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

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

4.1 直接求解的不可行性

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

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

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

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

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

定義 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)中的分子分母有一定的特點，即其分母都是一個以|Σ|為公比的等比數(shù)列的和，隨著長度n的增大，分母也不斷增大，且當長度n趨于正無窮大時，分母也趨于正無窮大.這一特點與數(shù)學領域中的施托爾茲定理(The O′Stolz theorem)[11]非常契合.施托爾茲定理常用于處理數(shù)列不定式的極限問題，根據(jù)施托爾茲定理可得：

(5)

(6)

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

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

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

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

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

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

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

此外，我們還注意到監(jiān)控器本身就是一個特殊的確定性有限自動機，且其是完全的(complete)，即對于監(jiān)控器中的任意狀態(tài)，以該狀態(tài)為源點出發(fā)的所有邊上的標簽對應的公式的析取等價于true(對應符號集合的并為Σ)，且任意兩條邊上標簽對應的公式的合取等價于false(對應符號集合的交集為空集).而監(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)與其直接后繼之間的遷移上的標簽對應的符號的并集是符號全集2AP，且任意兩條遷移對應的符號集合沒有交集.因此，我們用每條遷移上標簽對應的符號集合占符號全集Σ=2AP的比例來表示遷移概率.第二個問題，由于監(jiān)控器是一個確定性的有限自動機，所以，其只有一個初始狀態(tài)q0.因此，我們令ιinitr(q0)=1，且令其它的q∈Qr∧q≠q0，ιinitr(q)=0，這滿足∑q∈Qrιinitr(q)=1.除此之外，我們將監(jiān)控器中的狀態(tài)輸出添加到馬爾科夫鏈的標簽函數(shù)Lr中去(在圖中，我們將狀態(tài)輸出和狀態(tài)放在一起)，這是因為在后續(xù)算法的設計中，狀態(tài)輸出信息必不可少.通過上述定義，我們可以將監(jiān)控器描述為一個標準馬爾可夫鏈.

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

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

(7)

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

(8)

根據(jù)上述方程組，可求得x的唯一解，而xq0的值就是監(jiān)控器中不可監(jiān)控的有限序列的概率.所以，當xq0=0時，公式是可監(jiān)控的；當xq0=1時，公式是弱不可監(jiān)控的；當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ā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算法的復雜度.首先，MPMC算法中構(gòu)造公式φ的等價監(jiān)控器Mφ的復雜度是雙指數(shù)級的[6].在遍歷監(jiān)控器后，若集合U=?或U=Qr，則可直接返回求解結(jié)果，無需進行后續(xù)步驟的求解，此時，算法的復雜度是O(22n)，否則，需進行線性方程組的求解，而求解方程組的時間復雜度是多項式級的，所以，算法的復雜度也是O(22n).綜上，MPMC算法的復雜度是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.此算法較之前的計算方法相比，避免了對無限多項進行相加的計算，表示簡單，計算亦簡單.

5 實驗與分析

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

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

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

對于MPMC算法的三種實現(xiàn)，我們使用表1設計的用例集合分別對其進行了實驗，實驗表明MPMC算法的三種實現(xiàn)的求解結(jié)果是一樣的.為了驗證算法結(jié)果的正確性，我們使用文獻[9]中的算法工具對表1設計的用例集合進行了可監(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算法的實驗結(jié)果與可監(jiān)控性和弱可監(jiān)控性的判定結(jié)果進行了對比.從對比結(jié)果可以看出，所有弱不可監(jiān)控的公式通過MPMC算法計算得到的可監(jiān)控性概率都等于0，所有可監(jiān)控的公式通過MPMC算法計算得到的可監(jiān)控性概率都等于1，所有不可監(jiān)控但弱可監(jiān)控的公式通過MPMC算法計算得到的可監(jiān)控性概率的取值范圍都是(0,1).因此，我們可以判斷MPMC算法的實驗結(jié)果是正確的.

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

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

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

6 結(jié)束語

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