時(shí)序邏輯及其表達(dá)能力綜述

楊 科，肖美華，鐘小妹，占東明，2

（1.華東交通大學(xué)軟件學(xué)院，江西 南昌 330013；2.華中師范大學(xué)教育學(xué)院，湖北 武漢 430079）

時(shí)序邏輯來(lái)源于哲學(xué)和語(yǔ)言學(xué)，由模態(tài)邏輯演變而來(lái)，是一種特殊模態(tài)邏輯。時(shí)序邏輯將時(shí)間因素引入到模態(tài)邏輯中，將模態(tài)算子□(必然)解釋為“將來(lái)永遠(yuǎn)”,◇(可能)解釋為“將來(lái)會(huì)”，它是由Prior于1955 年首先提出的，以研究時(shí)間和時(shí)序的邏輯[1]。在過(guò)去幾十年里，許多邏輯學(xué)家和計(jì)算機(jī)科學(xué)家對(duì)其進(jìn)行研究和擴(kuò)充，衍生出各種不同的時(shí)序邏輯，被廣泛應(yīng)用于數(shù)學(xué)、計(jì)算機(jī)科學(xué)以及人工智能等領(lǐng)域。

早期的形式化方法（20 世紀(jì)70 年代前）致力于研究經(jīng)典一階邏輯、Hoare 邏輯在串行程序上的描述與驗(yàn)證，該類方法是以邏輯推理為基礎(chǔ)的演繹證明。從20 世紀(jì)70 年代中期開(kāi)始，并發(fā)程序設(shè)計(jì)成為理論計(jì)算機(jī)科學(xué)中的研究熱點(diǎn)。不同于串行程序，并發(fā)程序涉及到不同任務(wù)之間的同步以及信息交換，可能會(huì)造成數(shù)據(jù)競(jìng)爭(zhēng)、死鎖、原子性違反等錯(cuò)誤[2]，在串行程序分析方法的基礎(chǔ)上擴(kuò)充并發(fā)性的推理規(guī)則對(duì)于并發(fā)程序的分析驗(yàn)證并不適用。由于連續(xù)運(yùn)行的系統(tǒng)必然會(huì)涉及到時(shí)間概念，然而命題邏輯缺乏描述包含連續(xù)系統(tǒng)中與時(shí)間相關(guān)概念的能力。因此以色列科學(xué)家伯努利在1977 年提出將時(shí)序邏輯作為并發(fā)系統(tǒng)的規(guī)格說(shuō)明工具，基于時(shí)序邏輯對(duì)并發(fā)程序性質(zhì)進(jìn)行形式化規(guī)約和驗(yàn)證。20 世紀(jì)80 年代，隨著超大規(guī)模集成電路、并發(fā)分布式系統(tǒng)等技術(shù)的迅猛發(fā)展，鑒于演繹驗(yàn)證的局限性，對(duì)自動(dòng)化驗(yàn)證技術(shù)提出了更高的要求。美國(guó)的Clarke和Emerson，法國(guó)的Sifakis 和Queille 在1981 年分別獨(dú)立提出將時(shí)序邏輯與狀態(tài)空間搜索相結(jié)合的方法，誕生了模型檢測(cè)技術(shù)[3]。隨著模型檢測(cè)技術(shù)的發(fā)展，時(shí)序邏輯被廣泛應(yīng)用在系統(tǒng)形式化規(guī)約與驗(yàn)證中，尤其是上世紀(jì)90 年代符號(hào)模型檢測(cè)技術(shù)的出現(xiàn)，利用二叉決策圖的方式來(lái)表示模型的狀態(tài)遷移關(guān)系，使得可驗(yàn)證的系統(tǒng)狀態(tài)數(shù)多達(dá)10200，成功應(yīng)用于超大規(guī)模集成電路和大型軟件系統(tǒng)的驗(yàn)證中。時(shí)序邏輯作為一種描述與驗(yàn)證計(jì)算機(jī)系統(tǒng)的形式化規(guī)約語(yǔ)言，被廣泛應(yīng)用于各類系統(tǒng)的形式化驗(yàn)證。經(jīng)過(guò)40 多年的發(fā)展，時(shí)序邏輯已經(jīng)發(fā)展成為包括線性時(shí)序邏輯、計(jì)算樹(shù)邏輯和區(qū)間時(shí)序邏輯等眾多分支的一門學(xué)科。特別是在計(jì)算機(jī)科學(xué)中，時(shí)序邏輯作為形式規(guī)約語(yǔ)言，已經(jīng)成為形式化驗(yàn)證程序和并發(fā)系統(tǒng)的重要組成部分。

對(duì)于一種時(shí)序邏輯來(lái)說(shuō)，一般從可滿足性、復(fù)雜性、表達(dá)性3 個(gè)方面展開(kāi)研究[4]?？蓾M足性就是給定一個(gè)性質(zhì)規(guī)約公式φ，是否存在一個(gè)結(jié)構(gòu)M，該結(jié)構(gòu)恰好是給定公式φ 的模型，或者判定模型M 是否滿足公式φ；復(fù)雜性就是研究邏輯公式可滿足性的復(fù)雜度問(wèn)題；表達(dá)性是研究時(shí)序邏輯的表達(dá)能力，該邏輯公式能夠描述哪一種類型的性質(zhì)。本文著重研究時(shí)序邏輯的表達(dá)能力問(wèn)題，介紹各種時(shí)序邏輯和分析它們適合對(duì)哪些系統(tǒng)進(jìn)行性質(zhì)規(guī)約，以及不同時(shí)序邏輯在表達(dá)能力上的優(yōu)劣。

1 時(shí)序邏輯

時(shí)序邏輯主要研究狀態(tài)隨時(shí)間變化系統(tǒng)的邏輯特性，由于硬件和軟件的運(yùn)行都是隨著時(shí)間的變化而不斷變化，因此時(shí)序邏輯特別適合對(duì)該類系統(tǒng)模型進(jìn)行形式化規(guī)約，廣泛應(yīng)用在程序驗(yàn)證和硬件驗(yàn)證領(lǐng)域。在對(duì)系統(tǒng)形式化驗(yàn)證時(shí)，人們通常關(guān)心這兩種性質(zhì)：安全性（safety）和活性（liveness）[5]。它們分別表示“壞的事情永遠(yuǎn)不會(huì)發(fā)生”和“好的事情最終會(huì)發(fā)生”。系統(tǒng)的特性用時(shí)序邏輯來(lái)表示，比如系統(tǒng)是否會(huì)發(fā)生死鎖、程序代碼是否會(huì)陷入死循環(huán)和系統(tǒng)能否在規(guī)定時(shí)間內(nèi)對(duì)輸入信號(hào)做出正確響應(yīng)等。

下面簡(jiǎn)要介紹時(shí)序邏輯屬性、屬性的可描述性以及表達(dá)能力[6]的形式化定義。

定義1 （屬性）在一個(gè)無(wú)窮狀態(tài)序列δ：δ0，δ1，δ2，…（δ∈Sω）的集合Sω上定義屬性p（property，也稱之為性質(zhì)）。一個(gè)屬性p?Sω是所有滿足該屬性的無(wú)窮狀態(tài)序列δ 的集合，也就是說(shuō)一個(gè)無(wú)窮狀態(tài)序列δ 滿足屬性p 等價(jià)于該序列δ 屬于p 所表示的集合，記作δ｜=p?δ∈p。

定義2 （屬性p 的可描述性）設(shè)φ 是一個(gè)時(shí)序邏輯公式，如果δ∈p iff δ｜=φ 成立，那么屬性p 能夠用時(shí)序邏輯公式φ 來(lái)描述。

定義3 （表達(dá)能力）在一類模型M 下，語(yǔ)言L2至少具有和語(yǔ)言L1同等的表達(dá)能力，記作L1?ML2。有如下公式成立：

?φ1∈L1，?φ2∈L2，?M∈M，M｜=φ1iff M｜=φ2

如果有L1?ML2和L2?ML1成立，我們稱在模型M 上語(yǔ)言L1和L2表達(dá)能力相同，記作L1≡ML2。如果有L1?ML2成立而L1≡ML2不成立，稱在模型M 上語(yǔ)言L2的表達(dá)能力比L1更強(qiáng)，記作L1?ML2。

2 基于離散時(shí)間模型的時(shí)序邏輯

本節(jié)介紹基于離散時(shí)間模型的時(shí)序邏輯，它們的語(yǔ)義被解釋在孤立離散的點(diǎn)上，主要包括LTL，CTL 和CTL*，并對(duì)它們之間的區(qū)別進(jìn)行詳細(xì)分析比較。

2.1 線性時(shí)序邏輯LTL

