線性時(shí)間屬性中近似安全性和活性的刻畫

常玉婷, 潘海玉

(桂林電子科技大學(xué) 計(jì)算機(jī)與信息安全學(xué)院,廣西 桂林 541004)

形式規(guī)約作為形式化方法的主要內(nèi)容,包括性質(zhì)規(guī)約和模型規(guī)約[1]。在性質(zhì)規(guī)約中,包含安全性和活性的線性時(shí)間屬性的規(guī)約對(duì)于系統(tǒng)驗(yàn)證有著非常重要的作用。直觀上說,安全性是指“壞”的事情永遠(yuǎn)不會(huì)發(fā)生,活性是指“好”的事情最終會(huì)發(fā)生[2]。例如,在系統(tǒng)運(yùn)行時(shí)可能會(huì)存在多個(gè)進(jìn)程,這些進(jìn)程不會(huì)同時(shí)進(jìn)入臨界區(qū),這就保證了系統(tǒng)的安全性;若某個(gè)進(jìn)程在等待區(qū),則它最終會(huì)進(jìn)入臨界區(qū),這就保證了系統(tǒng)的活性。

在過去的幾十年中,線性時(shí)間屬性已經(jīng)得到了廣泛研究。Lamport[3]首先引入安全性和活性的概念。隨后Alpern等[4]在此基礎(chǔ)之上證明了任何一個(gè)線性時(shí)間屬性都可表達(dá)為安全性和活性的交集。進(jìn)一步,Alpern等[5]又從自動(dòng)機(jī)角度對(duì)安全性和活性進(jìn)行研究,首次給出安全性和活性的Büchi自動(dòng)機(jī)刻畫。Sistla[6]的研究表明,安全性和活性可通過線性時(shí)態(tài)邏輯公式進(jìn)行邏輯刻畫。Kupferman等[7]提出了一種檢測LTL公式是否是安全性公式的算法,通過給定的安全性構(gòu)造一個(gè)檢測壞前綴的Büchi自動(dòng)機(jī),同時(shí)構(gòu)造了一個(gè)緊密自動(dòng)機(jī)對(duì)已收集的中間數(shù)據(jù)進(jìn)行分析,以防雙指數(shù)爆炸。除此之外,還有許多有關(guān)線性時(shí)間屬性的研究[8]。

近年來,人們開始研究在概率、模糊和度量等背景下系統(tǒng)的量化驗(yàn)證問題。Kupferman等[9]通過加入概率組件,引入了一種概率壞前綴的概念,以此擴(kuò)展安全性在實(shí)際驗(yàn)證中的適用性。Faran等[10]利用概率給出安全等級(jí)的定義,并研究了利用確定性和非確定性自動(dòng)機(jī)及線性時(shí)態(tài)邏輯公式來確定語言的安全等級(jí)的問題。李永明等[11]將經(jīng)典遷移系統(tǒng)與模糊理論中的不確定性相結(jié)合,定義了可能性遷移系統(tǒng)的概念,并提出一種可能性測度方法,在此基礎(chǔ)上定義模糊線性時(shí)間屬性。此外,李永明等[12]將線性時(shí)間屬性推廣到多值邏輯上,根據(jù)Heyting代數(shù)理論,定義了真值度的概念,并給出安全性和活性在多值邏輯中的定義。Alfaro等[13]提出了度量遷移系統(tǒng)的概念,利用度量空間理論[17]來刻畫線性時(shí)間屬性,并給出了線性時(shí)態(tài)邏輯在度量空間上的一種擴(kuò)展形式。除了研究線性時(shí)間屬性,人們還研究了分支時(shí)間屬性[18]及模型檢測[14-16]等在概率、模糊和度量等背景下的性質(zhì)。

文獻(xiàn)[11]根據(jù)格的理論給出真值度的概念,并提出安全性和活性,但基于真值度的計(jì)算方式不能很好地刻畫系統(tǒng)和屬性之間的滿足程度。鑒于此,采用度量理論中的線性距離來量化系統(tǒng)多大程度滿足線性時(shí)間屬性,這個(gè)距離的值是系統(tǒng)與屬性之間距離差值的絕對(duì)值,若距離小于一個(gè)值,且值的范圍為[0,1],則表示系統(tǒng)滿足屬性的近似程度,值越小表示近似程度越高,當(dāng)值為0時(shí),表示系統(tǒng)滿足這個(gè)屬性。將線性距離與模糊理論相結(jié)合,采用距離刻畫系統(tǒng)與屬性之間關(guān)系的方法,定義出近似安全性與近似活性來量化系統(tǒng)滿足其屬性的程度。

