模態(tài)邏輯和時態(tài)邏輯

1、模態(tài)邏輯和時態(tài)邏輯-219 -.第10章模態(tài)邏輯和時態(tài)邏輯在本章中，我們研究模態(tài)邏輯和時態(tài)邏輯。10.1 模態(tài)邏輯(Modal Logic)模態(tài)邏輯涉及到必然性和可能性概念。一階模態(tài)邏輯語言 Lml由一階謂詞演算L加上兩個新的算子L(或必然算子)和(或可能算子)得到,更精確地說Lml由L加上下列子句組成：如果A是L的wff(合式公 式)，則LA和MA也是 wff。他們的語義解釋為若A在某些可能世界中為真則M真，如果A在每一個可能世界為真則LA為真。更精確形式定義為：定義1 一個模態(tài)框架(Model Frame) M是一個四元組v W, D, R, F ，其中 W是一個(可能世界的)非空集合；

2、D是一個個體非空域； R是W上的一個二元可達性關系； F是一個映射，它賦給每一個由一個n (n 0)元函數(shù)符號f和n個 W的元素w所組成的對(f, w)，以 一個Dn到D的函數(shù)，以及賦給每一個由n (n 0)元關系符號r和n個 W的元素w的對(r, w)以2Dn 一個元 素。在這樣一個模態(tài)框架中 Lml的解釋不同于謂詞演算中的演算 ，這里域 W起一個關鍵作用。但是解釋仍舊給定一個賦值函數(shù) g，它賦予D的元素到單個變量。為方便起見我們寫wRw表示w, w滿足關系R。記號M |= w,g A表示在框架M中在w世界g滿足合式公式A。其遞歸定義如下 M|=w,g C(t,t1,.,tn-1)當且僅當

