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

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

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

3、F(w,c)其中g(shù)(t)若t是一個(gè)變量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當(dāng)且僅當(dāng) Val(t 1,w,g)=Val(t 2,w,g)當(dāng)且僅當(dāng) M|=w,g A 且 M|= w,g B M|=w,g A 當(dāng)且僅當(dāng) M|=w,g A M|=w,g xA 當(dāng)且僅當(dāng)對(duì)每一個(gè)d D,M|= w,g(d|x) A M|=w,g MA當(dāng)且僅當(dāng)存在一個(gè) w W使得wRw且M|=w ,gA其它的邏輯連結(jié)詞按標(biāo)準(zhǔn)方法來解釋，此外定義LA = M A。R的形

4、式性質(zhì)決定了模態(tài)邏輯(公理和推理規(guī)則)。我們稱一個(gè)合式公式關(guān)于一個(gè)特殊框架類C為真,當(dāng)且僅當(dāng)它對(duì)C中每個(gè)框架的每個(gè)賦值函數(shù)和可能世界所滿足。因此，如果我們?nèi)為所有使R是自反的框架，則得到熟知的邏輯T。如果R是傳 遞的，則得到S4,如果R是自反，傳遞和對(duì)稱的(即等價(jià)關(guān)系)，則得到模態(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。由于使單個(gè)的域保持固定，Baican 公式x(LA) L( xA)對(duì)所有框架都為真。10.2時(shí)態(tài)邏輯(Tem

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

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

7、語句為 K-valid當(dāng)且僅當(dāng)它在全部時(shí)態(tài)框架中都真。 最小時(shí)態(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是一個(gè)公理(A7)HA，如果A是一個(gè)公理(MP)若A及A B，則B可以證明(見McArthur McArthus , J.(1979) Tense logic , Reidel1976或Rescher & Urquhart Rescher ,J.& Urquhant

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

9、要在公理系統(tǒng)(At)-(A 7)加上兩個(gè)公 理：(A8) FFAFA(A9)(PAPB) (P(A B) (P(A PB) (P(PA B)其中(A8)對(duì)應(yīng)于傳遞性，(A9)對(duì)應(yīng)于反向線性性。Reschen&Urguhant稱之為Kb邏輯。經(jīng)典時(shí)間圖是一個(gè)線性序列，這樣的概念來源于物理，例如牛頓的絕對(duì)時(shí)間是一維線性連續(xù)統(tǒng)，甚至相對(duì)物理中局部時(shí)間序列也是線性的。為了使將來和過去都分支，我們?cè)赗上加上限制：(R3)( s t)(R(s, t) (s = t) R(t, s)顯然(R3)等價(jià)于(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)對(duì)應(yīng)于向前線性性。由(A1HA10)所定義的時(shí)態(tài)邏輯稱為K1，由Nino Cocchiarella所引入。這個(gè)邏輯仍然留下許多關(guān)于時(shí)間性質(zhì)的未知基本問題。例如：是否有一個(gè)時(shí)間的開始和終止時(shí)刻？是否在 任何兩個(gè)時(shí)刻之間存在一個(gè)時(shí)刻？時(shí)間的連續(xù)性是否象實(shí)數(shù)一樣？對(duì)這些問題的不同回答導(dǎo)致不同的時(shí)態(tài) 邏輯。對(duì)第一個(gè)問題的肯定回答導(dǎo)致在關(guān)系R上的兩個(gè)進(jìn)一步限制：(R5)( s)(

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

12、Prior所建立，記為Kp最后一個(gè)問題涉及時(shí)間的稠密度象有理數(shù)還是象實(shí)數(shù)。若我們將一個(gè)稠密有序線性序列T分成兩個(gè)非空集合T1和T2，使得T1中每個(gè)點(diǎn)優(yōu)先于T2中的點(diǎn)，則可能存在三種情況：T1有一個(gè)最后元素，但 T2無第一個(gè)T1沒有最后一個(gè)元素，但 T2有第一個(gè)T1沒有最后元素，T2也沒有第一個(gè)若僅允許和，則 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)公理的時(shí)態(tài)邏輯為 Kc10.3模態(tài)框架(modal framework )一般的模態(tài)框架考慮一個(gè)由許多類似的狀態(tài)(state)(或世界world )組成的一個(gè)宇宙(universe),以及狀態(tài)之間可訪問的關(guān)系 R(s, S)組成。關(guān)系R(s, s)規(guī)定了從一個(gè)狀態(tài)s轉(zhuǎn)變成另一個(gè)狀態(tài)s的可能性。例如：在宇宙中的每個(gè)狀態(tài)是一個(gè)日子，一個(gè)可能的可訪問關(guān)系可以是兩天s, s之間的關(guān)系。若s是s的將來。主要記號(hào)想法是避免明顯控制或狀態(tài)參量(日子)或可訪問關(guān)系。而引入兩個(gè)特殊算符來指岀從 宇宙中一個(gè)狀態(tài)到可訪問狀態(tài)的性質(zhì)。引入兩個(gè)模態(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的一個(gè)R 可訪問的狀態(tài)下為真，則W在此狀態(tài)s下為真。一個(gè)模態(tài)公式是一個(gè)由命題符號(hào)，謂詞符號(hào)(包括等值符號(hào))，函數(shù)符號(hào)，常量符號(hào)，變量符號(hào)，典型的算符和量詞以及模態(tài)算子所組成。沒有模態(tài)算子的公

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

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

17、A, D。在一個(gè)給定的宇宙 U中，歸納地給一個(gè)模態(tài)公式w在一個(gè)狀態(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為真當(dāng)且僅當(dāng)或者 W1 s為真或者 W2 s為真。w s為真當(dāng)且僅當(dāng)w s為假xw s為真當(dāng)且僅當(dāng)存在一個(gè)不同于U的宇宙U，由最多在U中每個(gè)狀態(tài)中給出對(duì) X的解釋，使得I w I s在U 中為真。對(duì)其它算子及全稱量詞的規(guī)則可由上述規(guī)則導(dǎo)岀。例如考慮公式ww = X yp(x, y)對(duì)一個(gè)宇宙U = S, R, D的解釋W(xué) s對(duì)s S的意

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

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

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

21、它要求承認(rèn)對(duì)一個(gè)狀態(tài) S,如果從s的所有可訪問的狀態(tài)滿足 w， 則w被s本身滿足。這是顯然的，因?yàn)椋捎谧苑葱詓從其本身是可訪問的。公式 W w是有效的，因?yàn)樗鼘?duì)所有傳遞模型為真。它要求承認(rèn)對(duì)一個(gè)狀態(tài) sc，如果存在一個(gè)從S1的可訪問的狀態(tài)S2, 而si的是從狀態(tài)so可訪問的，使得S2滿足w,則如果存在一個(gè)從so的可訪問的狀態(tài)S3滿足w。在一個(gè)傳遞 模型中這總是成立，因?yàn)椋捎趥鬟f性，S2也是從so是可訪問的，我們可以取 S3 = S2。10.3.1 時(shí)態(tài)邏輯框架(temporal framework)時(shí)態(tài)邏輯框架是由模態(tài)邏輯框架推導(dǎo)岀的。在解釋的模型上放上進(jìn)一步限制。由時(shí)態(tài)邏輯所給的對(duì)基本的

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

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

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

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

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

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

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

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

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

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

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

33、一個(gè)w的滿足模型。我們把它記為(I ,a,b ) |= w。一個(gè)公式w是可滿足的(satisfiable)，如果存在 w的一個(gè)滿足模型。一個(gè)公式w稱為有效的(valid)，如果它在每個(gè)模型中為真。記為|= w。有時(shí)我們對(duì)某一限制模型類C感興趣。一個(gè)公式w對(duì)C中每個(gè)模型都為真，則稱w是C-有效的(C-valid)，記為C |= w o10.3.3 關(guān)于時(shí)態(tài)邏輯的永真公式下列是一些有效的時(shí)態(tài)語句:對(duì)偶性1.|= w w2.|= w口 w3.|=O wO w蘊(yùn)涵關(guān)系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)單調(diào)性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ù)學(xué)歸納法(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指出算子之間的對(duì)偶性(duality)。語句1說明，w在一個(gè)序列的所有狀態(tài)中為假當(dāng)且僅當(dāng)不存在使w在所有狀態(tài)中為真。語句2說明，存在一個(gè) w為假的狀態(tài)當(dāng)且僅當(dāng)不存在使w為真的狀態(tài)。語句3說明，w在下一狀態(tài)為假當(dāng)且僅當(dāng)不存在使w在下一狀態(tài)為真的情況。這個(gè)語句限制每個(gè)狀態(tài)有不多于一個(gè)單個(gè)后繼者。語句4到10表示算子之間的蘊(yùn)涵關(guān)系。語句4說明，如果w現(xiàn)在為真，則它將在將來某個(gè)時(shí)間為真。這

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

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

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

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

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

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

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

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

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

48、語句之外，其完全岀口條件總歸為真，并且除了execute ,using ui,., us語句以外，都是確定性的，即它們都有排他性轉(zhuǎn)移。例子：例1對(duì)于整數(shù)k和n，計(jì)算二項(xiàng)系數(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進(jìn)程P1進(jìn)程P2計(jì)算分子(numerator)計(jì)算分母(denominator)指令m2：loop until y 1 +y2 n同步進(jìn)程Pi和P2，以保證y3僅僅在它已被乘上n-i+1之后才被i除。這保證了整除性質(zhì)，這里用到數(shù)學(xué)定理：“i個(gè)相鄰的整數(shù)乘積j x (j+1)(j+i-1)總歸可以被i!所整除?？疾煸?m2中的中間表達(dá)式：n (n 1) (n j 1) y31 2 (i 1)其中1 ijn, y1 = n-j, y = i。分子由j個(gè)相鄰正整數(shù)相乘組成，因而，它可以由i除得盡。如果j = i,在我們絕對(duì)確信(n-i+1)已

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