時序邏輯及其表達能力綜述

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

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

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

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

對于一種時序邏輯來說，一般從可滿足性、復雜性、表達性3 個方面展開研究[4]。可滿足性就是給定一個性質規約公式φ，是否存在一個結構M，該結構恰好是給定公式φ 的模型，或者判定模型M 是否滿足公式φ；復雜性就是研究邏輯公式可滿足性的復雜度問題；表達性是研究時序邏輯的表達能力，該邏輯公式能夠描述哪一種類型的性質。本文著重研究時序邏輯的表達能力問題，介紹各種時序邏輯和分析它們適合對哪些系統進行性質規約，以及不同時序邏輯在表達能力上的優劣。

1 時序邏輯

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

下面簡要介紹時序邏輯屬性、屬性的可描述性以及表達能力[6]的形式化定義。

定義1 （屬性）在一個無窮狀態序列δ：δ0，δ1，δ2，…（δ∈Sω）的集合Sω上定義屬性p（property，也稱之為性質）。一個屬性p?Sω是所有滿足該屬性的無窮狀態序列δ 的集合，也就是說一個無窮狀態序列δ 滿足屬性p 等價于該序列δ 屬于p 所表示的集合，記作δ｜=p?δ∈p。

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

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

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

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

2 基于離散時間模型的時序邏輯

本節介紹基于離散時間模型的時序邏輯，它們的語義被解釋在孤立離散的點上，主要包括LTL，CTL 和CTL*，并對它們之間的區別進行詳細分析比較。

2.1 線性時序邏輯LTL

LTL 由Manna 和Pnueli 提出，是一種非常重要的時序邏輯，可以用來描述并發分布式系統的屬性，在模型檢測中得到廣泛使用。LTL 將時間序列設想成一個線性序列δ：s0，s1，s2，…，這是一種經典的時間模型。狀態之間按照時間參數嚴格排序，在狀態序列上解釋其真值，并且其真值隨時間變化而變化，這也是時序邏輯與經典邏輯的主要區別之處。

LTL 采用的時間結構是線性、離散的，其語義模型是通過Kripke 三元組ML=＜S，R，L＞來定義的，其中S 是狀態集合，R?S×S 是符合完全性約束的變遷關系（即對于任意的狀態s∈S，存在狀態s'∈S滿足（s，s'）∈R，L∶S→2AP是標記函數，用于標記某個狀態上所有滿足的原子命題集合。

以選舉算法為例，對如何使用LTL 描述領導人選舉算法需要滿足的性質進行闡述。領導人選舉算法是分布系統中一類非常重要的算法，目的是在多個服務器中選出一個特殊的節點作為領導人，可以簡化服務器之間的協作，有助于容錯和節省資源。我們用elected 表示選舉發生，num_leader 表示領導人數量，one_leader 表示成功選舉出領導人。

性質1：選舉結束后，最終會選出一位領導人：◇（num_leader＞0）。

性質2：選舉結束后，至多有一位領導人當選：□?（num_leader＞1）。

性質3：當某個節點被選為領導人之后，將永遠成為領導人：∧i□（electedi→one_leader）。

定理1 LTL 的表達能力與一階謂詞邏輯等價，不能表達ω 正則性質[7]。

該定理表明雖然LTL 與一階謂詞邏輯的表達能力等價，但對于兩者的可滿足性的復雜度卻不相同。對于一階謂詞邏輯來說，它的可滿足性問題的解決難度是非初等的，也就是說它的復雜度上界是無限增長的，而對于LTL 來說是PSPACE-完全的[8]，這也是LTL 能夠得到廣泛應用于程序驗證、程序綜合以及人工智能等領域的一個重要理論支撐[9]。

在顯式模型檢測中，通常是將軟硬件系統用形式化語言建模成模型M，同時利用LTL 公式將系統的屬性表示為φ，其核心是判斷系統模型的自動機AM與時序邏輯公式φ取反得到的等價自動機Aφ做交運算后的自動機AP是否為空。可以推斷出LTL是可以用自動機來表示的，但研究表明LTL 與自動機之間的轉換并不是雙向的，LTL 的表達能力弱于自動機[10]。

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

2.2 計算樹邏輯CTL

