安 杰, 張苗苗

(同濟大學 軟件學院,上海 201804)

文獻[7]證明了基于實時自動機的 LDI性質的模型檢驗問題是可判定的.實時自動機可以看作是一類特殊的時間自動機,即只有一個時鐘變量并且每次遷移都會重置該時鐘.基于該工作,學術界研究了在比實時自動機表達能力更強的模型(如時間自動機、混成自動機)下LDI公式的模型檢驗問題[8-12].其中,文獻[11,12]提出了一些對于時間自動機下LDI的模型檢驗的高效算法,并將這些方法擴展到時間自動機網(wǎng)絡中[13].

那么對于時段演算是否可以找到一個比 LDI更大的子集,其模型檢驗問題仍然是可以判定的.一個比較自然的想法是,對 LDI進行擴展,例如,加入布爾連接符和模態(tài)詞切變(chop),這樣就形成擴展線性時段不變式(extended linear duration invariants,簡稱ELDI).根據(jù)文獻[6]的結論,在離散時間語義和連續(xù)時間語義下,ELDI的可滿足性(satisfiability)和正確性(validity)都是不可判定的.Martin等人證明了在離散時間語義和連續(xù)時間語義下,對于有限狀態(tài)機下ELDI的模型檢驗問題是不可判定的[14].因此,他們提出了ELDI的一個近似語義,并且給出了在該近似語義和離散時間條件下的模型檢驗算法.由于該算法復雜度過高,在實際系統(tǒng)中很難運用,所以Martin等人提出了另外一種近似語義,并將ELDI的模型檢驗問題轉化為Presburger算術[15].受到該工作的啟發(fā),我們證明了在標準離散時間語義下基于時間自動機的ELDI有界模型檢驗問題是可以判定的,并給出了一種高效的模型檢驗算法[16].更進一步地,我們討論了在連續(xù)時間語義下基于時間自動機的 ELDI的有界模型檢驗問題,給出了復雜度為三階指數(shù)的判定算法[17].在此指出,文獻[16,17]與本文所說的有界模型檢驗均特指對于ELDI公式中觀測區(qū)間長度?有上界,即對于形式b≤?≤e,其中的上界e有界.

在本文中,我們研究在標準連續(xù)時間語義下基于實時自動機的 ELDI的有界模型檢驗問題.證明了該問題是可以判定的,并且給出模型檢驗算法.與文獻[7]的區(qū)別是,文獻[7]討論的是基于實時自動機的線性時段不變式(LDI)的模型檢驗問題,而本文討論的是基于實時自動機的擴展線性時段不變式(ELDI)的模型檢驗問題,針對的公式更加復雜.與文獻[16]比較最主要的一個不同點是,本文關注于連續(xù)時間語義,而文獻[16]關注的是離散時間語義.與文獻[17]比較,本文討論的模型是實時自動機,可以得到更加簡便的模型檢驗算法,在多個方面降低了時間復雜度,提高了算法實際運行效率.

本文驗證方法的基本思路如下.

· 第 1步,運用符號化的思想,在實時自動機上利用深度優(yōu)先搜索找到所有滿足觀測時長約束的符號化路徑片段;

· 第2步,將每條路徑轉化為一個量詞線性算術表達式(quantified linear real arithmetic,簡稱QLRA);

· 第3步,將得到的所有量詞線性算術表達式運用量詞消去工具(例如REDLOG)求解.

在第1步中,我們定義了符號化路徑片段,給出了相應的求取方法,并且有效地縮小了搜索空間.在第2步中,我們詳細定義并構造了組成量詞線性算術表達式的不等式約束,并且采用一些方法減少量詞的引入個數(shù).由于量詞消去的復雜度與量詞個數(shù)相關,因此第2步的處理也加快了第3步量詞消去的實際運行速度.

本文第 1節(jié)對相關基礎知識進行回顧,包括實時自動機和擴展的線性時段不變式,并給出本文涉及的量詞線性算術的定義,方便后文敘述.第 2節(jié)對于運用符號化的思想在實時自動機上利用深度優(yōu)先搜索找到所有滿足觀測時長約束的符號化路徑片段進行描述.第 3節(jié)介紹如何將一條符號化路徑片段轉化為一個量詞線性算術表達式.第4節(jié)根據(jù)量詞線性算術表達式結果給出ELDI模型檢驗的判定結果以及相關定理.第5節(jié)給出工具實現(xiàn)描述和實驗結果.最后對全文進行總結.

1 基礎知識及相關定義

