時序邏輯的語法語義比較分析

黃 羿，馬新強，劉友緣，羅萬成

(1.重慶文理學院機器視覺與智能信息系統重點實驗室，重慶 永川 402160;

2.貴州大學計算機科學與技術學院，貴州 貴陽 550025;3.貴州科學院，貴州 貴陽 550001)

時序邏輯的語法語義比較分析

黃 羿1，2，3，馬新強1，2，3，劉友緣1，羅萬成1

(1.重慶文理學院機器視覺與智能信息系統重點實驗室，重慶 永川 402160;

2.貴州大學計算機科學與技術學院，貴州 貴陽 550025;3.貴州科學院，貴州 貴陽 550001)

隨著信息技術的快速發展，信息和通信技術(ICT)系統被廣泛使用，因而其可靠性非常重要.本文采用時序邏輯的形式化方法對ICT系統進行可靠性檢測討論，主要從3種時序邏輯的語法、語義及它們的異同進行比較分析，為ICT的可靠性檢測分析提供了理論借鑒.

語法;語義;時序邏輯;可靠性

目前，人們對信息和通信技術(ICT)系統的依賴在快速增長，這些系統正變得越來越復雜.通過Internet和各種嵌入式系統(如智能卡、掌上電腦、移動電話)等大規模的應用，正迅速進入人們的日常生活.人們對嵌入式系統的依賴使得這些系統的可靠運行變得非常重要.這些系統如果在運行過程中出現錯誤有時會帶來金錢上的損失，有時甚至會帶來災難.因此，ICT系統的可靠性在系統設計中是一個關鍵問題，系統驗證技術適用于在更可靠的方式下設計ICT系統［1］.

利用系統驗證方式來構建或設計的軟件應具有某些特性，而要驗證的特性可以是一些基本的屬性，屬性大多是從系統規范得到的.系統規范描述了系統要做的和不做的，從而構成任何驗證活動的基礎.一旦系統不滿足某個規范的屬性則一個缺陷被發現了.一旦系統滿足所有的屬性就被認為是正確的.在本文中討論被稱為模型檢測的驗證技術.在這方面也有相關研究，例如:為了保證以Verilog硬件描述語言設計的片上系統的正確性，提出了Verilog程序的符號模型檢測方法.該方法依據形式化操作語義將 Verilog程序建模為有限狀態機，將設計規范用命題投影時序邏輯公式描述，并采用命題投影時序邏輯符號模型檢測工具對程序進行驗證，從而證明片上系統滿足設計規范［2］.

通過模型檢測技術驗證系統的可靠性時，應將反應式系統的屬性進行形式化描述，考慮到這類系統本身的特點，通常時序邏輯可作為這樣的一個形式化描述語言［3］.像在自然語言中的情形一樣，形式語言也有語義、語法和實例.語義涉及符號和符號表達式的涵義(當給符號以某種解釋時).語法涉及符號表達式的形式結構，不考慮任何對形式語言的解釋.形式語言的語義和語法既有聯系，又有區分［4］.在這里討論3種時序邏輯，分別是線性時序邏輯(LTL)、計算樹邏輯(CTL)、時序邏輯與行為邏輯的結合(TLA).

1 LTL的語法與語義

LTL即線性時序邏輯，用于對計算進行推理.雖然沒有明說，但隱含了整個系統是按著一個路徑向前發展演化的，就像一個只有一個線索的故事一樣.

1.1 LTL 的語法

定義1 令p是原子命題，LTL中的公式由有限次使用以下規則(1)～(5)形成:

(1)p是公式.

(2)如果Φ是公式，則﹁Φ是公式.

(3)如果Φ和Ψ是公式，則Φ∨Ψ是公式.

(4)如果Φ是公式，則ΧΦ是公式.

(5)如果Φ和Ψ是公式，則Φ∪Ψ是公式.

在定義1中可看出，規則(1)、(2)、(3)與命題邏輯中公式的形成規則相同，但和命題邏輯公式相比LTL公式引入了時序運算符Χ和∪.ΧΦ表示如果Φ在下個時刻成立，則ΧΦ在當前時刻成立.Φ∪Ψ表示在將來某個時刻Ψ成立，Φ在該時刻之前成立.

1.2 LTL 的語義

作者使用Kripke結構這個概念來定義時序公式的含義.

定義2 Kripke結構是一個四元組(S，I，R，Lable).其中

定義3 Kripke結構中的路徑是一個無限狀態序列s0s1s2…，使得(si，si+1)∈R對?i，i≥0.

定義4 LTL語義

令p∈AP是原子命題，σ是路徑，Φ和Ψ是TLT公式，可滿足關系|=定義為:

此外還引入4個輔助算子，F(將來)、G(總是)、W(除非)、R(釋放).

圖1 LTL實例

1.3 實例

如圖1所示的Kripke結構為:線性時序邏輯將時間看作線性的，即每個時刻系統只有一個可能的后繼狀態，因此，每個時刻只有一個唯一的可能的將來.如果每個時刻可能有多個不同的將來，這樣LTL就不能處理，因此引入CTL.

2 CTL的語法與語義

CTL即計算樹邏輯，是分支時序邏輯的一種.整個系統的演化也是從某個起始狀態開始的，但可以有不同的分支，即未來發展是不確定的.

2.1 CTL 的語法

定義5 令p是原子命題，CTL中的公式分為狀態公式和路徑公式.狀態公式由有限次使用以下規則形成:

(1)p是狀態公式.

(2)如果Φ是狀態公式，則﹁Φ是狀態公式.