1 近似線性時(shí)間屬性

1.1 線性距離

命題距離DP、跡距離DT及線性距離D分別刻畫了賦值之間的關(guān)系、(V(AP))ω中串之間的關(guān)系及FLT屬性之間的關(guān)系[12],定義分別如下:(V(AP))ω,下列結(jié)論成立:

1)Df(σ^,pref(P1))≤α,當(dāng)且僅當(dāng)存在σ∈(V(AP))ω,使得D(σ^σ,P1)≤α;

2) 若D(P1,P2)≤α,則Df(pref(P1),pref(P2))≤α。

證明 1)從左推右:設(shè)Df(σ^,pref(P1))≤α,則存在ρ^∈pref(P1),有DfT(σ^,ρ^)≤α。 令σ∈(V(AP))ω,且ρ^σ∈P1。將σ^擴(kuò)展為σ^σ。根據(jù)跡距離的定義,

1.2 近似安全性和近似活性

在系統(tǒng)運(yùn)行過程中,安全性保證“壞”的事情不會(huì)發(fā)生。經(jīng)典安全性的定義[2-3]有2種不同的定義形式,分別從好前綴和壞前綴定義而來,具體如下。

1)設(shè)P為AP上的線性時(shí)間(linear-time, 簡稱LT)屬性。對(duì)于所有跡σ∈(2AP)ω,若對(duì)任意i≥0,存在σ′∈(2AP)ω,使得σ≤iσ′?P,則σ?P,稱P是一個(gè)安全性。

2)設(shè)P為AP上的LT 屬性,若對(duì)所有跡σ∈(2AP)ω,且σ?P,存在σ^∈pref(σ),使得對(duì)任意σ′∈(2AP)ω,σ^σ′?P,則稱P是一個(gè)安全性。這里稱σ^為P的一個(gè)壞前綴。

通過引入距離閾值α,將好前綴的定義從經(jīng)典安全性推廣到近似安全性。具體定義如下。

定義1 設(shè)P為AP上的FLT 屬性,α∈[0,1]。對(duì)所有σ∈(V(AP))ω,若對(duì)任意i≥0,存在σ′∈(V(AP))ω,使得D(σ≤iσ′,P)≤α,則D(σ,P)≤α,稱P是一個(gè)α-安全性。

對(duì)于一個(gè)0-安全性P,由定義1 知,對(duì)任意i≥0,存在σ′∈(V(AP))ω,使得D(σ≤iσ′,P)=0,則D(σ,P)=0,即σ∈P。因此,0-安全性就是經(jīng)典的安全性。

相較于安全性,活性保證“好”的事情最終會(huì)發(fā)生。經(jīng)典活性的定義[3]為:設(shè)P為AP上的LT 屬性,若對(duì)任意σ^∈(2AP)*,存在σ′∈(2AP)ω,使得σ^σ′?P,則稱P是一個(gè)活性。

與近似安全性類似,以下給出活性的一種定量推廣形式——α-活性。

定義2 令α∈[0,1],P為AP上的FLT屬性。若對(duì)任意σ^∈(V(AP))*,存在σ′∈(V(AP))ω,有D(σ^σ′,P)≤α,則稱P是一個(gè)α-活性。

對(duì)于一個(gè)0-活性P,由定義2知,對(duì)任意σ^∈(V(AP))*,存在σ′∈(V(AP))ω,有D(σ^σ′,P)=0,即σ^σ′∈P。因此,0-活性就是經(jīng)典的活性。

2 近似線性時(shí)間屬性的邏輯刻畫

模糊遷移系統(tǒng)是一個(gè)五元組F=(S,→,s0,AP,L),其中:S為狀態(tài)集合;→?S×S為遷移關(guān)系;s0∈S為初始狀態(tài);AP為原子命題集合;L:S→V(AP)為標(biāo)記函數(shù)。