本節(jié)首先介紹實時自動機,實時自動機作為本文討論的模型檢驗問題中的模型語言.之后介紹擴展線性時段不變式(ELDI),ELDI作為本文模型檢驗問題中的需求描述邏輯.第 3節(jié)給出量詞線性算術的定義.為了敘述簡潔,本文固定一組命題集合記為P.

1.1 實時自動機

實時自動機(real-time automaton,簡稱 RTA)[18]可以看作時間自動機(timed automaton)[19]的一個子集,即只含有一個時鐘變量并且每次遷移都重置該時鐘變量.實時自動機是對實時系統(tǒng)建模的主流模型.下面給出實時自動機的定義.

定義1(實時自動機).一個實時自動機RTA是一個6元組A=(S,Σ,Δ,s0,F,μ),其中,

·S是一個有窮狀態(tài)(位置)集合;

·∑是一個有窮字母表;

· Δ?S×∑×S是遷移關系;

·s0∈S是初始狀態(tài);

·F?S是接收狀態(tài)集合;

·μ:Δ→2?≥0{?}是一個時間標簽函數(shù)(μ(Δ)通常是一些區(qū)間的集合,這些區(qū)間的端點一般落在?∪{∞}或者?≥0∪{+∞}).

例1:如圖1所示為一個實時自動機A,對于其6元組,狀態(tài)(位置)集合為S={s0,s1,s2},有窮字母表為∑={a,b,c},初始狀態(tài)為s0,接收狀態(tài)集合為F={s2},遷移集合為Δ={(s0,a,s1),(s1,b,s1),(s1,c,s2)},對應的時間標簽函數(shù)產(chǎn)生的時間標簽為μ(Δ)={[1,2],[1,3],[2,4]}.

特別地,在不影響理解的情況下,本文之后不對狀態(tài)和位置做出區(qū)分.本文討論的實時自動機不涉及茲諾行為(non-Zeno)[19],即每一個可控的循環(huán)最少消耗時間為?∈?＞0.

1.2 擴展線性時段不變式

擴展線性時段不變式是時段演算的一類重要子集,可以看作是在線性時段不變式(LDI)的基礎上引入邏輯連接符(?,?,?)以及模態(tài)詞切變(“;”)得到的.ELDI與 LDI相比具有更加復雜的語法結構,相應地,表達能力也更強.同時對其進行驗證也變得更加困難,特別是模態(tài)詞切變的引入,讓ELDI的模型檢驗問題與LDI的模型檢驗問題有了根本區(qū)別.

擴展線性時段不變式在語法上包括 3個組成部分:狀態(tài)表示式S、線性時段子式D、ELDI子式φ.擴展線性時段不變式的定義如下.

定義2(擴展線性時段不變式).擴展線性時段不變式的結構定義如下.

其中,P∈P表示狀態(tài)變量,ci和c為實數(shù),Ω為一個有窮的下標集合.每一個擴展線性時段不變式都可以表示為如下形式:b≤?≤e?φ,其中,b∈?≥0,e∈?≥0∪{+∞}.

特別地,本文中我們只關注觀測時長上界e有界的情形,本文所指的有界模型檢驗指的也是此種情形.

上面給出了 ELDI的語法介紹,其中包含模態(tài)詞切變,本文統(tǒng)一記為“;”.對于模態(tài)詞切變的解釋為

如圖2所示.

定義3(ELDI的語義解釋Iβ).給定一個實時自動機A和它的一個行為β,對于給定的命題集合P,實時自動機A的狀態(tài)(位置)可能滿足或者不滿足集合P中的命題.那么在連續(xù)時間語義下,擴展線性時段不變式對于該行為的解釋如下.

· 對于狀態(tài)表達式:給定一個時刻t∈?≥0,

Iβ(0)(t)=0 并且Iβ(1)(t)=1;

Iβ(?S)(t)=1-Iβ(S)(t);

Iβ(S1?S2)(t)=max{Iβ(S1)(t),Iβ(S2)(t)}.

· 對于時段:給定一個觀察區(qū)間[t1,t2],其中,t1,t2∈?≥0并且t1≤t2,那么∫S的解釋為

· 對于子式:給定一個觀察區(qū)間[t1,t2],一個ELDI子式φ的解釋為

1.3 量詞線性算術

量詞線性算術(quantified linear real arithmetic,簡稱QLRA)是一種一階邏輯理論.本文涉及的量詞線性算術表達式的語法如下.

定義4(量詞線性算術表達式語法)

其中,c0,c1,...,cn∈?,?∈ {=,＜},其他記號的解釋與一階邏輯和實數(shù)算術相同.