CTL[14]的語義模型與LTL 類似，都是通過Kripke 結構來定義的。不同的是，由狀態組成的序列∏∶s0，s1，s2，…，sk，…的路徑中，從模型的初始狀態作為根節點，對于k≥0，都有（sk，sk+1）∈R，模型的未來時刻存在著多種不確定狀態。因此，把所有路徑展開就形成了樹狀的拓撲結構，這也是被稱為計算樹的原因，又因為每個節點存在分支，所以CTL 也被稱之為分支時序邏輯（branching temporal logic，BTL）。

CTL 的語義模型是通過Kripke 三元組M=＜S，R，L＞來定義的，其中S 是狀態集合，R?S×S 是符合完全性約束的變遷關系（即對于任意的狀態s∈S,存在狀態s'∈S 滿足 （s，s'）∈R），L∶S→2AP是標記函數，用于標記某個狀態上所有滿足的原子命題集合。

為了更好地介紹如何使用CTL 描述相關性質，以多個進程訪問共享內存為例進行說明。假設有兩個獨立進程proc1和proc2訪問同一片共享內存，并且要避免它們同時訪問，一旦兩個進程同時訪問臨界區，那么就會造成程序崩潰。“entering”狀態表示當前某個進程請求訪問共享內存，“critical”狀態表示當前有某個進程正在訪問共享內存。

性質4：兩個進程不能同時訪問共享內存，即兩個進程間存在互斥性（mutual exclusion）。

2.3 計算樹邏輯CTL*

針對LTL 與CTL 在在處理計算分支上的不同，Clarke 對CTL 的語法和語義作適當的擴充，設計了兼容上述兩種時序邏輯算子的語言CTL*[15]，該語言融合兩種時序邏輯于一種語言之中，同時還克服了時序邏輯公式的二義性解釋（時序邏輯公式既可以解釋成線性的，也可以解釋成分支的）。

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

一個邏輯公式的可滿足性問題也稱為模型檢測問題，對于CTL* 有如下結論：

定理2 ①CTL*的模型檢測問題是多項式時間完備的；②CTL*的模型檢測問題具有NP 難度和co-NP 難度[16]。

CTL*是CTL 和LTL 的超集，表達能力雖然得到了加強，但仍然存在著兩個主要缺陷。首先CTL*公式描述的是系統從某一狀態s 開始后系統的所有可能發生的行為，并不關注系統是以一種什么樣的方式到達狀態s 的，換句話說CTL*公式不能描述狀態s 之前的系統行為。另外CTL*的缺陷是只能定性地描述系統建立可能發生的行為，但卻不能精確地描述該行為發生的確切時間，該類性質對于并發系統中區間相關性質尤為重要[17]。

2.4 LTL 和CTL 的比較

定義4 LTL 公式和CTL 公式的等價性。

如果一個LTL 公式φ 和一個CTL 公式? 是等價的，記作φ≡?，那么對于任意遷移系統（transition system，TS）上的原子命題來說，當且僅當下面的式子成立

從公式形式上來看，在LTL 公式上添加全稱路徑量詞得到CTL 公式，這是因為LTL 公式默認包含量詞。

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

對于LTL 公式◇□a 來說是滿足圖1 中狀態遷移系統的，初始狀態s0滿足公式◇□a，從s0出發最終會停留狀態s0或者s2，是滿足該公式的語義“從某一狀態開始a 永遠為真”。然而對于CTL 公式?◇?□a 來說不滿足圖2 中的狀態遷移系統，該公式在狀態s0處不成立，記作s0ω｜≠◇?□a，這是因為路徑s0*，s1，s2ω經過了一個不滿足原子命題a 的狀態s1，其中s0*表示由狀態s0構成的有窮序列，s2ω表示由狀態s2構成的無窮序列。

圖1 LTL 公式◇□a 的狀態遷移系統Fig.1 The state transition system of LTL ◇□a

圖2 CTL 公式?◇?□a 的計算樹展開形式Fig.2 The expansion form of computation tree of Formula CTL formula ?◇?□a