LTL 由Manna 和Pnueli 提出，是一種非常重要的時(shí)序邏輯，可以用來(lái)描述并發(fā)分布式系統(tǒng)的屬性，在模型檢測(cè)中得到廣泛使用。LTL 將時(shí)間序列設(shè)想成一個(gè)線性序列δ：s0，s1，s2，…，這是一種經(jīng)典的時(shí)間模型。狀態(tài)之間按照時(shí)間參數(shù)嚴(yán)格排序，在狀態(tài)序列上解釋其真值，并且其真值隨時(shí)間變化而變化，這也是時(shí)序邏輯與經(jīng)典邏輯的主要區(qū)別之處。

LTL 采用的時(shí)間結(jié)構(gòu)是線性、離散的，其語(yǔ)義模型是通過(guò)Kripke 三元組ML=＜S，R，L＞來(lái)定義的，其中S 是狀態(tài)集合，R?S×S 是符合完全性約束的變遷關(guān)系（即對(duì)于任意的狀態(tài)s∈S，存在狀態(tài)s'∈S滿足（s，s'）∈R，L∶S→2AP是標(biāo)記函數(shù)，用于標(biāo)記某個(gè)狀態(tài)上所有滿足的原子命題集合。

以選舉算法為例，對(duì)如何使用LTL 描述領(lǐng)導(dǎo)人選舉算法需要滿足的性質(zhì)進(jìn)行闡述。領(lǐng)導(dǎo)人選舉算法是分布系統(tǒng)中一類非常重要的算法，目的是在多個(gè)服務(wù)器中選出一個(gè)特殊的節(jié)點(diǎn)作為領(lǐng)導(dǎo)人，可以簡(jiǎn)化服務(wù)器之間的協(xié)作，有助于容錯(cuò)和節(jié)省資源。我們用elected 表示選舉發(fā)生，num_leader 表示領(lǐng)導(dǎo)人數(shù)量，one_leader 表示成功選舉出領(lǐng)導(dǎo)人。

性質(zhì)1：選舉結(jié)束后，最終會(huì)選出一位領(lǐng)導(dǎo)人：◇（num_leader＞0）。

性質(zhì)2：選舉結(jié)束后，至多有一位領(lǐng)導(dǎo)人當(dāng)選：□?（num_leader＞1）。

性質(zhì)3：當(dāng)某個(gè)節(jié)點(diǎn)被選為領(lǐng)導(dǎo)人之后，將永遠(yuǎn)成為領(lǐng)導(dǎo)人：∧i□（electedi→one_leader）。

定理1 LTL 的表達(dá)能力與一階謂詞邏輯等價(jià)，不能表達(dá)ω 正則性質(zhì)[7]。

該定理表明雖然LTL 與一階謂詞邏輯的表達(dá)能力等價(jià)，但對(duì)于兩者的可滿足性的復(fù)雜度卻不相同。對(duì)于一階謂詞邏輯來(lái)說(shuō)，它的可滿足性問(wèn)題的解決難度是非初等的，也就是說(shuō)它的復(fù)雜度上界是無(wú)限增長(zhǎng)的，而對(duì)于LTL 來(lái)說(shuō)是PSPACE-完全的[8]，這也是LTL 能夠得到廣泛應(yīng)用于程序驗(yàn)證、程序綜合以及人工智能等領(lǐng)域的一個(gè)重要理論支撐[9]。

在顯式模型檢測(cè)中，通常是將軟硬件系統(tǒng)用形式化語(yǔ)言建模成模型M，同時(shí)利用LTL 公式將系統(tǒng)的屬性表示為φ，其核心是判斷系統(tǒng)模型的自動(dòng)機(jī)AM與時(shí)序邏輯公式φ取反得到的等價(jià)自動(dòng)機(jī)Aφ做交運(yùn)算后的自動(dòng)機(jī)AP是否為空?？梢酝茢喑鯨TL是可以用自動(dòng)機(jī)來(lái)表示的，但研究表明LTL 與自動(dòng)機(jī)之間的轉(zhuǎn)換并不是雙向的，LTL 的表達(dá)能力弱于自動(dòng)機(jī)[10]。

雖然LTL 具有容易理解、表達(dá)能力較強(qiáng)的優(yōu)點(diǎn)，但它的缺點(diǎn)是不能表達(dá)ω-正則性質(zhì)，具備完整的ω-正則語(yǔ)言表達(dá)能力對(duì)于性質(zhì)規(guī)約語(yǔ)言來(lái)說(shuō)是十分重要的，尤其是對(duì)于無(wú)限狀態(tài)系統(tǒng)的形式化驗(yàn)證。因此一些研究對(duì)LTL 進(jìn)行擴(kuò)充，使得擴(kuò)展得到的時(shí)序邏輯表達(dá)能力等價(jià)于ω-正則語(yǔ)言[11]。一種方法是將時(shí)序邏輯構(gòu)筑于二階量詞或不動(dòng)點(diǎn)算子，如Kozen[12]提出了μ 演算，μ 演算在時(shí)間模型的基礎(chǔ)上加入了不動(dòng)點(diǎn)算子。通過(guò)引入不動(dòng)點(diǎn)算子使得μ 演算表達(dá)性增強(qiáng)，然而付出的代價(jià)是其可滿足性的判定問(wèn)題變得復(fù)雜，而且不動(dòng)點(diǎn)算子的嵌套使用令公式難以理解。另外一種方法則是在時(shí)序邏輯基礎(chǔ)上添加時(shí)序算子或者正則表達(dá)式，如Wolper[13]提出了ETL，通過(guò)在LTL 中加入正則表達(dá)式使其表達(dá)能力等價(jià)于自動(dòng)機(jī)。

2.2 計(jì)算樹(shù)邏輯CTL

CTL[14]的語(yǔ)義模型與LTL 類似，都是通過(guò)Kripke 結(jié)構(gòu)來(lái)定義的。不同的是，由狀態(tài)組成的序列∏∶s0，s1，s2，…，sk，…的路徑中，從模型的初始狀態(tài)作為根節(jié)點(diǎn)，對(duì)于k≥0，都有（sk，sk+1）∈R，模型的未來(lái)時(shí)刻存在著多種不確定狀態(tài)。因此，把所有路徑展開(kāi)就形成了樹(shù)狀的拓?fù)浣Y(jié)構(gòu)，這也是被稱為計(jì)算樹(shù)的原因，又因?yàn)槊總€(gè)節(jié)點(diǎn)存在分支，所以CTL 也被稱之為分支時(shí)序邏輯（branching temporal logic，BTL）。

CTL 的語(yǔ)義模型是通過(guò)Kripke 三元組M=＜S，R，L＞來(lái)定義的，其中S 是狀態(tài)集合，R?S×S 是符合完全性約束的變遷關(guān)系（即對(duì)于任意的狀態(tài)s∈S,存在狀態(tài)s'∈S 滿足 （s，s'）∈R），L∶S→2AP是標(biāo)記函數(shù)，用于標(biāo)記某個(gè)狀態(tài)上所有滿足的原子命題集合。

為了更好地介紹如何使用CTL 描述相關(guān)性質(zhì)，以多個(gè)進(jìn)程訪問(wèn)共享內(nèi)存為例進(jìn)行說(shuō)明。假設(shè)有兩個(gè)獨(dú)立進(jìn)程proc1和proc2訪問(wèn)同一片共享內(nèi)存，并且要避免它們同時(shí)訪問(wèn)，一旦兩個(gè)進(jìn)程同時(shí)訪問(wèn)臨界區(qū)，那么就會(huì)造成程序崩潰。“entering”狀態(tài)表示當(dāng)前某個(gè)進(jìn)程請(qǐng)求訪問(wèn)共享內(nèi)存，“critical”狀態(tài)表示當(dāng)前有某個(gè)進(jìn)程正在訪問(wèn)共享內(nèi)存。

性質(zhì)4：兩個(gè)進(jìn)程不能同時(shí)訪問(wèn)共享內(nèi)存，即兩個(gè)進(jìn)程間存在互斥性（mutual exclusion）。

2.3 計(jì)算樹(shù)邏輯CTL*

針對(duì)LTL 與CTL 在在處理計(jì)算分支上的不同，Clarke 對(duì)CTL 的語(yǔ)法和語(yǔ)義作適當(dāng)?shù)臄U(kuò)充，設(shè)計(jì)了兼容上述兩種時(shí)序邏輯算子的語(yǔ)言CTL*[15]，該語(yǔ)言融合兩種時(shí)序邏輯于一種語(yǔ)言之中，同時(shí)還克服了時(shí)序邏輯公式的二義性解釋（時(shí)序邏輯公式既可以解釋成線性的，也可以解釋成分支的）。