2 尋找滿足觀測時長約束的路徑片段.

本節(jié)介紹給定一個實時自動機A和觀測時長約束[b,e],求取所有滿足時長約束的路徑片段.由于本文討論的時間語義是連續(xù)語義,對于一個時間區(qū)間[t,t′],其包含無窮個時刻點,那么對于從同一個位置出發(fā)具有相同時間長度的執(zhí)行路徑可能有無數(shù)條.因此,本文的基本思路是采用符號化的思想,求取滿足觀測時長約束的符號化路徑片段.

文獻[17]采用基于區(qū)域圖(zone graph)的方法,需要先將自動機模型轉化為區(qū)域圖.求取區(qū)域圖后,在開始搜索時需要引入一個額外時鐘變量t并對區(qū)域圖中的區(qū)域(zone)進行隱式變換,該時鐘變量用來隱式記錄路徑片段的時間長度.但是求取區(qū)域圖在最壞情形下會使得搜索空間呈單指數(shù)擴大.本文基于實時自動機模型,所采用的方法不需要像文獻[17]那樣求取區(qū)域圖并進行處理,而是顯式地刻畫符號化路徑片段的時間長度,這樣大大降低了算法時間復雜度.

2.1 符號化路徑片段的定義

下面對符號化路徑片段及其時間長度給出顯性刻畫.

可見,符號化路徑片段記錄了某個執(zhí)行片段經(jīng)過的狀態(tài)(位置)以及系統(tǒng)在該位置可以停留的時限約束.特別地,對于執(zhí)行片段的最后一個位置,在實時自動機A中沒有遷移從該位置發(fā)生,那么可以認為系統(tǒng)可以在該位置停留的時限約束為[0,+∝].

2.2 符號化路徑片段的搜索算法

特別地,對于一條符號化執(zhí)行片段的第 1個位置,由于不知道開始觀測時系統(tǒng)已在該位置停留了多長時間,因此需要對于其時間長度進行特殊處理,即修改在該位置上停留的時間長度的下界為0,上界不改變.

該算法的輸入是實時自動機A和觀測時長約束[b,e],輸出為所有滿足觀測時長約束的符號化路徑片段的集合Θ.一開始,Θ為空,分別從實時自動機A中每一個狀態(tài)(位置)開始尋找.起初,當前符號化執(zhí)行片段ω為空(?),將棧STK中棧頂?shù)脑刈鳛棣氐南乱粋€位置,判斷當前ω的時間長度與約束[b,e]之間的關系(行9～行10,行19).第1種情況,如果當前ω的時間長度區(qū)間與約束區(qū)間有交集,說明當前ω是一條滿足觀測時長約束的符號化路徑片段,那么將當前ω復制到集合Θ(行 11).然后繼續(xù)向前尋找,查看當前狀態(tài)是否有后繼狀態(tài),如果有,則將所有后繼狀態(tài)加入到棧中(行12～行14),如果沒有,則說明需要回溯(行15～行 18).第2種情況(第1種情況不滿足時進入),如果當前ω的時間長度區(qū)間的最大值小于約束區(qū)間的下界b,則不將ω放入集合Θ中,直接繼續(xù)向前尋找(行12～行18),繼續(xù)尋找過程與第1種情況處理相同.第3種情況(前兩種情況都不滿足時進入),如果當前ω的時間長度區(qū)間的最小值第1次超過了時長約束的上界e(行19),由于是第1次從沒有超過上界變?yōu)槌^上界,這時同樣需要將該符號化執(zhí)行片段加入集合Θ中;然后直接開始回溯,不再向前尋找.直到棧STK為空,說明以s為開始位置的滿足觀測時長約束的符號化執(zhí)行片段已搜索完畢.由于以實時自動機A中所有的狀態(tài)為起點尋找,因此,該算法可以找到所有滿足時長約束的符號化執(zhí)行片段.

Table 1 The algorithm for finding all symbolic path segments whose lengths are in [b,e]表1 尋找所有滿足觀測時長約束[b,e]的符號化路徑片段的算法

2.3 搜索算法的正確性證明

對于算法1的正確性證明,即需要證明:(1) 算法會終止;(2) 通過其找到的集合Θ中任意一條符號化路徑片段ω一定是一條真實的路徑片段,并且時間長度與區(qū)間[b,e]相交;(3) 任意一條A能夠產(chǎn)生的一條符號化路徑片段ω,如果其時間長度與區(qū)間[b,e]相交,那么,它一定在集合Θ中.因此,我們證明如下定理.