另外，許多學者也對LTL 和CTL 的區別進行過系統研究。這兩種邏輯使用同一套符號體系，造成語義上的模糊，關于這兩種邏輯孰優孰劣，學者們有著不同的爭論。兩種時序邏輯的公式是一樣的，關鍵在于語義的區別。LTL 以路徑作為命題的論斷對象，而CTL 以狀態作為命題的論斷對象。圖靈獎得主Lamport 的結論是[18]：LTL 和CTL 一般來說是不能相比的，但在證明并發程序的某些性質時LTL 要優于CTL，而在證明非確定性程序的某些性質時CTL 要優于LTL。Lamport 和Emerson 等曾討論過LTL 和CTL 的本質區別，及其用于程序驗證時功能上的不同。那么它們的不同之處在于語義上的區別，主要體現在下列事實上。

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

其中，→p 的含義表示“有時p 成立”。該定理表明在不同語義模型下，LTL 和CTL 是不等價的，針對這兩種不同時序邏輯的表達能力問題，Lamport定義了強等價性。

定義5 給定時序結構M=（S，X，D），其中S 為非空狀態集，X 是非空路徑集，D 是一個映射。如果對于每條路徑a∈X 來說都有（L，M，a）｜=p 成立，則稱時序公式p 是在線性語義下M 為真，記作（L，M）→p。類似的，如果對于每個狀態t∈S 都有（B，M，t）→p成立，則稱時序公式p 在分支意義下M 為真。其中L 表示線性語義，B 表示分支語義。

定義6 令p 和q 表示兩個時序公式，C 是由一組時序結構組成的類，如果對C 中的每個時序結構，有如下公式成立

式中：I 和J 是兩個語義解釋，可以是線性語義L 或分支語義B，則稱時序公式p 和q 分別在語義解釋I 和J 下，相對于結構類C 是強等價的，記作p=q（I，J，C）。

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

定理4 存在這樣的結構類C，使得CTL 公式◇p 不強等價于任何LTL 公式。

定理5 存在這樣的結構類C，使得LTL 公式→◇p 不強等價于任何CTL 公式。

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

對于這兩種時序邏輯的比較，從邏輯的角度看這兩種語言各有長短。實際應用于模型檢測中，普遍認為對于安全屬性如公平性和活性的描述，使用LTL 表示更具有優勢。但是從計算的角度來看，實現CTL 模型檢測相對簡單，LTL 模型檢測問題是PSPACE-完全的，而CTL 模型檢測時間是線性或多項式的。從模型檢測的發展歷程來看，在模型檢測早期，以SMV 為代表的CTL 模型檢測器對硬件、數字電路驗證占主導地位。但對于刻畫系統性質的規約，使用LTL 更加簡潔且容易理解，再加上LTL 模型檢測算法有巨大進步，Cadence SMV 和SPIN 這類LTL 模型檢測工具得到廣泛應用。

對于LTL，CTL 的模型檢測，由于兩者的語義解釋不同造成模型檢測方法的不同。在對LTL 公式φ進行模型檢測時，模型檢測工具會對φ 取反得到有限自動機A?φ，然后與系統模型的有限自動機AM相乘，驗證兩個自動機的交集是否為空，若不為空，則表示設計中有不滿足屬性的行為。而對CTL 公式進行模型檢測是以Kripke 結構圖的所有狀態為根節點進行搜索，如果存在不滿足屬性的模型，即得到違反屬性的反例路徑。通過對比這兩種不同公式的模型檢測方法，可以得出LTL 模型檢測可以快速完成對路徑上的狀態搜索，所需要的狀態數比CTL 模型檢測更少。

3 連續時間模型的時序邏輯

本節介紹基于連續時間模型的時序邏輯，包括ITL 和PTL，對兩種邏輯系統進行分析比較，指出它們的適用范圍。

3.1 區間時序邏輯ITL

LTL，CTL 公式的語義在獨立的點上被解釋，一個點代表一個狀態，點之間的關系就代表時序之間的關系，這樣的時序關系無法描述正則表達式所表達的性質。由于基于連續時間模型的時序邏輯的表達能力較弱，使得對一些性質的驗證無法進行。因此很多關于LTL 的擴展已經被提出，如Kozen 提出了μ 演算[12]，Vardi 提出了ETL[13]。盡管這些時序邏輯具備完全正則語言能力，但仍難以表達一些狀態敏感的性質，如原子命題p 在某個具體狀態或具體區間上成立，此外如順序、循環等結構難以表達。