3、F(w,c)其中g(t)若t是一個變量Val(t,w,g)=F(w,f) (Val(t 0 ,w,g), ,Val(t m-1 ,w,g) 若 t= f(t 0, , tm-1) M|= w,g t1 = t2 M|=w,g A B當且僅當 Val(t 1,w,g)=Val(t 2,w,g)當且僅當 M|=w,g A 且 M|= w,g B M|=w,g A 當且僅當 M|=w,g A M|=w,g xA 當且僅當對每一個d D,M|= w,g(d|x) A M|=w,g MA當且僅當存在一個 w W使得wRw且M|=w ,gA其它的邏輯連結詞按標準方法來解釋，此外定義LA = M A。R的形

4、式性質決定了模態(tài)邏輯(公理和推理規(guī)則)。我們稱一個合式公式關于一個特殊框架類C為真,當且僅當它對C中每個框架的每個賦值函數(shù)和可能世界所滿足。因此，如果我們取C為所有使R是自反的框架，則得到熟知的邏輯T。如果R是傳 遞的，則得到S4,如果R是自反，傳遞和對稱的(即等價關系)，則得到模態(tài)邏輯 S5。模態(tài)邏輯T由謂詞邏 輯公理系統(tǒng)加上公理LA AL( A B) ( LA LB)得到。推理規(guī)則_ALA表示必要性。S4在T的公理系統(tǒng)中加上公理LA LLA。S5在S4公理系統(tǒng)中加上公理MA LMA。由于使單個的域保持固定，Baican 公式x(LA) L( xA)對所有框架都為真。10.2時態(tài)邏輯(Tem

5、poral Logic)時態(tài)邏輯，在不同時間，同一個語句可以有不同的真值。時態(tài)邏輯語言Lt由通常邏輯語句加上時態(tài)算子F, P, G , H組成。其中FA表示在將來(Future)某個時間A為真；PA表示在過去(Past某個時間A為真；GA表示在所有將來時間 A都為真；HA表示在過去時間 A總歸為真。定義2個時態(tài)框架T由時間非空點集T,一個時間優(yōu)先次序關系 R以及一個函數(shù)h:TX Lt的原子集合 0,1所組成。T = (T, R, h)。函數(shù)h給每一個原子語句在全部時間點上賦予真假值。h在整個Lt上的語義由下列方式規(guī)定： h(t, A B)=1 當且僅當 h(t, A)=1 且 h(t, B)=

6、1 h(t, A)=1 當且僅當 h(t, A)=0 h(t, FA)=1 當且僅當(t )( R(t, t)&h(t, A)=1) h(t, PA)=1 當且僅當(r )(R(t, t)&h(t, A)=1)其中R(t, t)表示按時間優(yōu)先次序t優(yōu)先于t 由GA和HA的意義知GA FAHA PA因此h(t, GA)=1 當且僅當(t )(R(t, t h( ) , A)=1)h(t, HA)=1 當且僅當(t )(R(t h(t , A)=1)如果一個語句在任何時間點都取值為1,我們稱它在這樣一個框架中為真，。對R的不同限制導致不同的時態(tài)邏輯變種。最小時態(tài)邏輯K為不對R加任何限制。我們稱一個

7、語句為 K-valid當且僅當它在全部時態(tài)框架中都真。 最小時態(tài)邏輯精確地是K-valid語句集合，并且有下列公理系統(tǒng)(A1-A7)為特征，以及 MP(modus ponens作為推理規(guī)則：(Ai) A，其中A是永真式。(A2)G(AB)(GAGB)(A3)H(AB)(HAHB)(A4)AHFA(A5)AGPA(A6)GA，如果A是一個公理(A7)HA，如果A是一個公理(MP)若A及A B，則B可以證明(見McArthur McArthus , J.(1979) Tense logic , Reidel1976或Rescher & Urquhart Rescher ,J.& Urquhant

8、, A (1971) temporal logic , Springer Verlag1971)這個系統(tǒng)的定理精確地是K-valid語句(完全性結果)分支時間(Branching Time)是在R上加上下面兩個限制：(R1)( t s r)(R(t, s) R(s, r) R(t, r)(R2) ( t s r)(R(t, r) R(s, r) R(t, s) (t = s) R(s, t)傳遞性(R1)表示時間優(yōu)先次序的傳遞性，(R2)表示反向線性性，即下列形式的時間分支：分支時間因此堅持僅存在一個過去，但允許將來保持分開。為了公理化這個邏輯(在所有滿足(R) (R2)框架上語句為真)我們需

9、要在公理系統(tǒng)(At)-(A 7)加上兩個公 理：(A8) FFAFA(A9)(PAPB) (P(A B) (P(A PB) (P(PA B)其中(A8)對應于傳遞性，(A9)對應于反向線性性。Reschen&Urguhant稱之為Kb邏輯。經(jīng)典時間圖是一個線性序列，這樣的概念來源于物理，例如牛頓的絕對時間是一維線性連續(xù)統(tǒng)，甚至相對物理中局部時間序列也是線性的。為了使將來和過去都分支，我們在R上加上限制：(R3)( s t)(R(s, t) (s = t) R(t, s)顯然(R3)等價于(R2)和向前線性性限制(R4)的合?。?R4) ( st r)(R(r, t) R(r, s) R(s,

10、t) (s = t) R(t, s)為了使所有滿足(R1)和(R3)框架上的語句為真，需要在公理系統(tǒng)(A1) (A9)上添加公理(A10)(A10)(FAFB) (F(A B) (F(A FB) (F(FA B)公理(A10)對應于向前線性性。由(A1HA10)所定義的時態(tài)邏輯稱為K1，由Nino Cocchiarella所引入。這個邏輯仍然留下許多關于時間性質的未知基本問題。例如：是否有一個時間的開始和終止時刻？是否在 任何兩個時刻之間存在一個時刻？時間的連續(xù)性是否象實數(shù)一樣？對這些問題的不同回答導致不同的時態(tài) 邏輯。對第一個問題的肯定回答導致在關系R上的兩個進一步限制：(R5)( s)(

11、t)(R(t, s)(R6)( s)( t)(R(s, t)(R5)保證時間無開始，(R6)保證時間無結束。它的公理系統(tǒng)為附加公理(A11), (A12)到(A1)(A10)上。(Aii) GAFA(A12) HAPA相應的時態(tài)邏輯由 Dana Scoff所引用，記為Kss任何兩個時刻之間是否存在一個時刻？肯定的回答導 致時間象有理數(shù)一樣稠密，否定的回答強迫時間具有自然數(shù)一樣的機構。一個肯定的回答強迫時間線在下 列意義下稠密。(R7)( s)( t)( r)(R(s, t) (R(s, r) R(r, t)要求在Ks公理系統(tǒng)中增加一個公理(A13) FA FFA這個線性時態(tài)邏輯由 A. N.

12、Prior所建立，記為Kp最后一個問題涉及時間的稠密度象有理數(shù)還是象實數(shù)。若我們將一個稠密有序線性序列T分成兩個非空集合T1和T2，使得T1中每個點優(yōu)先于T2中的點，則可能存在三種情況：T1有一個最后元素，但 T2無第一個T1沒有最后一個元素，但 T2有第一個T1沒有最后元素，T2也沒有第一個若僅允許和，則 T的次序是連續(xù)的。限制為：(R8) ( T1, T2)(T = T1U T2) ( s T1)( t T2)(R(s, t)( s) ( s T”(R(s, s) ( t T2)(R(s , t)上面的全線性連續(xù)性反映在公理：(A14) (GAPGA) (GA HA)其中口 B定義為GB

13、HB B。我們稱滿足(A11) (A 14)公理的時態(tài)邏輯為 Kc10.3模態(tài)框架(modal framework )一般的模態(tài)框架考慮一個由許多類似的狀態(tài)(state)(或世界world )組成的一個宇宙(universe),以及狀態(tài)之間可訪問的關系 R(s, S)組成。關系R(s, s)規(guī)定了從一個狀態(tài)s轉變成另一個狀態(tài)s的可能性。例如：在宇宙中的每個狀態(tài)是一個日子，一個可能的可訪問關系可以是兩天s, s之間的關系。若s是s的將來。主要記號想法是避免明顯控制或狀態(tài)參量(日子)或可訪問關系。而引入兩個特殊算符來指岀從 宇宙中一個狀態(tài)到可訪問狀態(tài)的性質。引入兩個模態(tài)算子(稱為必然算子neces

14、sity operator)和(稱為可能算子 possibility operator )。我們用I w I s表示公式w在狀態(tài)s的真值，則和的意義由下列解釋規(guī)則來定義：1 口 W I s = ( s )(R(s, s) I W I s)2 W I s = ( s)(R(s, s) A I W I s)即如果公式w在從狀態(tài)s的所有R-可訪問的狀態(tài)下都為真，則口W在此狀態(tài)s下為真。類似地，如果w至少在從狀態(tài)s的一個R 可訪問的狀態(tài)下為真，則W在此狀態(tài)s下為真。一個模態(tài)公式是一個由命題符號，謂詞符號(包括等值符號)，函數(shù)符號，常量符號，變量符號，典型的算符和量詞以及模態(tài)算子所組成。沒有模態(tài)算子的公

15、式稱為一個靜態(tài)(static)公式。一個完全的模態(tài)(動態(tài))公式可以很方便地看成是由把模態(tài)和典型的算子應用到靜態(tài)子公式上所組成。一個模態(tài)公式在給定宇 宙中某個狀態(tài)下的值由反復利用上面關于模態(tài)算子的規(guī)則以及對靜態(tài)子公式在該狀態(tài)下的計算而得到。例如公式rain(l) rain(l)(或者表示為 rain(to, I) (t to)rain(t , I)解釋成在一給定日在一給定地點I,如果它在那天給定地點I處下雨，則存在將來某天在I處下雨。因此，雨最終將停止。類似地rain(I) rain(I)(或者表示為 rain(t。，I) (t to) rain(t , I)表示如果在那天在I處下雨，則在I處天

16、天都將下雨。注意，任何模態(tài)公式總歸考慮關于某個固定的 參考狀態(tài)，這個狀態(tài)可以任意選擇。在本例中，意味著今天。一般有精確定義一個模態(tài)公式 W的一個宇宙U = S,R,D，它由一個狀態(tài)(或世界)集合 S以及在S上的 二元關系R (稱為可訪問關系)以及一個域(domain) D組成。每個狀態(tài)s S，s= Is, D提供域D上對W 中所有命題符號，消詞符號，函數(shù)符號，常量符號，(自由)變量符號的一個一階謂詞邏輯解釋。一個模 型(U，So)是一個具有U的狀態(tài)之一 so S的一個宇宙U。so被賦予為初始的參考狀態(tài)。簡言之，狀態(tài)集合Sw的宇宙=狀態(tài)間可訪問關系 R域D其中狀態(tài)s =在D上給w的符號賦值s =

17、A, D。在一個給定的宇宙 U中，歸納地給一個模態(tài)公式w在一個狀態(tài)s下定義其真假值，記為w so如果w是靜態(tài)的，即不含模態(tài)算子，則其真假值由w在s下的解釋決定。 w s 是 s(R(s, s) w s)(3) w s是 s(R(s, s) w s)W1 W2 s為真當且僅當或者 W1 s為真或者 W2 s為真。w s為真當且僅當w s為假xw s為真當且僅當存在一個不同于U的宇宙U，由最多在U中每個狀態(tài)中給出對 X的解釋，使得I w I s在U 中為真。對其它算子及全稱量詞的規(guī)則可由上述規(guī)則導岀。例如考慮公式ww = X yp(x, y)對一個宇宙U = S, R, D的解釋W s對s S的意

18、義是(xeD)( s eS)(R(S, s)( yeD) p(x, y) s)因此，倘若對所有賦給 x的值以及從s可以訪問的每個狀態(tài) s，存在一個對y的賦值(可能依賴于對x的賦值和s的選擇)使得p(x, y)在s中為真，則此公式將在宇宙U中的狀態(tài)s為真。注意，由我們的記號 (口 w) s表示在某個s可以達到的狀態(tài)s， w s為真。即， w代表：我們可以達到一點，在該點 w是從此而真的，即存在一個從s的R-可訪問的狀態(tài)s，使得s本身及它的所有R-后代都滿足w。 ( w) s表示對所有從s的R-可訪問的狀態(tài)s， w s為真。即， w代表：不管w走到哪里仍然是可實現(xiàn)的；即對每個從s的R-可訪問的狀態(tài)

19、s可以找到一個s的R 后代，它滿足w。 (w w) s表示對從s的所有R-可訪問的狀態(tài)s , w w s為真。即， (w w)代表：如果在任何時候 w在s的某個后代s變?yōu)檎?，則它對s的所有后代仍為真。如果一個公式 w在一個宇宙中的一個狀態(tài)so為真，則我們稱(U , so)是公式w的一個滿足模型或公式w在(U , So)被滿足。一個在每一個宇宙的所有狀態(tài)都為真的公式w被稱為有效的(valid)。即對w的每個宇宙U以及對U中每個狀態(tài)s, w s為真。例如公式：w三 w是一個有效的(valid)公式。這個公式建立“必然性(necessity)”和“可能性(possibility)之間聯(lián)系。另一個有效

20、的(valid)公式是： (w 1w 2)( w 1 w 2)即如果在所有可訪問狀態(tài)中成立w1w22并且如果w1在所有可訪問狀態(tài)中為真，則w2也必須在所有這些狀態(tài)中為真。這兩個公式對任何可訪問關系都是有效的。如果我們同意在關系R上放進一步一般限制，我們得到附加的有效的公式，它們對滿足這些限制的關系的任何模型為真。按照在R上加不同的限制就得到不同的模型系統(tǒng)。在我們的討論中，我們約定 R總歸是自反(reflexive)和傳遞(transitive)的；即如果一個公式在具 有自反和傳遞的可訪問關系的每個宇宙中的所有狀態(tài)是真，我們考慮它是有效的。例如，公式 w w是有效的。因為它對任何自反模型是真的。

21、它要求承認對一個狀態(tài) S,如果從s的所有可訪問的狀態(tài)滿足 w， 則w被s本身滿足。這是顯然的，因為，由于自反性s從其本身是可訪問的。公式 W w是有效的，因為它對所有傳遞模型為真。它要求承認對一個狀態(tài) sc，如果存在一個從S1的可訪問的狀態(tài)S2, 而si的是從狀態(tài)so可訪問的，使得S2滿足w,則如果存在一個從so的可訪問的狀態(tài)S3滿足w。在一個傳遞 模型中這總是成立，因為，由于傳遞性，S2也是從so是可訪問的，我們可以取 S3 = S2。10.3.1 時態(tài)邏輯框架(temporal framework)時態(tài)邏輯框架是由模態(tài)邏輯框架推導岀的。在解釋的模型上放上進一步限制。由時態(tài)邏輯所給的對基本的

22、可訪問關系解釋是時間的推移。如果經(jīng)過時間的發(fā)展s可以變化成s則一個世界s是從一個世界S可訪問的。我們集中到開發(fā)的歷史上，它是線性和離散的。因此時態(tài)邏輯的模型由3序列組成，即形如b =so, s1,的序列。在這樣一個序列，Sj可以從Si訪問當且僅當i Wj。由于序列的離散性，我們不僅可以 引用狀態(tài)在一給定狀態(tài)的將來，而且也引用唯一的立即將來狀態(tài)或下一個狀態(tài)。這導致一個附帶的算符， 即下一個時刻(next instant)算符記為O。相對于一般模態(tài)邏輯框架概念，一個宇宙由一個非空狀態(tài)(世界)組成。在這些狀態(tài)上，我們定義一個立即可訪問性關系P,這要求是一個函數(shù)，即意味著每個世界s精確地有另一個世界

23、s使得p (s, s。這對應于我們的離散時間模型，每個時刻精確地有一個后繼者。P的自反傳遞閉包(transitive reflexive closure)R =P *是一般模態(tài)邏輯框架所討論的可訪問性關系，并且是自反和傳遞的。 直觀地，R(s, s 成立，當s或者等同于s或者在s的未來上。根據(jù)加在R上的限制，所產(chǎn)生的模型(U, So)可以表示成一個無限狀態(tài)序列b = so, si, S2,其中p ( s, Si+i)對i 0為真。這直觀地對應于在時間離散點序列上所觀察到的一個過程的時態(tài)發(fā)展。下面給岀用于程序推理用的時態(tài)邏輯語言的一個更完全的語言定義，而沒有必要是最一般的時態(tài)語言。符號這個語言使

24、用一套由單個變量符號，常量符號，命題符號，函數(shù)符號和謂詞符號組成的基本符號集合。 這個集合分成兩個子集：全局符號和局部符號。全局符號在完全的宇宙上有一統(tǒng)一的解釋，并且當從一狀 態(tài)改變到另一狀態(tài)時不改變他們的值和意義。另一方面，局部符號在宇宙的不同的狀態(tài)上可以假定有不同 的意義和值。為了我們的目的，對我們感興趣的局部符號僅是局部單個變量和局部命題符號。我們將有所 有類型的全局符號。符號進一步分成不同的類別 (sort)。每個類別對應于一個不同的域，而且解釋將把一個域和每一類別 相連。對應一個類別，我們可以有在相連的域上解釋的單個常量，和從該域取值的單個變量，表示域上函 數(shù)的函數(shù)符號，以及表示域上

25、謂詞的謂詞符號。用于單個常量，函數(shù)和謂詞的符號是我們希望公式化的該 域的典型的一階謂詞邏輯理論。例如，在處理自然數(shù)理論中我們使用習慣的符號。0，+，-，x，*， 。注意某些函數(shù)和謂詞可以有一個非同質標記non-homogenous,即它們可以有不同的和不同的參量位置相連的類別。典型的例子是if-then-else函數(shù)，它接受一個布爾型參量和兩個可能的其它類別的參量。算子和量詞我們利用正常的布爾型(Boolean)連接詞A，V，以及等于算符=和一階量詞 及 的集合。這個集合稱為經(jīng)典算子(classical operators)o對于模態(tài)算子(modal operators)，我們使用下列模態(tài)算子

26、：一目 總歸(always)一目 有時(sometime)一目O 下一次(next)二目U 直到(until)量詞和僅應用于全局單個變量。項(term)同一階謂詞定義，項由單個常量和函數(shù)所應用的單個變量組成。注意函數(shù)參量的個數(shù)和參量類別要 相符.此外，如果t是一個項，則O t表示t的下一個值。注意，我們以兩種不同的方式使用下一次算子O, 一種作為時態(tài)算子應用到公式，一種作為時態(tài)算子應用到項。公式(語句)(Formula or sentences)公式由原子公式構成，我們將布爾型(Boolean)連接詞，在全局變量上的模態(tài)算子和量詞應用到它們之上。原子公式由應用于適當類別的項上的命題和謂詞(包含

27、=算符)組成。一個公式稱為靜態(tài)的(static),或經(jīng)典的(classic)，如果它不包含模態(tài)算子。我們有時將命題和(封閉的)公式看成產(chǎn)生真為1，假為0的整數(shù)值函數(shù)。 然后，這些函數(shù)可以被算術 地組合以便提供對等價的長的命題公式一個緊縮表示。例如對命題P1,P2 ,，Pn語句nP1 + P2 + + Pn = 1 或Pi=1i 1敘述精確地Pi之一為真。當然，這等價于公式(R Pj)10.3.2 模型（環(huán)境）對我們的語言來講，一個模型 （I ,a,b ）由一個（全局）解釋 I, 一個（全局）賦值a和一個狀態(tài)序 列b組成。解釋I規(guī)定對應于每個類別的一個域，并且把具體的元素，函數(shù)和謂詞賦給（全局）

28、單個常量，函數(shù) 和謂詞符號。賦值a將適當域上的一個值賦給每個全局自由變量及命題。對于序列a = SO, S1,我們記b =Si, Sj+1,為b的截去i個的尾部后綴（i-truncated suffix）。給定一個時態(tài)公式 W，下面我們介紹一個W在一個模型（I，a，b ）中真假值的歸納地定義。在（I，a，b ）下任何子公式或項T的值記為| ，|被隱含地假設。首先考慮項的估算：對一個局部單個變量或局部命題y:y |= ysS 0的值。u:即賦于y在b的第一個狀態(tài) 對一個全局單個變量或全局命題U |= a u即由a賦給u值對一個單個常量由I給其估算:C| = Ic對一函數(shù)f（x1,Xk）：f(t1

29、,.,tk) | I f (t1 | ,.,t即由應用所解釋的函數(shù)If到在環(huán)境中所估算的t1,tk值上給岀其值。第-257 -頁對一個項t:Ot|t| (1)=S1, S2,中值給出即Ot在b = S0, S1,中的值由t在平移序列b 現(xiàn)在考慮語句的估算：對一謂詞P（X1,Xk）包含（等號）:P(t1,.,tk)| IP(t1 | ,.,t對一個析取(disjunction):true(Wjw2) | true 當且僅當 w1 | true 或w對一個否定 (negation):( w) | true 當且僅當 w1 | false對下一次(next)算子：Ow |W|(1)于是O w意味著：

30、w將在下一個時刻為真，讀成“ next w”對一個全部時間(all-time (always) (henceforth)應用：w|true當且僅當對每個k 0,w|仏)true即w對b的所有后綴序列為真。于是口 w意味著：w將在所有將來時刻(包括現(xiàn)在)為真，讀成“ alwaysw”或“ henceforth w ”。對有時(some-time) (eventually ) (sometimes)應用： w |true當且僅當存在一個k0, w| %)true即w至少在b的一個后綴序列上為真。于是w意味著：w將在某個將來時刻(可能現(xiàn)在)為真，讀成“ sometimes w” 或“ eventua

31、lly w ”。對于一個直到(until)應用：w1Uw2 |true當且僅當存在某個 k 0,W2 | 伙)true且對所有 i ,0 ik,w1 | (i) true于是w1Uw2意味著：存在一個將來時刻w2將在該時刻為真，并且使得直到那個時刻之前w1繼續(xù)為真，讀成“ wentil w2 ”。對一個全稱量詞 (universal quantification):(u.w) |true當且僅當對每個 d D,w| true其中a = a u d是從a由把d賦給u得到的賦值。D是u的定義域。對一個存在量詞(exi stential quantification):(u.w) |true當且僅當

32、對某個 d D, w| true其中 a = a u d。下面是一些時態(tài)表達式和它們的直觀解釋例子：u v如果u現(xiàn)在為真，v將最終變成真。 (u v)無論何時u變成真，v將最終變成真。 w在將來某個時刻w變成永久地真。 (wA O w)存在將來某個時刻使得 w在那個時刻為真，而在下一個時刻為假。 w每個將來時刻后隨一個稍后一個時刻w在那個時刻為真，因此，w無限地經(jīng)常為真。 (u v)如果u旦變?yōu)檎?，則v在那個時刻及其之后都為真。 v(v) U u)如果v發(fā)生，它的首次出現(xiàn)被 u在其前(或相同)。如果w在模型(I , a,b )下為真，我們稱(I , a,b )滿足w或者稱(I , a,b )是

33、一個w的滿足模型。我們把它記為(I ,a,b ) |= w。一個公式w是可滿足的(satisfiable)，如果存在 w的一個滿足模型。一個公式w稱為有效的(valid)，如果它在每個模型中為真。記為|= w。有時我們對某一限制模型類C感興趣。一個公式w對C中每個模型都為真，則稱w是C-有效的(C-valid)，記為C |= w o10.3.3 關于時態(tài)邏輯的永真公式下列是一些有效的時態(tài)語句:對偶性1.|= w w2.|= w口 w3.|=O wO w蘊涵關系4.|= ww5.|= ww6.|=O w w7.|= wO w|= w w8.|= w0口 w9.|= W1 UW2 w210.| =

34、 w w11.| = w w12.| = w w交換律13.|= O w?？?w14.|= O wOOw15.|= (Ow1)U( O w2)O(w1Uw2)分配律16.|= (w1w2)( w1 w2)17.|= (w1w2)( w1 w2)18.|= O (w1w2)(O w1O w2)19.|= O (w1w2)(O w1O w2)20.|= O (w1w2)(O w1O w2)21.|= (w1 w2)Uw3)(w1Uw3)(w2Uw3)22.|= (w1U(w2 w3)(w1Uw2)(w1Uw3)23.|= ( w1 w2) (w1 w2)24.|= (w1w2)( w1 w2)25

35、.|= (w1Uw 3)(w 2Uw 3)(w 1 w2)Uw 3)26.|= (w1U(w2 w3)(w1Uw2) (w1Uw 3)單調性27.|= (w1w2)( w1 w2)28. |= (w1w2)( w1 w2)29.|= (W1W2)(O W1O W2)30.|= (W1W2)(W 1UW 2)(W2UW3)31.|= (W1W2)(w oUw 1)(W0UW2)frame rules32.|= ( W1O W2)O (W1W2)33.|= ( W1 W2) (W1W2)34.|= ( W1(W2UW3)(W1W2)U(W1 W3)歸納法則(induction rules)35.

36、|= (wOw)(w w)數(shù)學歸納法(computational induction)36. |= (w w) (wOw)最小數(shù)原則(least number priciple)37. |= w (w0口 w)38. |= w (wOO w)39. |=(W1UW2) (W2 (w 1 O(W1UW2)40. |= (wUw) w41. |= ( W1 W2)(W1UW2)42. |= (w1 W2)UW 3)(W1UW3) (W2UW3)43. |= (W1UW 3)(W2UW3)(W1UW3)44. |= (W1U(W2 W3)(W1UW2)UW3)45. |= (w1Uw2)Uw3)(w

37、1Uw2)UW 3)|= (w1U(w2 W3)(w1 W2)UW 3)46.=xWx w47.1=口xwx口 W48.|=OxWxO w49.|=Ox wx O w50. ( xw1)Uw 2)x(w1Uw2)倘若x在W2中不是自由變量51. |= (W1U( xW2)x(W1Uw 2)倘若x在W2中不是自由變量52.|=w| = 口 W53.|=w= W54.|=w|=O w55.|= W1W2|=口 W1口 W256.|= W1W2= W1 W257.|= W1W2|=O w1O W258.|= W1口 W2|=W1口 W3|= W2口 W359.|= W1 W2|=W1 W3|= W2

38、 W360.|= W1W2|= W2口 W3|=W1口 W4|= W3W461.|= W1W2|= w2 w3|=w1 w4|= w3w462.|= w1w2|= w2O w3|=w1O w4|= w3w4語句1到4指出算子之間的對偶性(duality)。語句1說明，w在一個序列的所有狀態(tài)中為假當且僅當不存在使w在所有狀態(tài)中為真。語句2說明，存在一個 w為假的狀態(tài)當且僅當不存在使w為真的狀態(tài)。語句3說明，w在下一狀態(tài)為假當且僅當不存在使w在下一狀態(tài)為真的情況。這個語句限制每個狀態(tài)有不多于一個單個后繼者。語句4到10表示算子之間的蘊涵關系。語句4說明，如果w現(xiàn)在為真，則它將在將來某個時間為真。這

39、也是目前被考慮為將來的一部分的 事實的立即結果。語句5是語句4的對，它說明，如果 w在所有將來時刻為真，則它現(xiàn)在也為真。語句6說明，如果w在下一時刻為真，則它將在某個時間為真。這是因為下一時刻也是將來的一部 分。語句7是語句6的對，它說明，如果 w在所有將來時刻為真，則它也在下一時刻為真。語句7說明，如果w總是為真，則它有時為真。語句8說明，如果w在所有將來時刻為真，則它也在下一時刻的所有將來時刻為真。語句9說明，如果wi直到w2將發(fā)生為止為真，則 w2將最終地發(fā)生。語句10說明，如果w在某個時刻之后永遠為真，則它無限地經(jīng)常為真。語句11和12表明和都是同前有效的(idempotent)。直觀

40、地講，兩者都含有將來是將來的將來的 含義。語句13到15表示下一次算子O與其它每個算子的交換性(commutativity)。它等于把我們的參考點從目前平移到緊接的下一時刻。語句13說明，如果w對每一個將來時刻的下一時刻成立，當且僅當w對除去當前的所有將來時刻都成立。語句14說明，如果w對某個將來時刻的下一時刻成立，當且僅當w對除去當前的某個將來時刻成立。語句14說明，如果O w1直到O w2的某個事例成立，當且僅當w1直到w2從下一個時刻開始成立。語句16到22表示時態(tài)算子和布爾連接詞之間分配律關系。語句23到26表示當時態(tài)算子和布爾連接詞之間交換次序時所成立的蘊涵。它們不是等價的，并且僅僅

41、給定的蘊涵方向為真。語句27到31表示每個時態(tài)算子的單調性(monotonicity);即，如果應用到一個公式 w1為真，并且 w1 全體地蘊涵(對所有時刻)w2,則它的應用到 w2也為真。這個性質分別對27中的口，28中的，29中的O，30和31中的U的兩個位置。語句32到34是框架規(guī)則(frame rules)。它們說明，如果已知w1對所有狀態(tài)成立，則w1可以被增加作 為在任何其它時態(tài)算子之下的一個合取。這分別對32中的O，33中的，34中的U的兩個參量加以敘述。語句35和36是歸納規(guī)則(induction rules)。語句35對應于計算歸納(computational inductio

42、n)即數(shù)學歸納法，它說明，如果w在任何時刻成立的事 實蘊涵它也在下一個時刻成立，以及在現(xiàn)在成立，則w在所有將來時刻都成立。語句36對應于最小數(shù)原理(least number priciple)，是語句35的對，它說明，如果 w現(xiàn)在為真，以及 在將來某個時刻為假，則存在某個時刻，使得w在那個時刻為真，并且在下一個時刻為假。語句37到39解釋口，和U算子分別由分配它們的效果到什么是目前所隱含和什么是下一個時刻 所隱含。語句40到45表示直到算子(until)的一些性質。語句46到51表示時態(tài)算子和量詞之間的交換關系。語句46和47熟知為Barcan公式。推理(inference)52說明如果 w是

43、正確的(valid)，則口 w也是正確的。w是正確的事實意味著它對任何 序列為真，因此，對一個給定的序列的所有后綴b(i)為真。于是 w對每個序列b為真，因此是一個正確的語句。推理53可以由推理52和利用正確語句7|=口 w w得到。推理54可以由推理52和利用正確語句7|= w Ow得到。推理55到57可以由推理52首先推導出|= (w1w2)，然后分別利用正確語句27到29推導出 1)個進程P1,Pm組成，每一個進程Pi(1im)是一個具有標號分別為歸，1嘰,lie的節(jié)點(位置location )的獨立轉移圖(transition grarh)。不同進程的標號集合 Li= l i0, li

44、1, lie互不相交。在每個進程中轉移圖中的邊(轉移)由下列形式所表示(見圖 1 )：其中y=(y1,y2,yn)是程序變量集合，它由所有進程訪問并共享。Ca( y )是轉移 的可行(enabling)條件，f是與轉移a相聯(lián)的變換。若c ()為真，則我們稱對于 y轉移a是可行的(enabled)o如圖2所示，對于一個帶有k個外出轉移的給定的節(jié)點l，我們定義E|(y)c1(y) .ck (y)是在節(jié)點l的完全出口 (full-exit)條件。我們不要求用完單個條件，即不要求對每個y， El(y) true ；因此，在我們的語義中是允許死鎖的。我們也不要求這些條件是排它性的；因而，每個單個進程可以

45、是不 確定性的。一個其單個條件是排它性的位置被稱為確定性位置。如果E|()為真，即從I發(fā)岀中至少有一個a i, i = 1,.,k是可行的，我們稱位置l對y 一可行的。如果進程Pi當前在l Li，而l是可行的，我 們稱該進程是可行的。ci (y) f 歹：i (y)這個程序變量集合 y =(yi ,y2,yn)是由所有進程可訪問和共享的。這個并發(fā)程序模型稱為共享變量 模型(Shared-variables model)。在這個模型中，進程間的通訊和同步經(jīng)由共享變量管理。一個并發(fā)程序的一 個完全規(guī)格說明也包含程序變量的初始值的說明。我們常常將一個進程以一個線性正文形式表示岀來而不用一個圖的形式來

46、表達。在這種情況下，節(jié)點正好是在每個語句前放的位置(標號)，而轉移是語句本身。線性正文形式限制每個節(jié)點最多有兩個轉移。下面我們列岀以線性正文形式表示的語句類型的形式及其對應的圖形表示形式：y ： =fI: if P(y) then goto m P(y) f i：if P(y)theny：=f(y)Lloop until P(y)這個語句循環(huán)直到條件 p()變?yōu)檎鏋橹?。Z-loop while P(y)這個語句是上面語句的補充：它循環(huán)直到條件p()變?yōu)檎鏋橹?。l compute,uPusing,vs(uin ,5)：二 二唧這個語句表示一個終止計算的段，其細節(jié)我們不感興趣。該段僅僅可能修改程序

47、變量Ui,.,Up, p 0，并且僅可以引用程序變量Vi,.,Vs, s 0。該段最后必經(jīng)終止。我們將經(jīng)常使用下列形式的計算段：I: computel :它是上面的弱特殊情況即p = s = 0，指的是既不修改又不訪問任何改程序變量的一個終止計算的段。I- execute Uj,，Up using vj, 3 vs匸 u&f (u J Up)：網(wǎng)true - 1true 這個語句表示任意一個程序段，它可以修改程序變量U1,up, p 0,并且僅可以引用程序變量V1,vs so。但不要求該程序段最終終止halt這是一個無出口的節(jié)點。I goto r注意，對于到目前為止考慮的所有語句，除了halt

48、語句之外，其完全岀口條件總歸為真，并且除了execute ,using ui,., us語句以外，都是確定性的，即它們都有排他性轉移。例子：例1對于整數(shù)k和n，計算二項系數(shù)(Binomial Coefficient) ： ,0 k n 。lo： if y 1 = (n-k) then go to ley1：=n ; y2：=0 ; y3：=1mo：if y 2 = k then go to me11： y3 := y3 x y1；m1：y2 ：= y2 + 1I2: y1 := y1 - 1;m2： loop until y 1 + y2 n13： go to lo;m3：y3： = y3 /

49、 y2le：halt;m4：go to meme：halt進程P1進程P2計算分子(numerator)計算分母(denominator)指令m2：loop until y 1 +y2 n同步進程Pi和P2，以保證y3僅僅在它已被乘上n-i+1之后才被i除。這保證了整除性質，這里用到數(shù)學定理：“i個相鄰的整數(shù)乘積j x (j+1)(j+i-1)總歸可以被i!所整除?？疾煸?m2中的中間表達式：n (n 1) (n j 1) y31 2 (i 1)其中1 ijn, y1 = n-j, y = i。分子由j個相鄰正整數(shù)相乘組成，因而，它可以由i除得盡。如果j = i,在我們絕對確信(n-i+1)已

50、經(jīng)被乘到y(tǒng)3之前，我們必須等待，直到 y1由12減少指令，從(n-i+1)減到n-i為止。 因此，進程P2在m2處等待，直到y(tǒng)1 + y2 n為止。為了追蹤在每一個進程中執(zhí)行的進展，我們可以設想一個位置變量向量-=-，皿，其中每個 n i G Li。位置變量n i指向Pi中位置，它是下一個將要執(zhí)行的位置?，F(xiàn)在，讓我們考慮在我們模型中執(zhí)行的概念、見解。一個主要簡單化的假設是程序由多道程序設計 (programming)或交叉(interleaving)執(zhí)行。在這個假設之下，執(zhí)行作為一個離散步的序列進行。在每一步，選 擇一個能行的進程，并且它的能行的轉移被執(zhí)行。我們用一個執(zhí)行這個選擇的調度程序來體現(xiàn)這個選擇。在計算的任何步，調度程序選擇一個能行的進程，并且讓那個進程執(zhí)行一條指令(轉移)。為了完全 性，我們也允許調度程序任意插入一個空閑步，在此步中不調度任何一個進程，不執(zhí)行任何指令，同時， 所有程序的值和位置變量保持相同。在無能行進程可供使用的情況下，一個空閑步是調度程序此后唯一選 擇，在這種情況下，我們稱程序是死鎖的。這種狀況的一個特殊情況是當程序已經(jīng)結束，即所有進程已經(jīng) 終止。因為假定交叉性，每個轉移被完整地執(zhí)行而無其