定理1(算法1正確性).給定一個實時自動機A和觀測時長約束[b,e],算法1是正確的,即:

· 終止性(termination):算法會終止;

· 可靠性(soundness):如果ω是集合Θ中的一條符號化執(zhí)行路徑,那么,ω一定是A能夠產(chǎn)生的一條符號化路徑的一個片段,并且該符號化執(zhí)行片段的時間長度與區(qū)間[b,e]相交;

· 完備性(completeness):如果ω是A能夠產(chǎn)生的一條符號化路徑的一個片段,并且片段的長度與區(qū)間[b,e]相交,那么,ω一定在集合Θ中.

對于可靠性,假設ω是集合Θ中的一條符號化執(zhí)行路徑,顯然,根據(jù)算法 1找到的執(zhí)行片段一定是自動機A可以產(chǎn)生的,并且根據(jù)第9行、第10行、第19行的判斷條件,該符號化執(zhí)行片段的長度與區(qū)間[b,e]相交.

對于完備性,假設ω:(si,μ(si,σi+1,si+1))...(sj,μ(sj,σj+1,sj+1))是自動機A能夠產(chǎn)生的一條符號化路徑的一個片段,并且長度區(qū)間與約束區(qū)間[b,e]相交.那么,可以構造一個ω′∈Θ.首先,我們讓ω′從(si,μ(si,σi+1,si+1))開始,顯然,算法1中第3行可以辦到.由于ω是自動機A能夠產(chǎn)生的一條符號化路徑的一個片段,那么,ω中的第2個位置(si+1,μ(si+1,σi+2,si+2))一定是(si,μ(si,σi+1,si+1))的一個后繼,并且(si,μ(si,σi+1,si+1))(si+1,μ(si+1,σi+2,si+2))的時間長度的最大值一定小于e,那么,根據(jù)第 9行～第18行,ω′會等于(si,μ(si,σi+1,si+1))(si+1,μ(si+1,σi+2,si+2)).以此推導,直到(sj,μ(sj,σj+1,sj+1))被加到ω′的最后.那么,ω′會在執(zhí)行第10行、第11行或者執(zhí)行第19行、第20行后被加入到Θ中,即ω′∈Θ.

3 構造量詞線性算術表達式

本節(jié)我們介紹如何將一條滿足觀測時長約束的路徑片段轉化為一個量詞線性算術表達式.給定一個觀測區(qū)間[t,t′],那么它一定被自動機的狀態(tài)(位置)所占據(jù),如圖 3所示,在該段時間區(qū)間上,系統(tǒng)依次處于狀態(tài)(位置)l1,l2,…,ln(可以有重復狀態(tài),這里為了描述簡潔,重新給出下標號).如果區(qū)間長度t′-t在觀測區(qū)間長度約束[b,e]內,即b≤t′-t≤e,那么,其對應的路徑片段即為一條滿足觀測時長約束的路徑片段.

對于每一個位置li(1≤i≤n),我們引入一個變量δi∈?≥0,表示系統(tǒng)在該位置停留的時長.對于ELDI子式,如果含有模態(tài)詞切變,例如式子φ1;φ2;…;φr,那么,每一個切變點必然位于某個位置lj內.對于某個切變點chopi,我們引入一個變量τi∈?≥0.如圖3所示,如果切變點chopi位于位置lj內,那么,τi表示從系統(tǒng)進入位置lj到切變點chopi的時間長度.運用引入的這些變量,我們可以將一條滿足觀測時長約束的符號化路徑片段表達為(l1,δ1)(l2,δ2)…(ln,δn).下面我們給出將其轉化為一種量詞線性算術表達式的方法.

3.1 構造符號化路徑片段的時限約束

首先,我們需要將這條符號化路徑片段的時限約束表示出來,即刻畫實時自動機產(chǎn)生這條符號化路徑片段的所有時限約束.這些時限約束包括3種類型:非負約束、加和有界約束和δ約束.

定義 7(非負約束).給定一個滿足觀測時長約束[b,e]的路徑片段(l1,δ1)(l2,δ2)…(ln,δn),那么,系統(tǒng)在每個位置的停留時長δi是一個非負實數(shù):

定義 8(加和有界約束).給定一個滿足觀測時長約束[b,e]的路徑片段(l1,δ1)(l2,δ2)...(ln,δn),那么,系統(tǒng)在所有位置停留的總時長滿足觀測時長約束:

加和有界約束的意義在于,第 2節(jié)中求取的每個符號化路徑片段的時間長度均是一個區(qū)間,只是與時長約束[b,e]有交集.那么,加和有界約束則進一步限定,無論每個δi如何取值,加和一定需要滿足時長約束[b,e],去除掉路徑片段的時間長度在[b,e]約束之外時的δi取值情況.

定義 9(δ約束).給定一個滿足觀測時長約束[b,e]的路徑片段(l1,δ1)(l2,δ2)…(ln,δn),那么,系統(tǒng)在每個位置停留的時長δi應滿足實時自動機在相應位置停留的時限約束,即保證該路徑片段確實為一條實時自動機能夠產(chǎn)生的路徑的一個片段.

對于實時自動機,δ約束求取的基本思路如下,分兩種情況加以討論.

第2種情況,如果執(zhí)行片段長度大于1,假設路徑片段為(l1,δ1)(l2,δ2)…(ln,δn),那么,對于路徑片段中相鄰的兩個位置(li,δi)和(li+1,δi+1),先找到li到li+1的所有遷移,將遷移上的時限約束作為對于(li,δi)的δ約束.同樣地,對于(l1,δ1)的δ約束需要處理下界.

由于第2節(jié)查找滿足觀測時限的符號化執(zhí)行路徑時已采用該思想,因此具體實現(xiàn)時只需將第2節(jié)中對于該條符號化執(zhí)行路徑片段所求的每個位置時間長度區(qū)間變?yōu)橄鄳摩募s束.表2中算法為生成3種時限約束的算法.該算法輸入為某個符號化路徑片段ω:(l1,δ1)(l2,δ2)…(ln,δn),輸出為這個符號化路徑片段所滿足的時限約束Γ.該算法比較簡單,行2到行3是對每個位置生成其需要滿足的δ約束,運用函數(shù)δ_constraint()求取,具體方法如前所述.第4行將3種類型的約束取交集,即為時限約束Γ.

Table 2 The algorithm for generating the timing constraints表2 生成時限約束的算法

3.2 構造語義不等式

為了能夠用量詞線性算術表達式表達每一個線性時段子式D的語義信息,我們需要構造 3種不等式:線性時段子式不等式、τ～δ不等式以及τ附加不等式.

定義10(線性時段子式不等式).給定一個ELDI子式φ,對于其中每一個線性時段子式D,將D中每一個狀態(tài)(位置)積分∫li用引入的變量δ和τ表示,得到的不等式D′即為一個線性時段子式不等式.

定義11(τ～δ不等式).如果一個切變點chopi落在位置lj內,那么對應的變量τi和δj應滿足的不等關系為0≤τi≤δj,稱為一個τ～δ不等式.

定義 12(τ附加不等式).如果存在兩個相鄰的切變點chopi和chopi+1位于同一個位置lj內,如果chopi+1在chopi左邊,那么對應的變量τi和τi+1應滿足的不等關系為 0≤τi+1≤τi,稱為一個τ附加不等式.

給定一個符號化路徑片段ω:(l1,δ1)(l2,δ2)…(ln,δn)和 EDLI子式φ,將其翻譯為一組不等式的思路是,根據(jù)EDLI子式φ的邏輯結構,分解到每個線性時段子式,將其翻譯為線性時段子式不等式、τ～δ不等式、τ附加不等式;然后再用相應的邏輯結構組合起來.

· 當φ=?φ,φ1?φ2,φ1?φ2時,我們將它們遞歸分解為線性時段子式.

· 當φ=φ1;φ2時,將ω分為兩個子片段ω1和ω2,分別對應到公式φ1和φ2上,從而將其轉化為與關系(?)上的兩個子問題.

3.3 構造量詞線性算術表達式

與文獻[17]相比,本文構造的時限約束和不等式更加明確,同時,構造算法中不需要引入額外的δ變量,即在遇到切變時,通過已有δ變量和τ變量的算術運算形式來表示片段中被切割的位置分屬兩個子片段的時間長度(τ,δi-τ).由于求解量詞線性算術表達式的復雜度與變量個數(shù)相關,因此,本文采用的方法減少了變量個數(shù),有效地縮短了求解所需時間.具體算法參考表3中算法.

Table 3 The algorithm for generating a QLRA formula表3 生成一個QLRA公式的算法