CTL*的語(yǔ)義與CTL 類似，因此不做過(guò)多介紹。LTL 和CTL 存在交集，這部分性質(zhì)既可以用LTL 公式表示，也可以用CTL 公式來(lái)表示。存在只能用LTL 公式表示的性質(zhì)（如A（FGp））卻不存在著相應(yīng)的CTL 公式，也存在只能用CTL 公式表示的性質(zhì)（如AG（EFp））卻不存在著相應(yīng)的LTL 公式。這兩種性質(zhì)的結(jié)合體A（FGp∨AG（EFp）既不能用LTL 表示，也不能用CTL 表示，只能用這兩種時(shí)序邏輯的超集CTL*表示。隨著CTL*表達(dá)能力的增強(qiáng)，CTL*模型檢測(cè)的復(fù)雜度隨之提高，CTL*的模型檢測(cè)問(wèn)題是PSPACE-完全的。隨著待驗(yàn)證系統(tǒng)規(guī)模狀態(tài)增加，CTL* 模型檢測(cè)中的狀態(tài)爆炸問(wèn)題更加突出，在實(shí)際驗(yàn)證中會(huì)根據(jù)具體情況犧牲部分表達(dá)能力而選擇復(fù)雜度較小的LTL 公式或CTL 公式。在表達(dá)能力上LTL 公式可以方便地描述路徑范圍的選擇，但在路徑量詞方面有所缺失，CTL 公式可以精細(xì)地描述某個(gè)路徑，但欠缺對(duì)路徑范圍的選擇。

一個(gè)邏輯公式的可滿足性問(wèn)題也稱為模型檢測(cè)問(wèn)題，對(duì)于CTL* 有如下結(jié)論：

定理2 ①CTL*的模型檢測(cè)問(wèn)題是多項(xiàng)式時(shí)間完備的；②CTL*的模型檢測(cè)問(wèn)題具有NP 難度和co-NP 難度[16]。

CTL*是CTL 和LTL 的超集，表達(dá)能力雖然得到了加強(qiáng)，但仍然存在著兩個(gè)主要缺陷。首先CTL*公式描述的是系統(tǒng)從某一狀態(tài)s 開(kāi)始后系統(tǒng)的所有可能發(fā)生的行為，并不關(guān)注系統(tǒng)是以一種什么樣的方式到達(dá)狀態(tài)s 的，換句話說(shuō)CTL*公式不能描述狀態(tài)s 之前的系統(tǒng)行為。另外CTL*的缺陷是只能定性地描述系統(tǒng)建立可能發(fā)生的行為，但卻不能精確地描述該行為發(fā)生的確切時(shí)間，該類性質(zhì)對(duì)于并發(fā)系統(tǒng)中區(qū)間相關(guān)性質(zhì)尤為重要[17]。

2.4 LTL 和CTL 的比較

定義4 LTL 公式和CTL 公式的等價(jià)性。

如果一個(gè)LTL 公式φ 和一個(gè)CTL 公式? 是等價(jià)的，記作φ≡?，那么對(duì)于任意遷移系統(tǒng)（transition system，TS）上的原子命題來(lái)說(shuō)，當(dāng)且僅當(dāng)下面的式子成立

從公式形式上來(lái)看，在LTL 公式上添加全稱路徑量詞得到CTL 公式，這是因?yàn)長(zhǎng)TL 公式默認(rèn)包含量詞。

然而并不是簡(jiǎn)單地去掉CTL 公式中的路徑量詞就得到相應(yīng)的LTL 公式，例如CTL 公式?◇?□a 和LTL 公式◇□a 并不是等價(jià)的。LTL 公式◇□a的含義是從某個(gè)狀態(tài)開(kāi)始，命題a會(huì)永遠(yuǎn)成立，然而CTL 公式?◇?□a 的語(yǔ)義解釋是對(duì)于任意一條路徑，最終會(huì)到達(dá)某個(gè)狀態(tài)s，使得s｜=?□a，當(dāng)且僅當(dāng)對(duì)于任意一條路徑π＝s0，s1，s2，…∈Path（s）會(huì)有狀態(tài)sj使得sj｜=?□a 成立，這也意味著狀態(tài)sj之后的所有可達(dá)狀態(tài)都滿足原子命題a。

對(duì)于LTL 公式◇□a 來(lái)說(shuō)是滿足圖1 中狀態(tài)遷移系統(tǒng)的，初始狀態(tài)s0滿足公式◇□a，從s0出發(fā)最終會(huì)停留狀態(tài)s0或者s2，是滿足該公式的語(yǔ)義“從某一狀態(tài)開(kāi)始a 永遠(yuǎn)為真”。然而對(duì)于CTL 公式?◇?□a 來(lái)說(shuō)不滿足圖2 中的狀態(tài)遷移系統(tǒng)，該公式在狀態(tài)s0處不成立，記作s0ω｜≠◇?□a，這是因?yàn)槁窂絪0*，s1，s2ω經(jīng)過(guò)了一個(gè)不滿足原子命題a 的狀態(tài)s1，其中s0*表示由狀態(tài)s0構(gòu)成的有窮序列，s2ω表示由狀態(tài)s2構(gòu)成的無(wú)窮序列。

圖1 LTL 公式◇□a 的狀態(tài)遷移系統(tǒng)Fig.1 The state transition system of LTL ◇□a

圖2 CTL 公式?◇?□a 的計(jì)算樹(shù)展開(kāi)形式Fig.2 The expansion form of computation tree of Formula CTL formula ?◇?□a

另外，許多學(xué)者也對(duì)LTL 和CTL 的區(qū)別進(jìn)行過(guò)系統(tǒng)研究。這兩種邏輯使用同一套符號(hào)體系，造成語(yǔ)義上的模糊，關(guān)于這兩種邏輯孰優(yōu)孰劣，學(xué)者們有著不同的爭(zhēng)論。兩種時(shí)序邏輯的公式是一樣的，關(guān)鍵在于語(yǔ)義的區(qū)別。LTL 以路徑作為命題的論斷對(duì)象，而CTL 以狀態(tài)作為命題的論斷對(duì)象。圖靈獎(jiǎng)得主Lamport 的結(jié)論是[18]：LTL 和CTL 一般來(lái)說(shuō)是不能相比的，但在證明并發(fā)程序的某些性質(zhì)時(shí)LTL 要優(yōu)于CTL，而在證明非確定性程序的某些性質(zhì)時(shí)CTL 要優(yōu)于LTL。Lamport 和Emerson 等曾討論過(guò)LTL 和CTL 的本質(zhì)區(qū)別，及其用于程序驗(yàn)證時(shí)功能上的不同。那么它們的不同之處在于語(yǔ)義上的區(qū)別，主要體現(xiàn)在下列事實(shí)上。

定理3 在LTL 中□p≡→p，但在CTL 中◇p?≡→p。

其中，→p 的含義表示“有時(shí)p 成立”。該定理表明在不同語(yǔ)義模型下，LTL 和CTL 是不等價(jià)的，針對(duì)這兩種不同時(shí)序邏輯的表達(dá)能力問(wèn)題，Lamport定義了強(qiáng)等價(jià)性。

定義5 給定時(shí)序結(jié)構(gòu)M=（S，X，D），其中S 為非空狀態(tài)集，X 是非空路徑集，D 是一個(gè)映射。如果對(duì)于每條路徑a∈X 來(lái)說(shuō)都有（L，M，a）｜=p 成立，則稱時(shí)序公式p 是在線性語(yǔ)義下M 為真，記作（L，M）→p。類似的，如果對(duì)于每個(gè)狀態(tài)t∈S 都有（B，M，t）→p成立，則稱時(shí)序公式p 在分支意義下M 為真。其中L 表示線性語(yǔ)義，B 表示分支語(yǔ)義。

定義6 令p 和q 表示兩個(gè)時(shí)序公式，C 是由一組時(shí)序結(jié)構(gòu)組成的類，如果對(duì)C 中的每個(gè)時(shí)序結(jié)構(gòu)，有如下公式成立

式中：I 和J 是兩個(gè)語(yǔ)義解釋，可以是線性語(yǔ)義L 或分支語(yǔ)義B，則稱時(shí)序公式p 和q 分別在語(yǔ)義解釋I 和J 下，相對(duì)于結(jié)構(gòu)類C 是強(qiáng)等價(jià)的，記作p=q（I，J，C）。

基于上述定義，可以證明得到如下兩個(gè)定理。

定理4 存在這樣的結(jié)構(gòu)類C，使得CTL 公式◇p 不強(qiáng)等價(jià)于任何LTL 公式。

定理5 存在這樣的結(jié)構(gòu)類C，使得LTL 公式→◇p 不強(qiáng)等價(jià)于任何CTL 公式。