由定義知,模糊遷移系統(tǒng)和經(jīng)典遷移系統(tǒng)的主要區(qū)別是標(biāo)記函數(shù)。根據(jù)文獻(xiàn)[2],經(jīng)典遷移系統(tǒng)的標(biāo)記函數(shù)為L:S→2AP,狀態(tài)上的標(biāo)記是原子命題集合中的元素。而本研究的模糊遷移系統(tǒng),其狀態(tài)上的標(biāo)記是原子命題AP的一個(gè)賦值。

模糊遷移系統(tǒng)可表示為帶標(biāo)簽的有向圖,如圖1所示。圖中的圓圈表示系統(tǒng)的狀態(tài),圓圈中的符號(hào)代表該狀態(tài)名,圓圈旁邊的部分表示該狀態(tài)上原子命題的賦值,若賦值為0,則省略該原子命題。例如,狀態(tài)s1是模糊遷移系統(tǒng)的一個(gè)狀態(tài),s1的標(biāo)記函數(shù)為L(s1),則根據(jù)圖1可知,L(s1)(p)=0.7,L(s1)(r)=0.4。在狀態(tài)s2中原子命題r賦值為0,故省略。圖1中的有向邊表示狀態(tài)之間的遷移,一條無出發(fā)結(jié)點(diǎn)的有向邊指向的狀態(tài)為初始狀態(tài),如狀態(tài)s0是該模糊遷移系統(tǒng)的初始狀態(tài)。

圖1 模糊遷移系統(tǒng)

定義3[19]給定原子命題集AP,AP上的FLTL公式的語法遞歸定義為

其中,p∈AP,c∈[0,1]。

以下給出FLTL 公式在(V(AP))ω上的語義解釋。

給定一個(gè)FLTL公式φ和閾值α∈[0,1],φ在α約束下表示一個(gè)FLT屬性Lα(φ),定義為

若Lα(φ)是一個(gè)α-安全性,則稱φ為α-安全性公式;同樣,若Lα(φ)是一個(gè)α-活性,則稱φ為α-活性公式。因當(dāng)α取值為0時(shí),α-安全性和α-活性即為經(jīng)典的安全性和活性,因此,此時(shí)α-安全性公式和α-活性公式為安全性公式和活性公式。

定理1 設(shè)p∈AP,c∈[0,1],且α∈[0,1]。在FLTL公式中,以下結(jié)論成立:

1)true和p?c-是α-安全性公式;

2)若φ1、φ2 是α-安全性公式,則φ1 ∧φ2,φ1 ∨φ2,Xφ1,Gφ1 和φ1Wφ2 也是α-安全性公式。

這里只證明p?c-。 其余證明與文獻(xiàn)[19]的證明類似。

設(shè)對(duì)所有σ∈(V(AP))ω,D(σ,Lα(φ))＞α,則對(duì)任意ρ∈Lα(φ),有DT(σ,ρ)＞α。 根據(jù)跡距離DT的定義,存在i∈N,使得DP(σi,ρi)＞α。 設(shè)i=0時(shí),DP(σ0,ρ0)≤α。此時(shí),對(duì)任意的p∈AP,|σ0(p)-ρ0(p)|≤α。 將ρ0擴(kuò)展為無限跡ρ′=ρ0σ1σ2…,則

要判斷φ是否是0.2-安全性公式,只需判斷Lα(φ)是否為0.2-安全性。設(shè)σ∈L0.2(φ)且σ?P,則存在j≥0,使得σj(p)≥0.8且σj(r)≥0.8。根據(jù)定義4,

定理2 令α∈[0,1]。在FLTL公式中,以下結(jié)論成立:

1)當(dāng)α∈[0,1)時(shí),true是α-活性公式;

2)p?c-是α-活性公式;

3)若φ1 和φ2 是α-活性公式,則φ1 ∧φ2 是α-活性公式;

4)若φ1 或φ2 是α-活性公式,則φ1 ∨φ2 是α-活性公式;

5)若φ2是α-活性公式,則φ1Uφ2和φ1Wφ2都是α-活性公式;

6)若φ1是α-活性公式,則Xφ1和Fφ1都是α-活性公式。