表3中生成一種量詞線性算術表達式的算法,其輸入為一個擴展線性時段表達式φ和一個符號化路徑片段ω:(l1,δ1)(l2,δ2)…(ln,δn);輸出為一個 ELDI子式表達式ξ.整個算法是一種遞歸算法,根據(jù)擴展線性時段表達式φ的邏輯結構進行遞歸.當遞歸到某個線性時段子式時,運用引入的變量的加和形式替換掉式子中的狀態(tài)積分,得到線性時段子式不等式(行 3).當碰到邏輯連接詞時,根據(jù)邏輯連接詞的語義,將問題分解為子問題,遞歸地調用本算法.每當碰到一個切變時,引入一個變量τ,將ω分為兩部分(行11),同時需要添加相應的τ～δ不等式(行11中最后一個不等式).當遇到兩個切變點落在同一個狀態(tài)時,τ～δ不等式會變成一個τ附加不等式.例如,當φ1仍然含有切變,且切變點落在ω1:(l1,δ1)…(li,τ)的最后一個位置時,新引入的變量τ′需要滿足的τ～δ不等式為 0≤τ′≤τ,那么,實際上是一個τ附加不等式.當片段有n個位置時,當前切變點的落位會有n+2種情況,即在這n個位置之前、在這n個位置中的某個、在這n個位置之后.集合Q記錄引入的(多個)τ變量.最后,我們將引入的δ變量、算法2求出的時限約束表達式Γ和得到的表達式ξ構造一個QLRA表達式π=?δ1,…,δn,Q.Γ?ξ.

3.4 構造算法的正確性證明

同樣地,我們需要證明構造算法的正確性,正確性證明主要依賴遞歸正確性.

定理2(算法3的正確性).給定一個滿足觀測時長約束[b,e]的符號化路徑片段ω和ELDI公式φ,算法3是正確的,即:

· 終止性:算法會終止;

· 可靠性:如果ω?,φ那么,QLRA(φ,ω)得到的QLRA表達式是滿足的(satisfiable);

· 完備性:如果QLRA(φ,ω)得到的QLRA表達式是滿足的,則ω?.φ

證明:對于終止性來說,由于算法是根據(jù) ELDI公式φ的結構進行遞歸的,因此可以看出算法是終止的.對于可靠性和完備性,下面分析每種遞歸結構.

· 當φ是一個線性時段子式,即φ=D =∑i∈Ωci∫Si≤c時,Iω,[t1,t2]?b≤?≤e?∑i∈Ωci∫Si≤c當且僅當b≤t2-t1≤e?∑i∈Ωci Iω(∫Si)([t1,t2])≤c,其中,t1,t2分別為路徑片段的起始時刻和終止時刻.顯然,當按照語義替換后,仍然有這一關系.因此,如果ω?φ,那么,QLRA(φ,ω)得到的QLRA表達式是滿足的;如果QLRA(φ,ω)得到的QLRA表達式是滿足的,則ω?φ.

· 當φ=?φ1時,對于可靠性,假設QLRA(?φ,ω)不滿足,那么,根據(jù)算法 3 有?QLRA(φ1,ω)不滿足,也就意味著QLRA(φ1,ω)正確.根據(jù)歸納假設條件,我們有ω?φ,可以得到ω不滿足?φ1.對于完備性,假設QLRA(?φ1,ω)正確,根據(jù)算法 3有QLRA(φ1,ω)不滿足.根據(jù)歸納假設,我們有ω不滿足?φ1,因此得到ω?φ.

· 當φ=φ1?φ2時,對于可靠性,假設QLRA(φ1?φ2,ω)不滿足,根據(jù)算法 3 有QLRA(φ1,ω)?QLRA(φ2,ω)不滿足.根據(jù)歸納假設,我們有ω不滿足φ1并且ω不滿足φ2,因此,ω不滿足φ1?φ2.對于完備性,假設QLRA(φ1?φ2,ω)正確,根據(jù)算法3有?QLRA(φ1,ω)或者?QLRA(φ2,ω)不滿足.根據(jù)歸納假設,我們有ω不滿足φ1或者ω不滿足φ2,因此得到ω?φ1?φ2.

· 當φ=φ1?φ2時,證明與φ=φ1?φ2類似.

· 當φ=φ1;φ2時,顯然ω?φ1;φ2當且僅當ω被分為兩個部分ω1和ω2且ω1?φ1?ω2?φ2.根據(jù)算法3,我們選取了所有可能的切變點位置,并按語義分解為兩個子問題ω1?φ1和ω2?φ2.因此,根據(jù)歸納假設,我們得出:如果ω?φ1;φ2,那么,QLRA(φ1;φ2,ω)得到的 QLRA 表達式是滿足的;如果QLRA(φ1;φ2,ω)得到的 QLRA 表達式是滿足的,則ω?φ1;φ2.

3.5 構建量詞線性算術表達式舉例

下面舉例說明如何構建一個量詞線性算術表達式.