上述定理的證明過(guò)程在文獻(xiàn)[19]中已經(jīng)給出，對(duì)于上述結(jié)論，可以用下面的例子進(jìn)行說(shuō)明。設(shè)P是一個(gè)不確定性程序，則P 的計(jì)算路徑和計(jì)算結(jié)果有多種可能性，如果要證明不管P 走哪一條路徑，它的計(jì)算最終必將終止，那么這個(gè)性質(zhì)用CTL 公式表示為?◇terminated（P），根據(jù)定理4，該公式是無(wú)法用LTL 公式表示的，因此在這一點(diǎn)上CTL 是強(qiáng)于LTL 的。另一方面，設(shè)Q 是一個(gè)并發(fā)程序，其中包含許多并發(fā)執(zhí)行的分量，如果要證明Q 對(duì)各分量Qi的調(diào)度符合公平性原則，即任何一個(gè)分量，只要獲取無(wú)數(shù)多次可執(zhí)行機(jī)會(huì)，則一定會(huì)被執(zhí)行，該性質(zhì)可以用LTL 表示為□?enabled（Qi）∨execute（Qi），根據(jù)定理5，該公式是無(wú)法用CTL 表示的。因此在這一點(diǎn)上LTL 又強(qiáng)于CTL。對(duì)于該結(jié)論的可靠性，Emerson 指出Lamport 的強(qiáng)等價(jià)性的要求過(guò)高，該結(jié)論是以某個(gè)斷言在所有狀態(tài)或所有路徑上為真的前提下進(jìn)行比較的。

對(duì)于這兩種時(shí)序邏輯的比較，從邏輯的角度看這兩種語(yǔ)言各有長(zhǎng)短。實(shí)際應(yīng)用于模型檢測(cè)中，普遍認(rèn)為對(duì)于安全屬性如公平性和活性的描述，使用LTL 表示更具有優(yōu)勢(shì)。但是從計(jì)算的角度來(lái)看，實(shí)現(xiàn)CTL 模型檢測(cè)相對(duì)簡(jiǎn)單，LTL 模型檢測(cè)問(wèn)題是PSPACE-完全的，而CTL 模型檢測(cè)時(shí)間是線性或多項(xiàng)式的。從模型檢測(cè)的發(fā)展歷程來(lái)看，在模型檢測(cè)早期，以SMV 為代表的CTL 模型檢測(cè)器對(duì)硬件、數(shù)字電路驗(yàn)證占主導(dǎo)地位。但對(duì)于刻畫(huà)系統(tǒng)性質(zhì)的規(guī)約，使用LTL 更加簡(jiǎn)潔且容易理解，再加上LTL 模型檢測(cè)算法有巨大進(jìn)步，Cadence SMV 和SPIN 這類LTL 模型檢測(cè)工具得到廣泛應(yīng)用。

對(duì)于LTL，CTL 的模型檢測(cè)，由于兩者的語(yǔ)義解釋不同造成模型檢測(cè)方法的不同。在對(duì)LTL 公式φ進(jìn)行模型檢測(cè)時(shí)，模型檢測(cè)工具會(huì)對(duì)φ 取反得到有限自動(dòng)機(jī)A?φ，然后與系統(tǒng)模型的有限自動(dòng)機(jī)AM相乘，驗(yàn)證兩個(gè)自動(dòng)機(jī)的交集是否為空，若不為空，則表示設(shè)計(jì)中有不滿足屬性的行為。而對(duì)CTL 公式進(jìn)行模型檢測(cè)是以Kripke 結(jié)構(gòu)圖的所有狀態(tài)為根節(jié)點(diǎn)進(jìn)行搜索，如果存在不滿足屬性的模型，即得到違反屬性的反例路徑。通過(guò)對(duì)比這兩種不同公式的模型檢測(cè)方法，可以得出LTL 模型檢測(cè)可以快速完成對(duì)路徑上的狀態(tài)搜索，所需要的狀態(tài)數(shù)比CTL 模型檢測(cè)更少。

3 連續(xù)時(shí)間模型的時(shí)序邏輯

本節(jié)介紹基于連續(xù)時(shí)間模型的時(shí)序邏輯，包括ITL 和PTL，對(duì)兩種邏輯系統(tǒng)進(jìn)行分析比較，指出它們的適用范圍。

3.1 區(qū)間時(shí)序邏輯ITL

LTL，CTL 公式的語(yǔ)義在獨(dú)立的點(diǎn)上被解釋，一個(gè)點(diǎn)代表一個(gè)狀態(tài)，點(diǎn)之間的關(guān)系就代表時(shí)序之間的關(guān)系，這樣的時(shí)序關(guān)系無(wú)法描述正則表達(dá)式所表達(dá)的性質(zhì)。由于基于連續(xù)時(shí)間模型的時(shí)序邏輯的表達(dá)能力較弱，使得對(duì)一些性質(zhì)的驗(yàn)證無(wú)法進(jìn)行。因此很多關(guān)于LTL 的擴(kuò)展已經(jīng)被提出，如Kozen 提出了μ 演算[12]，Vardi 提出了ETL[13]。盡管這些時(shí)序邏輯具備完全正則語(yǔ)言能力，但仍難以表達(dá)一些狀態(tài)敏感的性質(zhì)，如原子命題p 在某個(gè)具體狀態(tài)或具體區(qū)間上成立，此外如順序、循環(huán)等結(jié)構(gòu)難以表達(dá)。

與基于點(diǎn)語(yǔ)義的LTL 不同,系統(tǒng)的時(shí)間特征行為可能會(huì)出現(xiàn)在一系列時(shí)間區(qū)間上，那么就需要使用一些連續(xù)時(shí)間區(qū)間, 稱之為區(qū)間時(shí)間模型。Moszkowski 在其博士論文中提出了基于區(qū)間語(yǔ)義的ITL[20]，可用于描述區(qū)間中的狀態(tài)及其時(shí)序關(guān)系的性質(zhì)。

定理6 ITL 具有正則表達(dá)能力，能夠方便地表達(dá)狀態(tài)敏感的性質(zhì)，以及順序、迭代等行為[20]。

由于ITL 定義在有窮區(qū)間范圍內(nèi), 主要包括chop，next 以及投影符號(hào)proj 等時(shí)序操作符，因此使得ITL 比LTL 具有更強(qiáng)的表達(dá)能力。作為時(shí)序邏輯的一個(gè)重要分支，現(xiàn)在已經(jīng)擴(kuò)展應(yīng)用在并發(fā)軟件系統(tǒng)的規(guī)約和驗(yàn)證，但I(xiàn)TL 的缺陷在于只能應(yīng)用于有窮區(qū)間。

在ITL 中有兩個(gè)最具特色的動(dòng)作算子: 分割算子“；”（chop operator）和投影算子proj（projection operator）。分割算子“；”的作用是把一個(gè)有窮區(qū)間分割成兩個(gè)部分，可以表示成p，q，該公式的含義為前一部分性質(zhì)p 成立，后一部分性質(zhì)q 成立。投影算子proj 具有可重復(fù)行為，P proj Q 把一個(gè)有窮區(qū)間Q 分割成多份具有相同長(zhǎng)度的子區(qū)間。投影算子的主要作用是能產(chǎn)生重復(fù)操作的結(jié)構(gòu)，可用于描述Loops 循環(huán)，例如動(dòng)作P 每隔時(shí)間n 就執(zhí)行一次可描述為P proj len（n）。

3.2 投影時(shí)序邏輯PTL

由于ITL 是定義在有窮區(qū)間上的時(shí)序邏輯，所以該邏輯的缺陷是無(wú)法描述系統(tǒng)中的無(wú)窮行為。針對(duì)ITL 存在的問(wèn)題，西安電子科技大學(xué)段振華等提出了投影時(shí)序邏輯PTL[21]，對(duì)ITL 進(jìn)行擴(kuò)充到無(wú)窮區(qū)間范圍內(nèi)，并引入一個(gè)全新的投影操作結(jié)構(gòu)（P1，…，Pm）prj Q，從而得到一種描述有窮、無(wú)窮模型和時(shí)段的邏輯系統(tǒng)。

通過(guò)引入投影操作符號(hào)（P1，…，Pm）prj Q 將ITL推廣到無(wú)窮區(qū)間范圍，與原有的投影結(jié)構(gòu)P prj Q相比，新的投影操作更加靈活易用。PTL 相比ITL 的優(yōu)勢(shì)在于：由于擴(kuò)充了投影算子prj，PTL 可以應(yīng)用于無(wú)窮區(qū)間，允許用不同的時(shí)間粒度來(lái)描述計(jì)算的進(jìn)程，由此可定義順序、循環(huán)等操作。PTL 相比ITL更適合描述并發(fā)軟件[22-23]。

定理7 PPTL 具備完全正則表達(dá)能力，能夠?qū)樞?、并行、區(qū)間相關(guān)以及周期重復(fù)的性質(zhì)進(jìn)行描述[24-25]。