與基于點語義的LTL 不同,系統的時間特征行為可能會出現在一系列時間區間上，那么就需要使用一些連續時間區間, 稱之為區間時間模型。Moszkowski 在其博士論文中提出了基于區間語義的ITL[20]，可用于描述區間中的狀態及其時序關系的性質。

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

由于ITL 定義在有窮區間范圍內, 主要包括chop，next 以及投影符號proj 等時序操作符，因此使得ITL 比LTL 具有更強的表達能力。作為時序邏輯的一個重要分支，現在已經擴展應用在并發軟件系統的規約和驗證，但ITL 的缺陷在于只能應用于有窮區間。

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

3.2 投影時序邏輯PTL

由于ITL 是定義在有窮區間上的時序邏輯，所以該邏輯的缺陷是無法描述系統中的無窮行為。針對ITL 存在的問題，西安電子科技大學段振華等提出了投影時序邏輯PTL[21]，對ITL 進行擴充到無窮區間范圍內，并引入一個全新的投影操作結構（P1，…，Pm）prj Q，從而得到一種描述有窮、無窮模型和時段的邏輯系統。

通過引入投影操作符號（P1，…，Pm）prj Q 將ITL推廣到無窮區間范圍，與原有的投影結構P prj Q相比，新的投影操作更加靈活易用。PTL 相比ITL 的優勢在于：由于擴充了投影算子prj，PTL 可以應用于無窮區間，允許用不同的時間粒度來描述計算的進程，由此可定義順序、循環等操作。PTL 相比ITL更適合描述并發軟件[22-23]。

定理7 PPTL 具備完全正則表達能力，能夠對順序、并行、區間相關以及周期重復的性質進行描述[24-25]。

PTL 的一個命題子集也就是命題投影時序邏輯PPTL（propositional PTL，PPTL)的表達能力等價于Büchi 自動機[26]，因而證明其具有完全正則表達能力。PPTL 不僅能夠表達離散時間模型上的時序性質，還可以表達如區間相關性質以及周期性重復的閉包性質，主要使用區間長度算子len（n），分割算子chop，chop star 和投影算子prj 來實現，具體性質如下[4]：

1）區間相關的性質。例如“命題p 在時間長度為n 的區間上成立”可以表示為p∧len（n）；“命題p在第5 個和第10 個時間單元內成立”可以表示為len（5）；◇p∧len（5）。

2）周期重復的性質。例如“命題p 在偶數狀態上成立”可以表示為p∧（○2（p∧ε））*。因此對于驗證實時系統的性質不僅局限于傳統的安全性和活性，即描述性質“事件p 在將來會成立”，還可以通過時間間隔描述對于時間有嚴格要求的性質，例如性質“事件p 將在一段時間間隔內發生”。

3）順序、循環、迭代等結構。PPTL 中的分割算子chop 和chop star 可以對該類結構方便地進行描述。

總的來說，相比較其它時序邏輯如LTL，CTL 和ITL，PTL 的表達能力是完全正則的，等價于Büchi自動機，能夠表達區間相關的性質以及周期性重復的閉包性質，可描述并發情況以及實時性相關性質。雖然該邏輯的表達能力得到增強，但不可避免地帶來更高的模型檢測復雜度，減少系統狀態空間的方法如偏序規約、限界模型檢測以及組合驗證等技術被引入到PPTL 模型檢測中[28-29]。

4 處理復雜計算特征的時序邏輯

為了處理復雜的計算特征，如實時、隨機、混成、開放系統中的行為，許多時序邏輯被相繼提出。例如:為了描述隨機系統的高度不確定性，通過在計算樹邏輯中引入概率建立了概率計算樹邏輯以及連續隨機邏輯；為了描述實時系統中關于時間敏感的性質，提出了時段演算等一系列邏輯語言；為了處理混成系統中同時包含離散變量和連續變量的復雜行為，提出了微分動態邏輯；為了處理開放系統中多進程間的任意交互以及系統內部與外界環境的交互，計算樹邏輯被擴充為交替時序邏輯，下面將對這些時序邏輯變體及其適合描述哪些性質進行概述。

4.1 面向隨機系統的時序邏輯

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