例2:我們考慮圖1所示的實時自動機以及ELDI公式:3≤?≤4?∫s0+∫s1≤1;2∫s1-∫s2≤2,令D1=∫s0+∫s1≤1,D2=2∫s1-∫s2≤2.現(xiàn)有一條滿足觀測時長約束的符號化路徑片段ω:(s0,δ0)(s1,δ1)(s2,δ2),可見我們引入了3個δ變量.由于有一個切變,因此我們引入一個τ變量τ1.

首先,我們生成符號化路徑片段的所有時限約束.對于δ約束,由于(s0,δ0)是第 1個位置,后繼位置為(s1,δ1),因此,δ0應先取遷移(s0,a,s1)的時限約束,即 1≤δ0≤2.由于(s0,δ0)是第 1個位置,開始觀測時并不知道系統(tǒng)在s0已停留多長時間,因此,將δ0的下界改為0,得到δ0的最后約束為0≤δ0≤2.用同樣的方法得到(s1,δ1)的時限約束為2≤δ1≤4,(s2,δ2)的時限約束為δ2≥0.非負約束為(δ0≥0?δ1≥0?δ2≥0),加和有界約束為3≤δ0+δ1+δ2≤4.所有時限約束為3≤δ0+δ1+δ2≤4?(0≤δ0≤2?2≤δ1≤4?δ2≥0)?(δ0≥0?δ1≥0?δ2≥0).

然后,我們根據(jù)算法3來構造不等式和QLRA表達式.由于當前ELDI公式中是一個切變形式,那么會匹配到第 11 行,并有 5 種可能情況:(1) 當切變點落在s0左側時,ω1為空,ω2為(s0,δ0)(s1,δ1)(s2,δ2),那么,D1=0+0≤1,D2=2δ1-δ2≤2,即得到線性時段子式的不等式0+0≤1?2δ1-δ2≤2.(2) 當切變點落在s0時,ω1為(s0,τ1),ω2為(s0,δ0-τ1)(s1,δ1)(s2,δ2),那么,D1=τ1+0≤1,D2=2δ1-δ2≤2,即得到線性時段子式的不等式τ1+0≤1?2δ1-δ2≤2?0≤τ1≤δ0.(3) 當切變點落在s1時,ω1為(s0,δ0)(s1-τ1),ω2為(s1,δ1-τ1)(s2,δ2),那么,D1=δ0+τ1≤1,D2=2(δ1-τ1)-δ2≤2,即得到線性時段子式的不等式δ0+τ1≤1?2(δ1-τ1)-δ2≤2?0≤τ1≤δ1.(4) 當切變點落在s2時,用同樣的方法得到線性時段子式的不等式為δ0+δ1≤1?0-(δ2-τ1)≤2?0≤τ1≤δ2.(5) 當切變點落在s2的右側時,用上述方法得到線性時段子式的不等式為δ0+δ1≤1?0-0≤2.因此,根據(jù)算法3構造的QLRA表達式為

π=?δ0,?δ1,?δ2,?τ1.3≤δ0+δ1+δ2≤4?(0≤δ0≤2?2≤δ1≤4?δ2≥0)?(δ0≥0?δ1≥0?δ2≥0)?(0+0≤1?2δ1-δ2≤2)?(τ1+0≤1?2δ1-δ2≤2?0≤τ1≤δ0)?(δ0+τ1≤1?2(δ1-τ1)-δ2≤2?0≤τ1≤δ1)?(δ0+δ1≤1?0-(δ2-τ1)≤2?0≤τ1≤δ2)?(δ0+δ1≤1?0-0≤2).

4 求解QLRA表達式及判定定理

根據(jù)定理1和定理2,給定一個實時自動機A和一個觀測時長約束有上界的ELDI公式Φ,我們可以將模型檢驗問題A?Φ轉化為QLRA表達式的正確性(validity)問題.

定理 3.給定一個實時自動機A和一個觀測時長約束有上界的 ELDI公式Φ,A?Φ當且僅當∩ω∈Search（A,［b,e］）QLRA(Φ,ω)是正確的(valid).

定理3可以從定理1和定理2得出,這里不再證明.根據(jù)Tarski理論,量詞線性算術表達式的可滿足性和正確性問題是可以判定的[20],因此有下面的結論.

定理4.給定一個實時自動機A和一個觀測時長約束有上界的ELDI公式Φ,A,[b,e]?Φ是可判定的.