PTL 的一個(gè)命題子集也就是命題投影時(shí)序邏輯PPTL（propositional PTL，PPTL)的表達(dá)能力等價(jià)于Büchi 自動(dòng)機(jī)[26]，因而證明其具有完全正則表達(dá)能力。PPTL 不僅能夠表達(dá)離散時(shí)間模型上的時(shí)序性質(zhì)，還可以表達(dá)如區(qū)間相關(guān)性質(zhì)以及周期性重復(fù)的閉包性質(zhì)，主要使用區(qū)間長(zhǎng)度算子len（n），分割算子chop，chop star 和投影算子prj 來(lái)實(shí)現(xiàn)，具體性質(zhì)如下[4]：

1）區(qū)間相關(guān)的性質(zhì)。例如“命題p 在時(shí)間長(zhǎng)度為n 的區(qū)間上成立”可以表示為p∧len（n）；“命題p在第5 個(gè)和第10 個(gè)時(shí)間單元內(nèi)成立”可以表示為len（5）；◇p∧len（5）。

2）周期重復(fù)的性質(zhì)。例如“命題p 在偶數(shù)狀態(tài)上成立”可以表示為p∧（○2（p∧ε））*。因此對(duì)于驗(yàn)證實(shí)時(shí)系統(tǒng)的性質(zhì)不僅局限于傳統(tǒng)的安全性和活性，即描述性質(zhì)“事件p 在將來(lái)會(huì)成立”，還可以通過(guò)時(shí)間間隔描述對(duì)于時(shí)間有嚴(yán)格要求的性質(zhì)，例如性質(zhì)“事件p 將在一段時(shí)間間隔內(nèi)發(fā)生”。

3）順序、循環(huán)、迭代等結(jié)構(gòu)。PPTL 中的分割算子chop 和chop star 可以對(duì)該類結(jié)構(gòu)方便地進(jìn)行描述。

總的來(lái)說(shuō)，相比較其它時(shí)序邏輯如LTL，CTL 和ITL，PTL 的表達(dá)能力是完全正則的，等價(jià)于Büchi自動(dòng)機(jī)，能夠表達(dá)區(qū)間相關(guān)的性質(zhì)以及周期性重復(fù)的閉包性質(zhì)，可描述并發(fā)情況以及實(shí)時(shí)性相關(guān)性質(zhì)。雖然該邏輯的表達(dá)能力得到增強(qiáng)，但不可避免地帶來(lái)更高的模型檢測(cè)復(fù)雜度，減少系統(tǒng)狀態(tài)空間的方法如偏序規(guī)約、限界模型檢測(cè)以及組合驗(yàn)證等技術(shù)被引入到PPTL 模型檢測(cè)中[28-29]。

4 處理復(fù)雜計(jì)算特征的時(shí)序邏輯

為了處理復(fù)雜的計(jì)算特征，如實(shí)時(shí)、隨機(jī)、混成、開(kāi)放系統(tǒng)中的行為，許多時(shí)序邏輯被相繼提出。例如:為了描述隨機(jī)系統(tǒng)的高度不確定性，通過(guò)在計(jì)算樹(shù)邏輯中引入概率建立了概率計(jì)算樹(shù)邏輯以及連續(xù)隨機(jī)邏輯；為了描述實(shí)時(shí)系統(tǒng)中關(guān)于時(shí)間敏感的性質(zhì)，提出了時(shí)段演算等一系列邏輯語(yǔ)言；為了處理混成系統(tǒng)中同時(shí)包含離散變量和連續(xù)變量的復(fù)雜行為，提出了微分動(dòng)態(tài)邏輯；為了處理開(kāi)放系統(tǒng)中多進(jìn)程間的任意交互以及系統(tǒng)內(nèi)部與外界環(huán)境的交互，計(jì)算樹(shù)邏輯被擴(kuò)充為交替時(shí)序邏輯，下面將對(duì)這些時(shí)序邏輯變體及其適合描述哪些性質(zhì)進(jìn)行概述。

4.1 面向隨機(jī)系統(tǒng)的時(shí)序邏輯

隨機(jī)系統(tǒng)具有隨機(jī)不確定性，為了表達(dá)這種性質(zhì)概率時(shí)序邏輯被提出。概率屬性規(guī)約通常采用概率計(jì)算樹(shù)邏輯 （probabilistic computation tree logic，PCTL）[30]和連續(xù)隨機(jī)邏輯（continuous stochastic logic，CSL）[31]等概率時(shí)序邏輯描述。其中PCTL 是CTL的概率擴(kuò)展，應(yīng)用在離散時(shí)間馬爾科夫鏈和馬爾科夫決策，CSL 是在CTL 和PCTL 基礎(chǔ)上擴(kuò)展得到，應(yīng)用在連續(xù)時(shí)間馬爾可夫鏈, 下面對(duì)這兩種概率時(shí)序邏輯作詳細(xì)介紹與分析。

PCTL 適用于描述隨機(jī)不確定系統(tǒng)，能夠表達(dá)定量性質(zhì)。這種能力在隨機(jī)不確定性系統(tǒng)中是非常實(shí)用的，在形式化驗(yàn)證中有時(shí)并不要求系統(tǒng)性質(zhì)的絕對(duì)正確性，而是保證系統(tǒng)性質(zhì)在一定程度上的相對(duì)正確性。例如，在網(wǎng)絡(luò)通信過(guò)程中經(jīng)常會(huì)發(fā)生數(shù)據(jù)傳輸失敗的情況，因此需要對(duì)數(shù)據(jù)進(jìn)行重新發(fā)送。對(duì)如何使用PCTL 表達(dá)協(xié)議所期望的功能正確性和協(xié)議性能為例進(jìn)行說(shuō)明。在網(wǎng)絡(luò)通信過(guò)程中，組件A 和B 在發(fā)送消息時(shí)會(huì)有一定幾率發(fā)送失敗，如果發(fā)送失敗則會(huì)接著發(fā)送直到消息發(fā)送成功。

P＜0.05［X error A］：組件A 發(fā)送消息失敗的概率小于0.05。

P＜0.05［true U≤kmessage_num≥5］：在經(jīng)過(guò)k 步遷移之后，至少5 條消息被組件A 或B 成功發(fā)送的概率小于0.05。

P＞0.9［F＜100 “enabled”］：在經(jīng)過(guò)100 步遷移之后，消息全部發(fā)送成功達(dá)到穩(wěn)定狀態(tài)的概率大于0.9。

CSL 也是由CTL 的概率擴(kuò)展得到，它是在CTL的基礎(chǔ)上添加了兩個(gè)新的算子：路徑概率算子P 和穩(wěn)定狀態(tài)算子S，可以用來(lái)描述連續(xù)時(shí)間馬爾科夫鏈的穩(wěn)態(tài)行為，公式S～p（φ）表示一個(gè)狀態(tài)滿足φ 的穩(wěn)態(tài)概率～p。CSL 的語(yǔ)法中引入了一個(gè)新的公式?1∪I?2，其中I 是R 的時(shí)間間隔，而PCTL 中操作符∪被離散時(shí)間k 約束。因此CSL 與PCTL 的區(qū)別在于CSL 能夠表達(dá)某個(gè)自然數(shù)區(qū)間的行為，而PCTL 是不能的。除了S～p（φ）以外，在CSL 中的狀態(tài)公式與PCTL 沒(méi)有區(qū)別，它類似于PCTL 中的P～p（φ），表示在滿足～p 的概率條件下，將會(huì)保持在狀態(tài)φ很長(zhǎng)時(shí)間。CSL 適用于描述在連續(xù)時(shí)間段之內(nèi)需要滿足的性質(zhì)，例如“在緊急情況下，飛行控制系統(tǒng)中的閥門必須在1 秒之內(nèi)打開(kāi)的概率大于99%”,表示為

目前PCTL 和CSL 已經(jīng)在概率模型檢測(cè)器PRISM 中得到支持和應(yīng)用，被用于規(guī)約概率系統(tǒng)的期望屬性。此外PRISM 通過(guò)擴(kuò)展回報(bào)，一個(gè)形如的r：S×S→R≥0 回報(bào)結(jié)構(gòu)將非負(fù)數(shù)的回報(bào)值添加到狀態(tài)遷移過(guò)程中，可用于分析與回報(bào)期望值相關(guān)的屬性，這是通過(guò)擴(kuò)充R 算子實(shí)現(xiàn)的。以分布式系統(tǒng)中的自穩(wěn)定算法為例進(jìn)行說(shuō)明，在分布式環(huán)境下往往要求系統(tǒng)具有自穩(wěn)定性，這就要求自穩(wěn)定算法在沒(méi)有外界干預(yù)下，經(jīng)過(guò)有限次步驟后從一個(gè)雜亂無(wú)章的初始狀態(tài)到達(dá)一個(gè)穩(wěn)定狀態(tài)。對(duì)于自穩(wěn)定算法關(guān)于時(shí)間消耗的屬性，通過(guò)一個(gè)簡(jiǎn)單的回報(bào)結(jié)構(gòu)time將系統(tǒng)中每一步的狀態(tài)遷移的回報(bào)值設(shè)定為1，有如下公式