PCTL 適用于描述隨機不確定系統，能夠表達定量性質。這種能力在隨機不確定性系統中是非常實用的，在形式化驗證中有時并不要求系統性質的絕對正確性，而是保證系統性質在一定程度上的相對正確性。例如，在網絡通信過程中經常會發生數據傳輸失敗的情況，因此需要對數據進行重新發送。對如何使用PCTL 表達協議所期望的功能正確性和協議性能為例進行說明。在網絡通信過程中，組件A 和B 在發送消息時會有一定幾率發送失敗，如果發送失敗則會接著發送直到消息發送成功。

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

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

P＞0.9［F＜100 “enabled”］：在經過100 步遷移之后，消息全部發送成功達到穩定狀態的概率大于0.9。

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

目前PCTL 和CSL 已經在概率模型檢測器PRISM 中得到支持和應用，被用于規約概率系統的期望屬性。此外PRISM 通過擴展回報，一個形如的r：S×S→R≥0 回報結構將非負數的回報值添加到狀態遷移過程中，可用于分析與回報期望值相關的屬性，這是通過擴充R 算子實現的。以分布式系統中的自穩定算法為例進行說明，在分布式環境下往往要求系統具有自穩定性，這就要求自穩定算法在沒有外界干預下，經過有限次步驟后從一個雜亂無章的初始狀態到達一個穩定狀態。對于自穩定算法關于時間消耗的屬性，通過一個簡單的回報結構time將系統中每一步的狀態遷移的回報值設定為1，有如下公式

4.2 面向實時系統的時序邏輯

實時系統是一種能夠在有限時間范圍內對來自外部輸入等做出快速響應的系統，例如控制系統、監測系統、通信系統等。實時系統的部件之間具有并發性，運行通常并不終止，對規定動作的進行和完成時間也有很高的要求。

時段演算適用于對實時系統的實時需求進行刻畫[34]，不僅能夠像其它實時邏輯描述刻度時間性質和時間邊界特性，還可以描述一段時間范圍內性質的累積。以燃氣燃燒器為例，對如何使用時段演算形式化刻畫離散狀態系統的實時特性進行說明。我們希望控制煤氣燃燒器的點火機制和關閉機制，把煤氣泄漏控制在安全閾值之內。需求說明為：在煤氣灶使用期間如果對其連續觀察超過60 s，那么煤氣泄漏的時間不能超過觀測時間的1/20。引入b和e 分別表示觀測的起始、截止時間，只有當煤氣被釋放且沒有火焰出現的狀態被稱為煤氣泄漏，用布爾函數Leak（t）來表示煤氣的泄漏狀態，可表示Leak（t）?Gas（t）∧?Flame（t）為,那么該安全需求形式化表示為

設計原則2：任何兩個泄露時段的時間間隔不能少于30 s。

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

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

4.3 面向混成系統的時序邏輯

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

由于混成系統的并發性和時間屬性使得混成系統的狀態空間極為龐大，而且系統中的狀態可達性不可判定使得基于模型檢測的混成系統形式化驗證難以開展。André Platzerti[42]提出了一類描述混成系統屬性的規約語言：微分動態邏輯（differential dynamic logic，DDL）家族，該類邏輯是離散一階動態邏輯的擴展，DDL 在離散一階動態邏輯的基礎上引入了描述連續狀態變化的結構，利用混成程序（hybrid program）建模混成系統中狀態以及狀態變遷，具體為使用離散跳躍集表示混成系統中的離散變遷，使用微分方程組描述系統動態行為中的連續變遷，然后通過控制結構操作符（U，*，∶）將系統的離散和連續行為組合在一起。

DDL 適用于描述混成系統中離散變遷與連續動態行為特征[43]。這表明DDL 可用于描述混成系統中連續變化的物理層和離散變化的控制層之間的相互交互過程，并且相關推理規則已經被提出，能對混成系統的行為特性進行推理驗證。基于DDL對混成系統的形式化驗證主要是采用定理證明方法，同時結合了組合驗證思想，在驗證過程中對待驗證屬性公式進行逐步分解然后獨立驗證，能夠明顯克服基于混成自動機、混成Petri 網驗證混成系統時面臨的狀態爆炸問題，提高驗證效率并能夠保持系統模型特征與變遷結構。

