時(shí)序邏輯的語(yǔ)法語(yǔ)義比較分析

黃 羿，馬新強(qiáng)，劉友緣，羅萬(wàn)成

(1.重慶文理學(xué)院機(jī)器視覺(jué)與智能信息系統(tǒng)重點(diǎn)實(shí)驗(yàn)室，重慶 永川 402160;

2.貴州大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，貴州 貴陽(yáng) 550025;3.貴州科學(xué)院，貴州 貴陽(yáng) 550001)

時(shí)序邏輯的語(yǔ)法語(yǔ)義比較分析

黃 羿1，2，3，馬新強(qiáng)1，2，3，劉友緣1，羅萬(wàn)成1

(1.重慶文理學(xué)院機(jī)器視覺(jué)與智能信息系統(tǒng)重點(diǎn)實(shí)驗(yàn)室，重慶 永川 402160;

2.貴州大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，貴州 貴陽(yáng) 550025;3.貴州科學(xué)院，貴州 貴陽(yáng) 550001)

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

語(yǔ)法;語(yǔ)義;時(shí)序邏輯;可靠性

目前，人們對(duì)信息和通信技術(shù)(ICT)系統(tǒng)的依賴在快速增長(zhǎng)，這些系統(tǒng)正變得越來(lái)越復(fù)雜.通過(guò)Internet和各種嵌入式系統(tǒng)(如智能卡、掌上電腦、移動(dòng)電話)等大規(guī)模的應(yīng)用，正迅速進(jìn)入人們的日常生活.人們對(duì)嵌入式系統(tǒng)的依賴使得這些系統(tǒng)的可靠運(yùn)行變得非常重要.這些系統(tǒng)如果在運(yùn)行過(guò)程中出現(xiàn)錯(cuò)誤有時(shí)會(huì)帶來(lái)金錢上的損失，有時(shí)甚至?xí)?lái)災(zāi)難.因此，ICT系統(tǒng)的可靠性在系統(tǒng)設(shè)計(jì)中是一個(gè)關(guān)鍵問(wèn)題，系統(tǒng)驗(yàn)證技術(shù)適用于在更可靠的方式下設(shè)計(jì)ICT系統(tǒng)［1］.

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

通過(guò)模型檢測(cè)技術(shù)驗(yàn)證系統(tǒng)的可靠性時(shí)，應(yīng)將反應(yīng)式系統(tǒng)的屬性進(jìn)行形式化描述，考慮到這類系統(tǒng)本身的特點(diǎn)，通常時(shí)序邏輯可作為這樣的一個(gè)形式化描述語(yǔ)言［3］.像在自然語(yǔ)言中的情形一樣，形式語(yǔ)言也有語(yǔ)義、語(yǔ)法和實(shí)例.語(yǔ)義涉及符號(hào)和符號(hào)表達(dá)式的涵義(當(dāng)給符號(hào)以某種解釋時(shí)).語(yǔ)法涉及符號(hào)表達(dá)式的形式結(jié)構(gòu)，不考慮任何對(duì)形式語(yǔ)言的解釋.形式語(yǔ)言的語(yǔ)義和語(yǔ)法既有聯(lián)系，又有區(qū)分［4］.在這里討論3種時(shí)序邏輯，分別是線性時(shí)序邏輯(LTL)、計(jì)算樹(shù)邏輯(CTL)、時(shí)序邏輯與行為邏輯的結(jié)合(TLA).

1 LTL的語(yǔ)法與語(yǔ)義

LTL即線性時(shí)序邏輯，用于對(duì)計(jì)算進(jìn)行推理.雖然沒(méi)有明說(shuō)，但隱含了整個(gè)系統(tǒng)是按著一個(gè)路徑向前發(fā)展演化的，就像一個(gè)只有一個(gè)線索的故事一樣.

1.1 LTL 的語(yǔ)法

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

(1)p是公式.

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

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

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

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

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

1.2 LTL 的語(yǔ)義

作者使用Kripke結(jié)構(gòu)這個(gè)概念來(lái)定義時(shí)序公式的含義.

定義2 Kripke結(jié)構(gòu)是一個(gè)四元組(S，I，R，Lable).其中

定義3 Kripke結(jié)構(gòu)中的路徑是一個(gè)無(wú)限狀態(tài)序列s0s1s2…，使得(si，si+1)∈R對(duì)?i，i≥0.

定義4 LTL語(yǔ)義

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

此外還引入4個(gè)輔助算子，F(xiàn)(將來(lái))、G(總是)、W(除非)、R(釋放).

圖1 LTL實(shí)例

1.3 實(shí)例

如圖1所示的Kripke結(jié)構(gòu)為:線性時(shí)序邏輯將時(shí)間看作線性的，即每個(gè)時(shí)刻系統(tǒng)只有一個(gè)可能的后繼狀態(tài)，因此，每個(gè)時(shí)刻只有一個(gè)唯一的可能的將來(lái).如果每個(gè)時(shí)刻可能有多個(gè)不同的將來(lái)，這樣LTL就不能處理，因此引入CTL.

2 CTL的語(yǔ)法與語(yǔ)義

CTL即計(jì)算樹(shù)邏輯，是分支時(shí)序邏輯的一種.整個(gè)系統(tǒng)的演化也是從某個(gè)起始狀態(tài)開(kāi)始的，但可以有不同的分支，即未來(lái)發(fā)展是不確定的.

