安 杰, 張苗苗

(同濟(jì)大學(xué) 軟件學(xué)院,上海 201804)

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

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

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

本文驗(yàn)證方法的基本思路如下.

· 第 1步,運(yùn)用符號(hào)化的思想,在實(shí)時(shí)自動(dòng)機(jī)上利用深度優(yōu)先搜索找到所有滿足觀測(cè)時(shí)長(zhǎng)約束的符號(hào)化路徑片段;

· 第2步,將每條路徑轉(zhuǎn)化為一個(gè)量詞線性算術(shù)表達(dá)式(quantified linear real arithmetic,簡(jiǎn)稱QLRA);

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

在第1步中,我們定義了符號(hào)化路徑片段,給出了相應(yīng)的求取方法,并且有效地縮小了搜索空間.在第2步中,我們?cè)敿?xì)定義并構(gòu)造了組成量詞線性算術(shù)表達(dá)式的不等式約束,并且采用一些方法減少量詞的引入個(gè)數(shù).由于量詞消去的復(fù)雜度與量詞個(gè)數(shù)相關(guān),因此第2步的處理也加快了第3步量詞消去的實(shí)際運(yùn)行速度.

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

1 基礎(chǔ)知識(shí)及相關(guān)定義

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

1.1 實(shí)時(shí)自動(dòng)機(jī)

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

定義1(實(shí)時(shí)自動(dòng)機(jī)).一個(gè)實(shí)時(shí)自動(dòng)機(jī)RTA是一個(gè)6元組A=(S,Σ,Δ,s0,F,μ),其中,

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

·∑是一個(gè)有窮字母表;

· Δ?S×∑×S是遷移關(guān)系;

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

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

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

例1:如圖1所示為一個(gè)實(shí)時(shí)自動(dòng)機(jī)A,對(duì)于其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)},對(duì)應(yīng)的時(shí)間標(biāo)簽函數(shù)產(chǎn)生的時(shí)間標(biāo)簽為μ(Δ)={[1,2],[1,3],[2,4]}.

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

1.2 擴(kuò)展線性時(shí)段不變式

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

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

定義2(擴(kuò)展線性時(shí)段不變式).擴(kuò)展線性時(shí)段不變式的結(jié)構(gòu)定義如下.

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

特別地,本文中我們只關(guān)注觀測(cè)時(shí)長(zhǎng)上界e有界的情形,本文所指的有界模型檢驗(yàn)指的也是此種情形.

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

如圖2所示.

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

· 對(duì)于狀態(tài)表達(dá)式:給定一個(gè)時(shí)刻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)}.

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

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

1.3 量詞線性算術(shù)

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

定義4(量詞線性算術(shù)表達(dá)式語(yǔ)法)

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

2 尋找滿足觀測(cè)時(shí)長(zhǎng)約束的路徑片段.

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

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

2.1 符號(hào)化路徑片段的定義

下面對(duì)符號(hào)化路徑片段及其時(shí)間長(zhǎng)度給出顯性刻畫.

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

2.2 符號(hào)化路徑片段的搜索算法

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

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

Table 1 The algorithm for finding all symbolic path segments whose lengths are in [b,e]表1 尋找所有滿足觀測(cè)時(shí)長(zhǎng)約束[b,e]的符號(hào)化路徑片段的算法

2.3 搜索算法的正確性證明

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

定理1(算法1正確性).給定一個(gè)實(shí)時(shí)自動(dòng)機(jī)A和觀測(cè)時(shí)長(zhǎng)約束[b,e],算法1是正確的,即:

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

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

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

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

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

3 構(gòu)造量詞線性算術(shù)表達(dá)式

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

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

3.1 構(gòu)造符號(hào)化路徑片段的時(shí)限約束

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

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

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

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

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

對(duì)于實(shí)時(shí)自動(dòng)機(jī),δ約束求取的基本思路如下,分兩種情況加以討論.

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

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

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

3.2 構(gòu)造語(yǔ)義不等式

為了能夠用量詞線性算術(shù)表達(dá)式表達(dá)每一個(gè)線性時(shí)段子式D的語(yǔ)義信息,我們需要構(gòu)造 3種不等式:線性時(shí)段子式不等式、τ～δ不等式以及τ附加不等式.

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

定義11(τ～δ不等式).如果一個(gè)切變點(diǎn)chopi落在位置lj內(nèi),那么對(duì)應(yīng)的變量τi和δj應(yīng)滿足的不等關(guān)系為0≤τi≤δj,稱為一個(gè)τ～δ不等式.

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

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

· 當(dāng)φ=?φ,φ1?φ2,φ1?φ2時(shí),我們將它們遞歸分解為線性時(shí)段子式.

· 當(dāng)φ=φ1;φ2時(shí),將ω分為兩個(gè)子片段ω1和ω2,分別對(duì)應(yīng)到公式φ1和φ2上,從而將其轉(zhuǎn)化為與關(guān)系(?)上的兩個(gè)子問題.

3.3 構(gòu)造量詞線性算術(shù)表達(dá)式

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

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

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

3.4 構(gòu)造算法的正確性證明

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

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

· 終止性:算法會(huì)終止;

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

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

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

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

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

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

· 當(dāng)φ=φ1?φ2時(shí),證明與φ=φ1?φ2類似.

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

3.5 構(gòu)建量詞線性算術(shù)表達(dá)式舉例

下面舉例說明如何構(gòu)建一個(gè)量詞線性算術(shù)表達(dá)式.

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

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

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

π=?δ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表達(dá)式及判定定理

根據(jù)定理1和定理2,給定一個(gè)實(shí)時(shí)自動(dòng)機(jī)A和一個(gè)觀測(cè)時(shí)長(zhǎng)約束有上界的ELDI公式Φ,我們可以將模型檢驗(yàn)問題A?Φ轉(zhuǎn)化為QLRA表達(dá)式的正確性(validity)問題.

定理 3.給定一個(gè)實(shí)時(shí)自動(dòng)機(jī)A和一個(gè)觀測(cè)時(shí)長(zhǎng)約束有上界的 ELDI公式Φ,A?Φ當(dāng)且僅當(dāng)∩ω∈Search（A,［b,e］）QLRA(Φ,ω)是正確的(valid).

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

定理4.給定一個(gè)實(shí)時(shí)自動(dòng)機(jī)A和一個(gè)觀測(cè)時(shí)長(zhǎng)約束有上界的ELDI公式Φ,A,[b,e]?Φ是可判定的.

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

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

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

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

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

Table 4 The results of the experiment表4 實(shí)驗(yàn)結(jié)果

6 總 結(jié)

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

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