4.2 面向?qū)崟r(shí)系統(tǒng)的時(shí)序邏輯

實(shí)時(shí)系統(tǒng)是一種能夠在有限時(shí)間范圍內(nèi)對(duì)來(lái)自外部輸入等做出快速響應(yīng)的系統(tǒng)，例如控制系統(tǒng)、監(jiān)測(cè)系統(tǒng)、通信系統(tǒng)等。實(shí)時(shí)系統(tǒng)的部件之間具有并發(fā)性，運(yùn)行通常并不終止，對(duì)規(guī)定動(dòng)作的進(jìn)行和完成時(shí)間也有很高的要求。

時(shí)段演算適用于對(duì)實(shí)時(shí)系統(tǒng)的實(shí)時(shí)需求進(jìn)行刻畫(huà)[34]，不僅能夠像其它實(shí)時(shí)邏輯描述刻度時(shí)間性質(zhì)和時(shí)間邊界特性，還可以描述一段時(shí)間范圍內(nèi)性質(zhì)的累積。以燃?xì)馊紵鳛槔瑢?duì)如何使用時(shí)段演算形式化刻畫(huà)離散狀態(tài)系統(tǒng)的實(shí)時(shí)特性進(jìn)行說(shuō)明。我們希望控制煤氣燃燒器的點(diǎn)火機(jī)制和關(guān)閉機(jī)制，把煤氣泄漏控制在安全閾值之內(nèi)。需求說(shuō)明為：在煤氣灶使用期間如果對(duì)其連續(xù)觀察超過(guò)60 s，那么煤氣泄漏的時(shí)間不能超過(guò)觀測(cè)時(shí)間的1/20。引入b和e 分別表示觀測(cè)的起始、截止時(shí)間，只有當(dāng)煤氣被釋放且沒(méi)有火焰出現(xiàn)的狀態(tài)被稱為煤氣泄漏，用布爾函數(shù)Leak（t）來(lái)表示煤氣的泄漏狀態(tài)，可表示Leak（t）?Gas（t）∧?Flame（t）為,那么該安全需求形式化表示為

設(shè)計(jì)原則2：任何兩個(gè)泄露時(shí)段的時(shí)間間隔不能少于30 s。

通過(guò)上面的示例可以看出，時(shí)段演算繼承了ITL 的優(yōu)點(diǎn)，克服了基于點(diǎn)語(yǔ)義的CTL*及其子集只能描述某個(gè)時(shí)刻系統(tǒng)狀態(tài)的性質(zhì)，能夠描述時(shí)段累積性質(zhì)，那么一個(gè)狀態(tài)的前驅(qū)序列的性質(zhì)也可以通過(guò)時(shí)段演算公式表示，因此時(shí)段演算被廣泛應(yīng)用于實(shí)時(shí)系統(tǒng)的形式化驗(yàn)證當(dāng)中。雖然時(shí)段演算強(qiáng)大的性質(zhì)表達(dá)能力使其對(duì)系統(tǒng)規(guī)約帶來(lái)很大的方便性，但與此同時(shí)基于時(shí)段演算的自動(dòng)化驗(yàn)證是十分困難的，時(shí)段演算沒(méi)有絕對(duì)意義上的完備公理系統(tǒng)，時(shí)段演算公式的可滿足性與模型檢測(cè)問(wèn)題都是不可判定的。目前的做法是針對(duì)時(shí)間模型做一些限制（如對(duì)離散時(shí)間域的長(zhǎng)度進(jìn)行限制得到有界離散時(shí)間模型）或者限制模態(tài)算子的使用來(lái)得到其可判定的子集和模型檢測(cè)子集[35]。

此外，針對(duì)實(shí)時(shí)系統(tǒng)的性質(zhì)規(guī)約與驗(yàn)證，還有許多時(shí)序邏輯被相繼提出，對(duì)它們的研究主要分為兩個(gè)方向。其中一種是通過(guò)在時(shí)序邏輯中引入含時(shí)間 界 限 的 時(shí) 序 算 子 （如□≤tφ，□≤［t1，t2］φ，◇≤tφ，◇≤［t1，t2］φ）來(lái)表示實(shí)時(shí)性質(zhì)，包括時(shí)間計(jì)算樹(shù)邏輯[36]和度量區(qū)間時(shí)序邏輯[37]等。另外一種是在時(shí)序邏輯中引入顯式的時(shí)鐘變量來(lái)表示時(shí)間約束，代表性的有實(shí)時(shí)時(shí)序邏輯[38]，例如性質(zhì)“命題p 在時(shí)間區(qū)間［t1，t2］內(nèi)成立”可形式化表示為：?u（t=u∧◇（p∧（u+t1≤t∧t≤u+t2））），其中，t 是全局時(shí)鐘變量，u 是剛性變量。上述時(shí)序邏輯適用于作為實(shí)時(shí)與混成系統(tǒng)的性質(zhì)規(guī)約語(yǔ)言，對(duì)于實(shí)時(shí)系統(tǒng)通常是利用時(shí)間自動(dòng)機(jī)或者混成自動(dòng)機(jī)來(lái)建模，模型構(gòu)建和屬性規(guī)約分別采用兩種不同的語(yǔ)言來(lái)描述。針對(duì)該方法的局限性李廣元提出了面向?qū)崟r(shí)系統(tǒng)的連續(xù)時(shí)序邏輯[39]，這是LTL 在實(shí)時(shí)領(lǐng)域的一種擴(kuò)展，該邏輯語(yǔ)言繼承了時(shí)序邏輯程序設(shè)計(jì)語(yǔ)言的優(yōu)點(diǎn)，既能夠表示實(shí)時(shí)系統(tǒng)的實(shí)現(xiàn)與性質(zhì)規(guī)約，又能在統(tǒng)一的語(yǔ)義框架下表示高層的需求規(guī)約與低層的實(shí)現(xiàn)模型之間不同抽象級(jí)別的描述。

4.3 面向混成系統(tǒng)的時(shí)序邏輯

混成系統(tǒng)是一種特殊的實(shí)時(shí)系統(tǒng)，混成系統(tǒng)的研究對(duì)象包括嵌入式系統(tǒng)和信息物理融合系統(tǒng)等[40]。該類系統(tǒng)的特征是既有離散的邏輯控制又有連續(xù)的時(shí)間行為，并且這兩部分行為相互交織混雜在同一系統(tǒng)中。混成系統(tǒng)的狀態(tài)變化既隨時(shí)間連續(xù)變化，也受到離散事件驅(qū)動(dòng)[41]。20 世紀(jì)90 年代以來(lái)，隨著混成系統(tǒng)在工業(yè)、航空航天領(lǐng)域得到廣泛應(yīng)用，對(duì)該類系統(tǒng)的安全性和可靠性提出了嚴(yán)格要求，保障混成系統(tǒng)的可靠性是目前的研究熱點(diǎn)。普通的時(shí)段演算主要關(guān)注離散狀態(tài)系統(tǒng)中某類狀態(tài)在給定觀測(cè)時(shí)間區(qū)間（時(shí)段）上的積分，而對(duì)于混成系統(tǒng)中的連續(xù)動(dòng)態(tài)行為缺乏相應(yīng)的描述機(jī)制。Raven 提出了擴(kuò)展的時(shí)段演算（extended duration calculus，EDC），在原有的時(shí)段演算基礎(chǔ)上引入連續(xù)實(shí)值函數(shù)對(duì)混成系統(tǒng)的連續(xù)動(dòng)態(tài)行為進(jìn)行描述，混成系統(tǒng)的模型以及性質(zhì)被擴(kuò)展的時(shí)段演算公式形式化表示，然后基于時(shí)段演算的公理系統(tǒng)和推理規(guī)則對(duì)混成系統(tǒng)進(jìn)行推理驗(yàn)證。