2.1 CTL 的語(yǔ)法

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

(1)p是狀態(tài)公式.

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

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

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

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

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

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

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

2.2 CTL 的語(yǔ)義

CTL公式的解釋同樣使用Kripke結(jié)構(gòu)來(lái)定義，CTL中Kripke結(jié)構(gòu)的定義與LTL中Kripke定義相同.CTL中路徑的定義與LTL中路徑的定義相同.

定義6 CTL語(yǔ)義定義6與定義4對(duì)比可看出，CTL語(yǔ)義中將可滿足關(guān)系細(xì)分為狀態(tài)公式和路徑公式的可滿足關(guān)系，而LTL語(yǔ)義中的可滿足關(guān)系僅是CTL路徑公式的可滿足關(guān)系.因此，LTL可看作是CTL的特例.

2.3 實(shí)例如圖2所示實(shí)例的Kripke結(jié)構(gòu)為:

圖2 CTL實(shí)例

3 TLA語(yǔ)法與語(yǔ)義

TLA是時(shí)序邏輯與行為邏輯的結(jié)合，用來(lái)對(duì)并發(fā)和反應(yīng)式離散系統(tǒng)進(jìn)行形式化和推理.在TLA中，算法被表示為公式.

3.1 TLA 的語(yǔ)法

定義7

通過(guò)PLTL、CTL、TLA關(guān)于公式的定義不難看出，TLA中謂詞中引入了使能斷言這一概念，公式里引入了行為、狀態(tài)函數(shù)的概念.一個(gè)行為是由變量、下一變量、常量所形成的表達(dá)式，其值是布爾值.行為表示的是舊狀態(tài)和新?tīng)顟B(tài)之間的關(guān)系.狀態(tài)函數(shù)是由變量、常量形成的算術(shù)表達(dá)式.使能斷言是對(duì)每個(gè)行為 A，一個(gè)狀態(tài)s下Enabled A為真當(dāng)且僅當(dāng)起始于s下能執(zhí)行一個(gè)A步.如果一個(gè)行為A表示一個(gè)程序的原子操作，則Enabled A在能執(zhí)行這個(gè)操作的那些狀態(tài)下值為真.

3.2 TLA 的語(yǔ)義

3.3 實(shí)例

4 結(jié)語(yǔ)

通過(guò)LTL、CTL、TLA語(yǔ)法、語(yǔ)義的定義和實(shí)例可看出，這三者都用狀態(tài)代表每個(gè)時(shí)間點(diǎn)，而無(wú)限的狀態(tài)序列在LTL、CTL中用路徑來(lái)表示，而在TLA中不怎么使用路徑這一概念.在LTL、CTL語(yǔ)義中主要表述路徑、狀態(tài)與公式間的可推導(dǎo)關(guān)系，LTL中的推導(dǎo)關(guān)系主要反映在某個(gè)時(shí)間點(diǎn)上，系統(tǒng)是否具有某種性質(zhì);或系統(tǒng)是否一直具有某種性質(zhì)，等等.CTL中推導(dǎo)關(guān)系可反映每個(gè)時(shí)間點(diǎn)上系統(tǒng)滿足哪些性質(zhì);或者某種性質(zhì)是否在所有的分支路徑上可滿足還是只在某條路徑上滿足等.TLA則是時(shí)序邏輯和行為邏輯的結(jié)合，這種結(jié)合在TLA中的語(yǔ)法、語(yǔ)義的定義和推理規(guī)則中都有所反映.TLA的推理規(guī)則考慮了行為的影響，除此之外，推理規(guī)則還包含簡(jiǎn)單的時(shí)序邏輯推理規(guī)則.當(dāng)然，TLA也比LTL、CTL復(fù)雜.通過(guò)對(duì)3種時(shí)序邏輯的語(yǔ)法、語(yǔ)義及它們的異同進(jìn)行比較分析，為ICT的可靠性檢測(cè)分析提供了理論借鑒.

下一步的研究主要針對(duì)ICT系統(tǒng)的特點(diǎn)應(yīng)用時(shí)序邏輯形式化描述和分析.同時(shí)，針對(duì)智能信息的可靠性、可信性［5］及安全性分析中能否利用時(shí)序邏輯形式化方法進(jìn)行刻畫(huà)，都是值得研究的問(wèn)題.

致謝:感謝貴州大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院龍士工、王以松教授的傳道授業(yè)解惑.

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

［2］逄濤，段振華，劉曉芳.Verilog程序的命題投影時(shí)序邏輯符號(hào)模型檢測(cè)［J］.西安電子科技大學(xué)學(xué)報(bào)，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］陸鐘萬(wàn).面向計(jì)算機(jī)科學(xué)的數(shù)理邏輯(第2版)［M］.北京:科學(xué)出版社，2004:1-6.

［5］馬新強(qiáng)，黃羿.基于格的可信計(jì)算模型［J］.通信學(xué)報(bào)，2010，31(8A):105-110.

(責(zé)任編輯 穆 剛)

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

重慶市前沿與基礎(chǔ)研究項(xiàng)目(CSTC2013JCYJA40053);重慶市教委科學(xué)技術(shù)研究項(xiàng)目(KJ131218、KJ111217、KJ1401112);永川區(qū)自然科學(xué)基金(重點(diǎn))項(xiàng)目(YCSTC2013NB8001，YCSTC2013AD2002).

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