DDL 具有良好的擴展性，基于DDL 的定理證明是在給定的公理和推理規則上進行，為了使DDL具有更強大的證明能力，可以對DDL 的公理系統和推理規則進行擴充。目前在DDL 基礎上根據不同的應用情況以及不同的操作模型衍生出許多變體，包括微分代數動態邏輯 （differential-algebraic dynamic logic，DAL），微分時序動態邏輯（differential temporal dynamic logic，dTL），微分代數時序動態邏輯（differential-algebraic temporal dynamic logic，DATL）以及量化微分動態邏輯（quantified differential dynamic logic，QdL）[44-46]。DDL 缺乏描述物理環境中連續動態行為特性的有效方法，同時存在微分方程不可解的情況，針對該問題在一階動態邏輯的基礎上提出了DAL，使用微分不變量技術進行推理驗證而不必求解微分方程。為了驗證混成系統中的時序屬性，將DDL，DAL 分別與時序邏輯相結合得到dTL 和DATL，DATL 將動態邏輯的模態操作符和時序邏輯的時序操作符完美結合在一起，得到形如的邏輯公式，可以同時描述系統的時序行為和非時序行為。為了處理分布式混成系統的形式化驗證，基于一階動態邏輯和量化的微分方程相結合得到QdL。DDL家族之間的關系可以用圖3 來說明。

圖3 微分動態邏輯家族示意圖Fig.3 Schematic diagram of differential dynamic logic family

4.4 面向開放系統的時序邏輯

封閉系統的行為由當前系統所處的狀態決定，與外部環境無關，針對封閉系統的模型檢測主要采用LTL 或CTL 來描述系統的性質。開放系統的行為不僅由系統當前所處狀態決定，同時也受到外部環境的約束[47]。與封閉系統相比，開放系統的外部環境是不確定的，開放系統中不同組件之間的交互會導致難以預測的情況發生，如可觀測性以及可控性等。因此，開放系統的形式化驗證需要將外部環境的各種不確定情況納入考慮范圍內[48]。Alur 提出了交替時序邏輯（alternating-time temporal logic，ATL）[49]，該邏輯描述的是開放系統與外界環境之間的交互以及內部組件之間的合作與競爭關系，將系統中的各組件之間的交互最終到達的穩定狀態規約為開放系統與外界環境之間的博弈結果，所以又被稱為博弈邏輯。

ATL 適用于描述開放系統與外界環境之間的交互以及內部組件之間的合作與競爭關系[50]。這表明對于系統行為同時受到內部結構和外部環境輸入的開放系統，系統不同組件之間交互后最終達到的狀態，可以使用ATL 規約為開放系統與外部環境之間的博弈。以幾個簡單的例子介紹如何使用ATL來描述開放系統中各個主體之間的合謀與對抗行為，來說明ATL 對于開放系統的表達能力。假設存在參與者集合∑＝｛a，b，c｝，不同的參與者存在著策略使得命題p 成立，同時不同參與者之間存在著合謀與競爭，有如下ATL 公式：

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

《b，c》□p：針對參與者a,無論參與者b 和c 如何合謀，永遠不能避免系統最終達到一個狀態使得命題p 成立。

《a，b》○（p∧?《c》□p）：針對參與者c，參與者a和b 合謀能夠使得下一狀態命題p 成立，并且從下一狀態開始參與者c 永遠不能使命題p 成立。

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

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

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

5 時序邏輯未來的研究方向

從時序邏輯的發展趨勢來看，今后一段時間時序邏輯的研究工作包括以下幾個方面：

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

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

3）時序邏輯的判定問題、模型檢測問題和公理化問題。對于時序邏輯而言，除了需要研究它的表達能力之外，還需要研究該邏輯的判定性、模型檢測和公理系統。時序邏輯的判定問題即該邏輯的（可滿足）判定性及復雜度，該問題在一種新的時序邏輯被提出時是必須考慮的。基于時序邏輯的模型檢測即自動化驗證系統模型是否滿足性質規約的重要手段，設計高效的模型檢測算法與開發相關支撐工具是人們追求的目標。公理化問題即基于該邏輯提出相應的公理和推理規則，并保證該公理系統的可靠性和完備性。針對特殊的無窮狀態系統的模型檢測，結合定理證明技術能夠有效緩解系統狀態空間的膨脹。

6 結束語

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