2)令φ=p?c-。設(shè)φ不是α-活性公式,則存在^σ∈ (V(AP))*,對(duì) 任 意σ′ ∈ (V(AP))ω,有D（^σσ′,Lα(φ)）＞α。令^σσ′=σ。由線性距離D的定義知,對(duì)任意ρ∈Lα(φ),TD(σ,ρ)＞α。進(jìn)一步,由跡距離DT的定義,存在i≥0,使得DP(σi,ρi)＞α。又根據(jù)定理1的證明,當(dāng)i=0時(shí),DP(σ0,ρ0)＞α,因此

因此φ是α-活性公式。

3)設(shè)φ1 和φ2 是α-活性公式。令φ=φ1 ∧φ2,σ∈Lα(φ),根據(jù)Lα(φ)的定義,‖φ‖(σ)＞α,即

所以‖φ1‖(σ)＞α且‖φ2‖(σ)＞α,即σ∈Lα(φ1)且σ∈Lα(φ2)。因?yàn)棣?和φ2是α-活性公式,則對(duì)任意^σ∈(V(AP))*,存在σ′∈(V(AP))ω,有

因此φ是α-活性公式。

4)設(shè)φ1 或φ2 是α-活性公式。令φ=φ1 ∨φ2,σ∈Lα(φ),根據(jù)Lα(φ)的定義,‖φ‖(σ)＞α,即

所以有‖φ1‖(σ)＞α或‖φ2‖(σ)＞α,即σ∈Lα(φ1)或σ∈Lα(φ2)。不妨設(shè)σ∈Lα(φ1)。當(dāng)φ1是α-活性公式時(shí),對(duì)任意^σ∈(V(AP))*,都存在σ′∈(V(AP))ω,有D(^σσ′,Lα(φ1))≤α。因此,存在ρ∈Lα(φ1),使得DT(^σσ′,ρ)≤α。故

φ1是α-活性公式,所以Fφ1 是α-活性公式。

例2 設(shè)AP={p,r},V(AP)為AP在[0,1]f上所有賦值的集合。令P是一個(gè)0.5-活性,對(duì)所有σ∈P滿足:任意i≥0,σi(p)＜0.5或σi(r)＜0.5?，F(xiàn)在使用FLTL公式描述該屬性。令

根 據(jù)L0.5(φ)的 定 義,σ∈L0.5(φ)。 故P?L0.5(φ)。綜上所述,Lα(φ)=P成立,所以(p?1)U(r?1)是0.5-活性公式。

3 實(shí)例

考慮一個(gè)由墻、窗戶、加熱器和控制器組成的房間?？刂破鞯哪康氖潜M可能將溫度維持在用戶舒適的范圍。因?yàn)椤笆孢m”是一個(gè)模糊的概念,人們不能很精確地將“舒適”的意思描述出來,每個(gè)人對(duì)“舒適”的描述也會(huì)不一樣,所以可以將“舒適”一詞通過以下模糊集的定義來解釋[21-23]:

其中:Te(t)為室外溫度;T(t)為當(dāng)前室內(nèi)溫度;E(t)為特定于墻體和窗戶的熱交換系數(shù);H(t)為加熱器的功率。

假設(shè)溫度控制器可接收的溫度范圍為10～45℃,當(dāng)室內(nèi)溫度低于17℃時(shí),加熱器開啟;當(dāng)室內(nèi)溫度高于24℃時(shí),加熱器關(guān)閉;當(dāng)室溫處于20～22℃時(shí),加熱器處于睡眠模式,當(dāng)處于睡眠模式的時(shí)間超過60 min時(shí),加熱器將自動(dòng)關(guān)閉。設(shè)置控制器每30 min接收一次溫度讀數(shù),然后判斷是否對(duì)加熱器進(jìn)行開或關(guān)或睡眠的操作。

對(duì)房間溫度的舒適度演化進(jìn)行建模。設(shè)