(3)如果Φ和Ψ是狀態公式，則Φ∨Ψ是狀態公式.

(4)如果φ是路徑公式，則Εφ和Αφ是狀態公式.

路徑公式由有限次使用以下規則形成:

(1)如果Φ是狀態公式，則ΧΦ是路徑公式.

(2)如果Φ和Ψ是狀態公式，則Φ∪Ψ是路徑公式.

從定義1、2中可以看出，CTL對LTL中的公式區分為狀態公式和路徑公式.狀態公式表示狀態的屬性，路徑公式表示路徑的屬性.運算符Χ和∪的含義與PLTL相同，但在CTL中是路徑運算符號.加上路徑量詞Ε(對某條路徑)或Α(對所有路徑)前綴，路徑公式轉換為狀態公式.

2.2 CTL 的語義

CTL公式的解釋同樣使用Kripke結構來定義，CTL中Kripke結構的定義與LTL中Kripke定義相同.CTL中路徑的定義與LTL中路徑的定義相同.

定義6 CTL語義定義6與定義4對比可看出，CTL語義中將可滿足關系細分為狀態公式和路徑公式的可滿足關系，而LTL語義中的可滿足關系僅是CTL路徑公式的可滿足關系.因此，LTL可看作是CTL的特例.

2.3 實例如圖2所示實例的Kripke結構為:

圖2 CTL實例

3 TLA語法與語義

TLA是時序邏輯與行為邏輯的結合，用來對并發和反應式離散系統進行形式化和推理.在TLA中，算法被表示為公式.

3.1 TLA 的語法

定義7

通過PLTL、CTL、TLA關于公式的定義不難看出，TLA中謂詞中引入了使能斷言這一概念，公式里引入了行為、狀態函數的概念.一個行為是由變量、下一變量、常量所形成的表達式，其值是布爾值.行為表示的是舊狀態和新狀態之間的關系.狀態函數是由變量、常量形成的算術表達式.使能斷言是對每個行為 A，一個狀態s下Enabled A為真當且僅當起始于s下能執行一個A步.如果一個行為A表示一個程序的原子操作，則Enabled A在能執行這個操作的那些狀態下值為真.

3.2 TLA 的語義

3.3 實例

4 結語

通過LTL、CTL、TLA語法、語義的定義和實例可看出，這三者都用狀態代表每個時間點，而無限的狀態序列在LTL、CTL中用路徑來表示，而在TLA中不怎么使用路徑這一概念.在LTL、CTL語義中主要表述路徑、狀態與公式間的可推導關系，LTL中的推導關系主要反映在某個時間點上，系統是否具有某種性質;或系統是否一直具有某種性質，等等.CTL中推導關系可反映每個時間點上系統滿足哪些性質;或者某種性質是否在所有的分支路徑上可滿足還是只在某條路徑上滿足等.TLA則是時序邏輯和行為邏輯的結合，這種結合在TLA中的語法、語義的定義和推理規則中都有所反映.TLA的推理規則考慮了行為的影響，除此之外，推理規則還包含簡單的時序邏輯推理規則.當然，TLA也比LTL、CTL復雜.通過對3種時序邏輯的語法、語義及它們的異同進行比較分析，為ICT的可靠性檢測分析提供了理論借鑒.

下一步的研究主要針對ICT系統的特點應用時序邏輯形式化描述和分析.同時，針對智能信息的可靠性、可信性［5］及安全性分析中能否利用時序邏輯形式化方法進行刻畫，都是值得研究的問題.

致謝:感謝貴州大學計算機科學與技術學院龍士工、王以松教授的傳道授業解惑.

［1］Katoen JP.Formalmethods and tools group，principles ofmodel checking［M］.2005:15-50.

［2］逄濤，段振華，劉曉芳.Verilog程序的命題投影時序邏輯符號模型檢測［J］.西安電子科技大學學報，2014，41(2):98-104.

［3］Lamport L.The temporal logic of actions［J］.ACM Transactions on Programming Languages and Systems 1993，11(1):1-52.

［4］陸鐘萬.面向計算機科學的數理邏輯(第2版)［M］.北京:科學出版社，2004:1-6.

［5］馬新強，黃羿.基于格的可信計算模型［J］.通信學報，2010，31(8A):105-110.

(責任編輯 穆 剛)

Com parative analysis of tem poral logic syntax and semantics

HUANG Yi，MA Xinqiang，LIU Youyuan，LUOWancheng

(1.Key Laboratory of Machine Vision and Intelligent Information System，Chongqing University of Arts and Sciences，Yongchuan Chongqing 402160，China;2.Schoolof Computer Science and Technology，Guizhou University，Guiyang Guizhou 550025，China;3.Guizhou Academ y of Science，Guiyang Guizhou 550001，China)

With the rapid development of information technology，information and communication technology(ICT)systems are widely used in kinds of fields.Therefore，its reliability is of great importance.In this paper，the formalmethod of temporal logic is employed for reliability testing on ICT system.The syntax and semantics of three temporal logics，aswell as their similarities and differences are compared and analyzed，to provide a theoretical reference for reliability testing on ICT system.

syntax;semantics;temporal logic;reliability

TP391

A

1673-8004(2014)05-0116-05

2014-05-29

重慶市前沿與基礎研究項目(CSTC2013JCYJA40053);重慶市教委科學技術研究項目(KJ131218、KJ111217、KJ1401112);永川區自然科學基金(重點)項目(YCSTC2013NB8001，YCSTC2013AD2002).

黃羿(1976-)，女，重慶人，貴州大學博士研究生，副教授，主要從事邏輯程序、人工智能方面的研究.