由于混成系統(tǒng)的并發(fā)性和時(shí)間屬性使得混成系統(tǒng)的狀態(tài)空間極為龐大，而且系統(tǒng)中的狀態(tài)可達(dá)性不可判定使得基于模型檢測(cè)的混成系統(tǒng)形式化驗(yàn)證難以開(kāi)展。André Platzerti[42]提出了一類描述混成系統(tǒng)屬性的規(guī)約語(yǔ)言：微分動(dòng)態(tài)邏輯（differential dynamic logic，DDL）家族，該類邏輯是離散一階動(dòng)態(tài)邏輯的擴(kuò)展，DDL 在離散一階動(dòng)態(tài)邏輯的基礎(chǔ)上引入了描述連續(xù)狀態(tài)變化的結(jié)構(gòu)，利用混成程序（hybrid program）建?；斐上到y(tǒng)中狀態(tài)以及狀態(tài)變遷，具體為使用離散跳躍集表示混成系統(tǒng)中的離散變遷，使用微分方程組描述系統(tǒng)動(dòng)態(tài)行為中的連續(xù)變遷，然后通過(guò)控制結(jié)構(gòu)操作符（U，*，∶）將系統(tǒng)的離散和連續(xù)行為組合在一起。

DDL 適用于描述混成系統(tǒng)中離散變遷與連續(xù)動(dòng)態(tài)行為特征[43]。這表明DDL 可用于描述混成系統(tǒng)中連續(xù)變化的物理層和離散變化的控制層之間的相互交互過(guò)程，并且相關(guān)推理規(guī)則已經(jīng)被提出，能對(duì)混成系統(tǒng)的行為特性進(jìn)行推理驗(yàn)證?；贒DL對(duì)混成系統(tǒng)的形式化驗(yàn)證主要是采用定理證明方法，同時(shí)結(jié)合了組合驗(yàn)證思想，在驗(yàn)證過(guò)程中對(duì)待驗(yàn)證屬性公式進(jìn)行逐步分解然后獨(dú)立驗(yàn)證，能夠明顯克服基于混成自動(dòng)機(jī)、混成Petri 網(wǎng)驗(yàn)證混成系統(tǒng)時(shí)面臨的狀態(tài)爆炸問(wèn)題，提高驗(yàn)證效率并能夠保持系統(tǒng)模型特征與變遷結(jié)構(gòu)。

DDL 具有良好的擴(kuò)展性，基于DDL 的定理證明是在給定的公理和推理規(guī)則上進(jìn)行，為了使DDL具有更強(qiáng)大的證明能力，可以對(duì)DDL 的公理系統(tǒng)和推理規(guī)則進(jìn)行擴(kuò)充。目前在DDL 基礎(chǔ)上根據(jù)不同的應(yīng)用情況以及不同的操作模型衍生出許多變體，包括微分代數(shù)動(dòng)態(tài)邏輯 （differential-algebraic dynamic logic，DAL），微分時(shí)序動(dòng)態(tài)邏輯（differential temporal dynamic logic，dTL），微分代數(shù)時(shí)序動(dòng)態(tài)邏輯（differential-algebraic temporal dynamic logic，DATL）以及量化微分動(dòng)態(tài)邏輯（quantified differential dynamic logic，QdL）[44-46]。DDL 缺乏描述物理環(huán)境中連續(xù)動(dòng)態(tài)行為特性的有效方法，同時(shí)存在微分方程不可解的情況，針對(duì)該問(wèn)題在一階動(dòng)態(tài)邏輯的基礎(chǔ)上提出了DAL，使用微分不變量技術(shù)進(jìn)行推理驗(yàn)證而不必求解微分方程。為了驗(yàn)證混成系統(tǒng)中的時(shí)序?qū)傩?，將DDL，DAL 分別與時(shí)序邏輯相結(jié)合得到dTL 和DATL，DATL 將動(dòng)態(tài)邏輯的模態(tài)操作符和時(shí)序邏輯的時(shí)序操作符完美結(jié)合在一起，得到形如的邏輯公式，可以同時(shí)描述系統(tǒng)的時(shí)序行為和非時(shí)序行為。為了處理分布式混成系統(tǒng)的形式化驗(yàn)證，基于一階動(dòng)態(tài)邏輯和量化的微分方程相結(jié)合得到QdL。DDL家族之間的關(guān)系可以用圖3 來(lái)說(shuō)明。

圖3 微分動(dòng)態(tài)邏輯家族示意圖Fig.3 Schematic diagram of differential dynamic logic family

4.4 面向開(kāi)放系統(tǒng)的時(shí)序邏輯

封閉系統(tǒng)的行為由當(dāng)前系統(tǒng)所處的狀態(tài)決定，與外部環(huán)境無(wú)關(guān)，針對(duì)封閉系統(tǒng)的模型檢測(cè)主要采用LTL 或CTL 來(lái)描述系統(tǒng)的性質(zhì)。開(kāi)放系統(tǒng)的行為不僅由系統(tǒng)當(dāng)前所處狀態(tài)決定，同時(shí)也受到外部環(huán)境的約束[47]。與封閉系統(tǒng)相比，開(kāi)放系統(tǒng)的外部環(huán)境是不確定的，開(kāi)放系統(tǒng)中不同組件之間的交互會(huì)導(dǎo)致難以預(yù)測(cè)的情況發(fā)生，如可觀測(cè)性以及可控性等。因此，開(kāi)放系統(tǒng)的形式化驗(yàn)證需要將外部環(huán)境的各種不確定情況納入考慮范圍內(nèi)[48]。Alur 提出了交替時(shí)序邏輯（alternating-time temporal logic，ATL）[49]，該邏輯描述的是開(kāi)放系統(tǒng)與外界環(huán)境之間的交互以及內(nèi)部組件之間的合作與競(jìng)爭(zhēng)關(guān)系，將系統(tǒng)中的各組件之間的交互最終到達(dá)的穩(wěn)定狀態(tài)規(guī)約為開(kāi)放系統(tǒng)與外界環(huán)境之間的博弈結(jié)果，所以又被稱為博弈邏輯。

ATL 適用于描述開(kāi)放系統(tǒng)與外界環(huán)境之間的交互以及內(nèi)部組件之間的合作與競(jìng)爭(zhēng)關(guān)系[50]。這表明對(duì)于系統(tǒng)行為同時(shí)受到內(nèi)部結(jié)構(gòu)和外部環(huán)境輸入的開(kāi)放系統(tǒng)，系統(tǒng)不同組件之間交互后最終達(dá)到的狀態(tài)，可以使用ATL 規(guī)約為開(kāi)放系統(tǒng)與外部環(huán)境之間的博弈。以幾個(gè)簡(jiǎn)單的例子介紹如何使用ATL來(lái)描述開(kāi)放系統(tǒng)中各個(gè)主體之間的合謀與對(duì)抗行為，來(lái)說(shuō)明ATL 對(duì)于開(kāi)放系統(tǒng)的表達(dá)能力。假設(shè)存在參與者集合∑＝｛a，b，c｝，不同的參與者存在著策略使得命題p 成立，同時(shí)不同參與者之間存在著合謀與競(jìng)爭(zhēng)，有如下ATL 公式：

《a》◇p：針對(duì)參與者b 和c，參與者a 存在一個(gè)獲勝策略使得命題p 最終成立。

《b，c》□p：針對(duì)參與者a,無(wú)論參與者b 和c 如何合謀，永遠(yuǎn)不能避免系統(tǒng)最終達(dá)到一個(gè)狀態(tài)使得命題p 成立。

《a，b》○（p∧?《c》□p）：針對(duì)參與者c，參與者a和b 合謀能夠使得下一狀態(tài)命題p 成立，并且從下一狀態(tài)開(kāi)始參與者c 永遠(yuǎn)不能使命題p 成立。

上述公式形式化地描述了一個(gè)開(kāi)放系統(tǒng)中不同成員之間的合作與對(duì)抗行為，這種表達(dá)能力對(duì)于描述電子商務(wù)協(xié)議這種開(kāi)放系統(tǒng)是非常合適且有效的。與傳統(tǒng)的安全協(xié)議中協(xié)議參與方是誠(chéng)實(shí)的相比，電子商務(wù)協(xié)議中除了可信第三方（trusted third party，TTP）是誠(chéng)實(shí)可信的，其他參與主體都是互不信任且會(huì)做出欺騙行為。例如電子支付協(xié)議中存在消費(fèi)者已經(jīng)收到貨物但是卻拒不承認(rèn)的情況，或者消費(fèi)者與攻擊者合謀一起欺騙商家等惡意行為，電子商務(wù)協(xié)議中的安全威脅不僅僅來(lái)自外部環(huán)境，更多的是協(xié)議參與方之間的合謀與對(duì)抗。在基于Dolev-Yao 模型的協(xié)議分析過(guò)程中，安全協(xié)議被當(dāng)作一個(gè)封閉系統(tǒng)進(jìn)行研究，不能有效地描述協(xié)議與外部環(huán)境之間的交互。而基于ATL 的電子商務(wù)協(xié)議安全性分析中，充分考慮了協(xié)議主體間的相互博弈，所有協(xié)議參與方根據(jù)自身利益最大化選擇適合自己的策略，根據(jù)博弈結(jié)果決定自己下一步動(dòng)作，能夠?qū)f(xié)議主體間的合謀與對(duì)抗行為進(jìn)行精確地描述。目前實(shí)驗(yàn)結(jié)果表明ATL 比LTL，CTL 更適合分析電子商務(wù)協(xié)議這一類開(kāi)放系統(tǒng)，已經(jīng)成功發(fā)現(xiàn)合同簽署協(xié)議、公平交換協(xié)議中存在不滿足公平性等缺陷[51-52]。