QLRA表示式可以運用量詞消去技術求解,量詞消去技術基于柱形代數(shù)分解理論(cylindrical algebraic decomposition,簡稱CAD)[21],該方法的最壞復雜度與變量規(guī)模呈二階指數(shù)關系,但是,由于QLRA表達式中均為線性不等式,因此,求解比較迅速.目前,量詞消去技術在許多求解器中都有實現(xiàn),例如,REDLOG、QEPCAD[22]、Z3等.

5 工具實現(xiàn)與實驗

目前,我們在Linux平臺上實現(xiàn)了一個原型工具,如圖4所示為工具的架構圖.工具接收兩個輸入:一是,實時自動機(A)模型文件,格式參考 UPPAAL模型文件格式;二是,擴展線性時段不變式(φ),存放在一個文本文件中.工具會接收這兩個輸入,首先尋找所有滿足觀測時長約束?的符號化路徑片段,并得到其集合Θ,然后構造QLRA表達式,生成所有QLRA表達式的集合∏,并保存在符合REDLOG輸入格式的文本文件中;然后將該文件傳遞給量詞消去工具REDLOG,REDLOG會依次求解QLRA表達式πi,并將每個表達式的結果(true or false)記錄在一個文本文件中.

在實驗部分,我們討論文獻[14,16]中給出的一個實驗.一個實時自動機A由N個簡單的實時自動機M迭代組成.Mi如圖5所示,由4個狀態(tài)組成Ai,Bi,Ci,Di,系統(tǒng)在每個狀態(tài)上停留一個時間單位.特別地,對于1≤i≤N,Di有一條遷移前往Ai+1;對于 1≤j≤i≤N,Di有一條遷移前往Aj.文獻[14,16]在離散時間語義下進行了實驗,本文則在標準連續(xù)時間語義下進行了實驗,迭代次數(shù)N從3到6.表4是我們的實驗結果,tqlra表示生成所有QLRA表達式所用時間,tqe表示運用量詞消去工具求解所有 QLRA表達式所用時間,ttotal表示驗證的總時間,而t′total表示采用文獻[17]中算法的總時間,時間單位均為s.我們同樣對含有不同邏輯運算符和切變的ELDI式子進行了實驗,工具和實驗可以參考https://github.com/Leslieaj/VCELDI.

由于本文采用標準連續(xù)時間語義,而文獻[16]采用離散時間語義,所以模型檢驗的總時間比文獻[16]中相同問題所用時間要長.這是由于采用方法、基于的模型以及討論的時間語義不同所致,我們的優(yōu)勢是可以解決連續(xù)時間語義下的模型檢驗問題.與文獻[17]中算法的實驗結果相比,我們的驗證方法所用時間明顯低于文獻[17]驗證所需時間,可見本文方法有效地降低了驗證算法的復雜度,提高了實際驗證速度.

Table 4 The results of the experiment表4 實驗結果

6 總 結

本文討論了在連續(xù)時間語義下,對于一個觀測時長約束有上界的擴展線性時段不變式(ELDI)在實時自動機上的模型檢驗問題.本文證明了該問題是可以判定的,并且給出了判定方法.首先,我們采用符號化的思想,運用深度優(yōu)先搜索得到所有滿足觀測時長約束的符號化路徑片段;然后,將每一個符號化路徑片段轉化為一個量詞線性算術表達式;最后,運用量詞消去工具REDLOG求解這些量詞線性算術表達式.

時間復雜度方面,對于第1步,我們可以看到算法1與自動機中狀態(tài)(位置)數(shù)目呈一階指數(shù)關系.第2步中,生成 QLRA表達式的算法復雜度是多項式復雜度.最后一步運用量詞消去工具求解,量詞消去工具的最壞時間復雜度與變量個數(shù)呈二階指數(shù)關系.但是,根據(jù)前文分析,QLRA 表示式中均為線性不等式,所以求解比較快,近似為多項式和一階指數(shù),這一點可以從實驗tqlar和tqe的比較中看出.所以,對于時間復雜度來說,與實時自動機的規(guī)模和擴展線性時段不變式的切變個數(shù)呈一階指數(shù)關系,最壞是二階指數(shù)關系.而文獻[17]中的驗證算法復雜度一般為二階指數(shù),最壞情況為三階指數(shù).與文獻[17]相比,復雜度和運行速度方面的優(yōu)化有以下兩點:第一,縮短了搜索空間,降低了搜索算法的復雜度,并減少了所產(chǎn)生的QLRA公式數(shù)量;第二,對于單個QLRA表達式,減少了量詞的引入個數(shù).從而,整體上降低了驗證算法的復雜度,并加快了量詞消去工具求解時的實際運行速度.