線性時序邏輯公式的可監控性量化算法

陳云云，陳 哲

(南京航空航天大學 計算機科學與技術學院，南京 211106) (軟件新技術與產業化協同創新中心，南京 211106) (高安全系統的軟件開發與驗證技術工業和信息化部重點實驗室，南京 211106)

1 引 言

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

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

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

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

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

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

2 理論知識

2.1 可監控性、弱可監控性

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

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

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

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

圖1 公式Xp∧GFp的等價監控器Fig.1 Monitor of formula Xp∧GFp

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

2.2 馬爾可夫鏈

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

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

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

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

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

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

(1)

其中，

(2)

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

3 概率可監控性

為了確保對系統進行運行時驗證時所使用的約束公式是合理的，需要對約束公式的可監控性和弱可監控性進行判定.但是，可監控性的要求過于嚴格，而弱可監控性又僅僅解決了“存在”的問題.

圖2 監控器的結構圖Fig.2 Structure diagram of monitor

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

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

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

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

(3)

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

4 概率可監控性的求解算法

4.1 直接求解的不可行性

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

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

圖3 公式φ2的等價監控器M2Fig.3 Monitor of formula φ2

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

4.2 概率可監控性問題的補問題

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

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

(4)

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

(5)

(6)

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

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

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

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

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

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

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

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

定義 11.給定一個監控器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.

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

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

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

(7)

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

(8)

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

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

證明：根據馬爾科夫鏈的性質[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公式φ

輸出：公式φ的可監控性概率

1.begin

2.構造公式φ的等價監控器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算法中構造公式φ的等價監控器Mφ的復雜度是雙指數級的[6].在遍歷監控器后，若集合U=?或U=Qr，則可直接返回求解結果，無需進行后續步驟的求解，此時，算法的復雜度是O(22n)，否則，需進行線性方程組的求解，而求解方程組的時間復雜度是多項式級的，所以，算法的復雜度也是O(22n).綜上，MPMC算法的復雜度是O(22n).

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

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

5 實驗與分析

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

表1 實驗用例參數Table 1 Experimental use case parameters

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

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

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

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

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

6 結束語

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