此后有許多研究工作對(duì)ATL 進(jìn)行擴(kuò)展形成了ATL 家族，主要體現(xiàn)在策略表示、與其它邏輯相融合等方面的擴(kuò)展。ATL 規(guī)定每一個(gè)路徑選擇量詞《A》必須有一個(gè)時(shí)序算子相匹配，針對(duì)該缺陷提出的ATL*支持這兩種算子之間的任意嵌套，因此ATL*的性質(zhì)表達(dá)能力比ATL 更強(qiáng)。ATL中只能對(duì)策略進(jìn)行量化，模糊地表示存在某一策略使得性質(zhì)φ 成立，但不能明確指出是哪一個(gè)策略使得性質(zhì)φ 成立，針對(duì)該問(wèn)題具體策略交替時(shí)序邏輯（ATL with explicit strategies，ATLES）[53]被 提出。為了將行動(dòng)的實(shí)施與其所掌握的知識(shí)前提（knowledge precondition）形式化表示，文獻(xiàn)[54]將ATL 與認(rèn)知邏輯（epistemic logic）相結(jié)合提出了交替認(rèn)知時(shí)序邏輯（alternating-time temporal epistemic logic，ATEL）。為了解決開(kāi)放系統(tǒng)的驗(yàn)證過(guò)程中沒(méi)有考慮隨機(jī)行為的問(wèn)題，通過(guò)引入概率分布到認(rèn)知模型中來(lái)描述系統(tǒng)中的隨機(jī)性，文獻(xiàn)[55]基于ATEL 提出了概率交替時(shí)序認(rèn)知邏輯（probabilistic alternating-time temporal epistemic logic，PATEL），能夠?qū)﹂_(kāi)放系統(tǒng)中的知識(shí)前提及其它性質(zhì)進(jìn)行定量驗(yàn)證。文獻(xiàn)[56]將ATL 與投影時(shí)序邏輯PTL 結(jié)合提出了交替投影時(shí)序邏輯（alternating projection temporal logic，APTL），該邏輯融合了這兩種邏輯的優(yōu)點(diǎn)，不僅可以描述有窮區(qū)間、無(wú)窮區(qū)間內(nèi)的性質(zhì)，還可以描述開(kāi)放系統(tǒng)中與博弈相關(guān)的性質(zhì)。上述ATL 家族之間的關(guān)系如圖4 所示。

圖4 交替時(shí)序邏輯家族示意圖Fig.4 Schematic diagram of alternating-time temporal logic family

5 時(shí)序邏輯未來(lái)的研究方向

從時(shí)序邏輯的發(fā)展趨勢(shì)來(lái)看，今后一段時(shí)間時(shí)序邏輯的研究工作包括以下幾個(gè)方面：

1）擴(kuò)充已有的時(shí)序邏輯，使其能夠適用于復(fù)雜系統(tǒng)的形式化規(guī)約。例如，隨著大規(guī)模集成電路和EDA 技術(shù)的發(fā)展，片上系統(tǒng)（system on chip）成為嵌入式系統(tǒng)的發(fā)展方向，減少片上系統(tǒng)中的設(shè)計(jì)錯(cuò)誤，提高系統(tǒng)的設(shè)計(jì)可靠性是關(guān)鍵性問(wèn)題，基于仿真的方法中存在著覆蓋率不足、仿真時(shí)間過(guò)長(zhǎng)等問(wèn)題。信號(hào)時(shí)序邏輯[57]是在模擬和混合信號(hào)電路背景下提出的規(guī)約語(yǔ)言，以LTL 為基礎(chǔ)同時(shí)具有實(shí)時(shí)和實(shí)值約束，可以描述離散和連續(xù)系統(tǒng)的實(shí)時(shí)屬性。在量子計(jì)算方面，隨著量子計(jì)算機(jī)在計(jì)算速度方面有超越經(jīng)典計(jì)算機(jī)的絕對(duì)優(yōu)勢(shì)，量子程序的開(kāi)發(fā)及驗(yàn)證是發(fā)揮量子計(jì)算機(jī)能力的關(guān)鍵因素，目前基于CTL 的量子計(jì)算樹(shù)邏輯 （quantum computation tree logic，QCTL）[58-59]已被提出用于量子程序的性質(zhì)規(guī)約。此外，新的計(jì)算模式如大數(shù)據(jù)、機(jī)器學(xué)習(xí)算法不斷涌現(xiàn)，這些計(jì)算模式下程序行為與經(jīng)典的串行與并發(fā)程序有顯著差異，因此需要擴(kuò)充或設(shè)計(jì)新的時(shí)序邏輯來(lái)描述這些新的計(jì)算模式[60-61]。

2）研究不同形式化邏輯系統(tǒng)之間的組合，使得組合后的邏輯能夠吸收不同邏輯的特性。例如分離邏輯是對(duì)霍爾邏輯的擴(kuò)展，對(duì)于驗(yàn)證具有復(fù)雜數(shù)據(jù)結(jié)構(gòu)的動(dòng)態(tài)內(nèi)存程序非常實(shí)用，但從表達(dá)能力來(lái)看，分離邏輯并未突破一階邏輯的范疇，在描述和驗(yàn)證內(nèi)存的時(shí)序性質(zhì)方面仍有欠缺[62]。時(shí)序邏輯雖然能夠描述狀態(tài)隨時(shí)間變化系統(tǒng)的時(shí)序性質(zhì)，但不能夠描述帶有指針的程序性質(zhì),文獻(xiàn)[63-64]提出一種結(jié)合分離邏輯和PPTL 的二維(時(shí)間和空間)時(shí)序邏輯PPTLSL，該邏輯繼承了分離邏輯和PPTL 的優(yōu)勢(shì)，能夠描述指針程序的時(shí)序性質(zhì)。此外，利用until算子描述的性質(zhì)在LTL 中可以輕松實(shí)現(xiàn)，但卻不能被PPTL 有效支持。文獻(xiàn)[65]將LTL 中的until 算子在有窮區(qū)間和無(wú)窮區(qū)間上重新定義并擴(kuò)充到PPTL中，提出一種新的統(tǒng)一時(shí)序邏輯UTL（unified temporal logic，UTL），該邏輯完美地結(jié)合了LTL 和PPTL的特性。

3）時(shí)序邏輯的判定問(wèn)題、模型檢測(cè)問(wèn)題和公理化問(wèn)題。對(duì)于時(shí)序邏輯而言，除了需要研究它的表達(dá)能力之外，還需要研究該邏輯的判定性、模型檢測(cè)和公理系統(tǒng)。時(shí)序邏輯的判定問(wèn)題即該邏輯的（可滿足）判定性及復(fù)雜度，該問(wèn)題在一種新的時(shí)序邏輯被提出時(shí)是必須考慮的。基于時(shí)序邏輯的模型檢測(cè)即自動(dòng)化驗(yàn)證系統(tǒng)模型是否滿足性質(zhì)規(guī)約的重要手段，設(shè)計(jì)高效的模型檢測(cè)算法與開(kāi)發(fā)相關(guān)支撐工具是人們追求的目標(biāo)。公理化問(wèn)題即基于該邏輯提出相應(yīng)的公理和推理規(guī)則，并保證該公理系統(tǒng)的可靠性和完備性。針對(duì)特殊的無(wú)窮狀態(tài)系統(tǒng)的模型檢測(cè)，結(jié)合定理證明技術(shù)能夠有效緩解系統(tǒng)狀態(tài)空間的膨脹。

6 結(jié)束語(yǔ)

形式化方法是驗(yàn)證安全攸關(guān)系統(tǒng)安全性與可靠性的重要手段，時(shí)序邏輯作為形式化規(guī)約語(yǔ)言，能夠描述軟硬件系統(tǒng)中基于時(shí)間變化的狀態(tài)遷移，是形式化驗(yàn)證的基礎(chǔ)。本文首先介紹基于離散時(shí)間模型的LTL，CTL 和CTL*，以及基于連續(xù)時(shí)間模型的ITL 和PTL，對(duì)它們之間的區(qū)別進(jìn)行闡述；然后介紹為了處理復(fù)雜計(jì)算特征(如隨機(jī)、實(shí)時(shí)、混成和開(kāi)放系統(tǒng)中的行為)而提出的各種時(shí)序邏輯；最后指出時(shí)序邏輯未來(lái)的研究方向。