其中,S={s0,s1,s2},AP={t,c},其中:狀態(tài)s0表示加熱器處于關(guān)閉狀態(tài);狀態(tài)s1表示加熱器處于加熱狀態(tài);狀態(tài)s2表示加熱器處于睡眠狀態(tài);c表示當(dāng)前溫度下用戶的舒適度;t表示溫度系數(shù)(即當(dāng)前溫度/100),AP的賦值是在[0,1]范圍內(nèi)。為了方便計(jì)算,所有的數(shù)值均保留小數(shù)點(diǎn)后3位。設(shè)加熱器開啟的功率為0.06℃/min,睡眠模式的功率為0.03℃/min。墻體和窗戶的熱交換系數(shù)為0.005℃/min。令i≥1,可使用公式[22]

計(jì)算大約30imin后的室溫,再通過x求μc。 公式所計(jì)算的具體值如表1所示。

根據(jù)表1,可以構(gòu)建FTS。如圖2所示,此時(shí)室溫為16℃,加熱器處于關(guān)閉狀態(tài)。由于溫度低于17℃,開啟加熱器,到達(dá)狀態(tài)s1。在30 min后,溫度控制器接收當(dāng)前室溫,根據(jù)上述公式,計(jì)算可得室溫為17.65℃,此時(shí)用戶舒適度仍為0,繼續(xù)處于狀態(tài)s1。通過計(jì)算,在i=4,即120 min后,室內(nèi)溫度將升至約20.3℃,此時(shí)用戶舒適度約為0.767,此時(shí)加熱器切換為睡眠模式,到達(dá)狀態(tài)s2。 由于加熱器處于睡眠模式的時(shí)間超過60 min,加熱器i=7時(shí)切換為關(guān)閉狀態(tài)s1。這里不再考慮在加熱器從睡眠模式關(guān)閉后的情況。

圖2 FTS

表1 溫度控制器接收t及s和c的關(guān)系

所構(gòu)建的FTS有2個(gè)屬性需要考慮:一是“安全性”,就是用戶一直感到舒適;二是“活性”,就是最終會(huì)到達(dá)一個(gè)合適的舒適度范圍。假設(shè)滿足安全性的“好”的舒適度范圍為[0.6,0.9],而滿足活性的合適的舒適度范圍為[0.6,1]。

首先考慮安全性的規(guī)范。根據(jù)圖2,令P是一個(gè)FLT屬性,且P是一個(gè)0.1-安全性,對(duì)所有σ∈P滿足:任意i≥0,0.6≤σi(c)≤0.9。因?yàn)椤鞍踩浴笔且ＷC一直在舒適度的范圍,所以使用FLTL公式中的G描述該系統(tǒng)所刻畫的安全性。令φ=G(c?1),根據(jù)Lα(φ)的定義,

因此,G(c?1)是0.1-安全性公式。0.1-安全性表示:該系統(tǒng)所滿足的舒適度范圍和滿足安全性的舒適度范圍之間,只要保證在0.1誤差以內(nèi),都可視為是“安全”的。

根據(jù)圖2,令P為一個(gè)FLT 屬性,且P是一個(gè)0.3-活性,對(duì)所有σ∈P滿足:存在i≥0,σi(c)＜0.7。因?yàn)椤盎钚浴笔亲罱K要處于舒適的狀態(tài),所以使用FLTL公式中的F描述該屬性。令φ=F(c?1),根據(jù)Lα(φ)的定義,所以,σ?L0.3(φ),這與假設(shè)矛盾。故σ∈P,L0.3(φ)?P。 設(shè)σ∈P,則存在i≥0,σi(c)＜0.7。根據(jù)定義4,

根據(jù)L0.3(φ)的 定 義,σ∈L0.3(φ)。 故P?L0.3(φ)。綜上所述,Lα(φ)=P成立,所以F(c?1)是0.3-活性公式。0.3-活性表示:該系統(tǒng)所滿足的舒適度范圍和滿足活性的舒適度范圍之間,只要保證在0.3誤差內(nèi),都可以視為系統(tǒng)滿足該屬性。

4 結(jié)束語

研究了模糊背景下的近似安全性和近似活性及其邏輯和自動(dòng)機(jī)刻畫。通過引入距離閾值α∈[0,1],定義了α-安全性和α-活性,并通過一些例子來描述所給出的定義,最后通過模糊線性時(shí)態(tài)邏輯公式給出近似安全性和近似活性的邏輯刻畫。下一步將考慮研究模糊背景下近似安全性和近似活性相關(guān)驗(yàn)證算法及自動(dòng)機(jī)的刻畫。