淺談時(shí)態(tài)邏輯在計(jì)算機(jī)科學(xué)中的發(fā)展

　　時(shí)態(tài)邏輯(又稱時(shí)序邏輯、時(shí)間邏輯)作為描述根據(jù)時(shí)間限定的命題或推理所使用的任意規(guī)則和符號(hào)系統(tǒng)，是模態(tài)邏輯的一個(gè)重要分支。在命題邏輯的基礎(chǔ)上，Arthur Norman Prior在上個(gè)世紀(jì)50年代幾乎獨(dú)自創(chuàng)建了這一現(xiàn)代邏輯的重要分支的基礎(chǔ)，對(duì)時(shí)態(tài)邏輯的發(fā)展具有里程碑意義，被視為“時(shí)態(tài)邏輯之父”。從上個(gè)世紀(jì)80年代開始，在其他學(xué)科如：計(jì)算機(jī)科學(xué)、數(shù)學(xué)、人工智能以及語(yǔ)言學(xué)等的發(fā)展需要的促進(jìn)下，時(shí)態(tài)邏輯獲得了新的進(jìn)一步的發(fā)展，從而形成了一些不僅具有理論意義而且也有豐富的實(shí)際應(yīng)用價(jià)值的成果。

　　1 計(jì)算機(jī)科學(xué)中時(shí)態(tài)邏輯的形式化

　　在邏輯學(xué)中，形式化是指分析、研究思維形式結(jié)構(gòu)的方法。“邏輯學(xué)的研究對(duì)象是思維的形式和規(guī)律，但這里的思維形式并非指的是人們思維過(guò)程中，能動(dòng)地、概括地間接反映現(xiàn)實(shí)世界的過(guò)程中所使用的那些形式，即具體的概念、判斷和推理，而是撇開了它們的具體內(nèi)容，僅僅抽象出其一般的形式結(jié)構(gòu)的概念、判斷和推理，這種邏輯形式通常借助于一定的語(yǔ)言形式來(lái)表達(dá)。”傳統(tǒng)的形式邏輯，是以自然語(yǔ)言為主要表述手段，這種表述接近日常思維實(shí)際，卻存在歧義、模糊、不夠精確的缺點(diǎn)。現(xiàn)代形式邏輯則以人工語(yǔ)言為主要表述手段，引入符號(hào)語(yǔ)言表達(dá)變項(xiàng)和常項(xiàng)。

　　在計(jì)算機(jī)科學(xué)領(lǐng)域，形式化方法是一種建立在嚴(yán)格的數(shù)學(xué)基礎(chǔ)上，具有精確數(shù)學(xué)表達(dá)形式和語(yǔ)義的開發(fā)方法。這種開發(fā)方法試圖實(shí)現(xiàn)從軟件的規(guī)范，軟件的設(shè)計(jì)到軟件的代碼實(shí)現(xiàn)自動(dòng)轉(zhuǎn)換和驗(yàn)證，從而充分保證系統(tǒng)的正確性和可靠性。在軟件開發(fā)過(guò)程中，最初級(jí)最原始的描述系統(tǒng)也就是規(guī)范的方法是用日常語(yǔ)言，這是一種非形式化方法，但這種描述方法可能存在模糊性、歧義性和層次混亂的缺點(diǎn)。

　　2 時(shí)態(tài)邏輯對(duì)計(jì)算機(jī)科學(xué)的貢獻(xiàn)

　　時(shí)態(tài)邏輯不僅可以作為哲學(xué)分析的有力工具，還對(duì)語(yǔ)言學(xué)、數(shù)學(xué)和計(jì)算機(jī)科學(xué)等其他學(xué)科產(chǎn)生了重要的影響，尤其是在計(jì)算機(jī)科學(xué)中。近些年來(lái)，軟件工程、人工智能發(fā)展迅猛，時(shí)態(tài)邏輯對(duì)計(jì)算機(jī)科學(xué)的重要影響逐漸被人們所認(rèn)知。在計(jì)算機(jī)出現(xiàn)初期，其功能相當(dāng)于一個(gè)十分龐大的計(jì)算器，輸入數(shù)字后，輸出計(jì)算結(jié)果。直到20世紀(jì)70年代，計(jì)算機(jī)科學(xué)家們認(rèn)為有必要對(duì)這些輸出的計(jì)算結(jié)果進(jìn)行正確性驗(yàn)證，可是由于計(jì)算機(jī)功能的越發(fā)強(qiáng)大，數(shù)據(jù)具有多任務(wù)和多變化的特性，對(duì)其進(jìn)行核查會(huì)越發(fā)的艱難。因此，計(jì)算機(jī)科學(xué)家們必須去研究在時(shí)間的推移下計(jì)算機(jī)系統(tǒng)的行為這一因素。于是，在這樣的背景下，這一理論在20世紀(jì)70年代被數(shù)學(xué)家Amir Pnueli和他的搭檔Zohar Manna引入計(jì)算機(jī)科學(xué)中，在計(jì)算機(jī)科學(xué)中得到了迅速的發(fā)展。時(shí)態(tài)邏輯是形式邏輯的一個(gè)分支，是經(jīng)典邏輯的一個(gè)簡(jiǎn)單的擴(kuò)充，它提供了一個(gè)很自然的方式來(lái)描述程序中的時(shí)態(tài)行為。時(shí)態(tài)邏輯能夠以一種簡(jiǎn)單、自然地方式來(lái)支持層次化的規(guī)范和驗(yàn)證。

　　時(shí)態(tài)邏輯對(duì)計(jì)算機(jī)科學(xué)的發(fā)展還有一個(gè)有用之處是：時(shí)態(tài)邏輯能夠表達(dá)程序的兩個(gè)特性：安全性和存活性。安全性用于描述事件必須不會(huì)發(fā)生，相當(dāng)于程序中的約束條件;存活性用來(lái)描述事件必須最終會(huì)發(fā)生，它可以防止程序只滿足初始條件及影響其它行為。線性時(shí)態(tài)邏輯顯示任何兩個(gè)不同的時(shí)間點(diǎn)都有先后關(guān)系，時(shí)間序列成不分叉的線狀分布的時(shí)態(tài)。與“線性時(shí)態(tài)邏輯”相對(duì)，在分支時(shí)間時(shí)態(tài)邏輯中，時(shí)間的結(jié)構(gòu)有分支樹形的性質(zhì)，即每一個(gè)時(shí)刻都有多個(gè)后繼時(shí)刻，時(shí)間結(jié)構(gòu)就如同一棵有無(wú)數(shù)分枝的樹，樹上的每個(gè)時(shí)間點(diǎn)都有一個(gè)到有限多個(gè)后繼時(shí)間。

　　3對(duì)時(shí)態(tài)邏輯未來(lái)發(fā)展的展望

　　可以預(yù)見，時(shí)態(tài)邏輯在計(jì)算機(jī)科學(xué)中不斷而深入的應(yīng)用，將為時(shí)態(tài)邏輯乃至整個(gè)邏輯學(xué)提供一種源動(dòng)力。時(shí)態(tài)邏輯未來(lái)的一個(gè)重要發(fā)展方向就是擴(kuò)充發(fā)展，在時(shí)態(tài)邏輯中加入其它的算子就能組成新的邏輯系統(tǒng)。就時(shí)態(tài)邏輯目前在計(jì)算機(jī)科學(xué)中的應(yīng)用來(lái)看，雖然己經(jīng)取得了矚目成就，但計(jì)算機(jī)科學(xué)家們己經(jīng)看到，同其它形式系統(tǒng)一樣，時(shí)態(tài)邏輯也有其局限性：一是時(shí)態(tài)邏輯不能很容易的實(shí)現(xiàn)并發(fā)程序的規(guī)范和驗(yàn)證。設(shè)計(jì)并發(fā)程序是一個(gè)艱難的過(guò)程，時(shí)態(tài)邏輯提供了一種方法，這種方法能夠準(zhǔn)確說(shuō)明程序該做什么和精確分析程序?qū)⒆鍪裁?。精確的推理對(duì)任何形式系統(tǒng)來(lái)說(shuō)都是艱難和費(fèi)時(shí)的，但時(shí)態(tài)邏輯是據(jù)我所知能消除并發(fā)程序中因時(shí)間依賴而產(chǎn)生的細(xì)微誤差的唯一方法。二是時(shí)態(tài)邏輯的表達(dá)能力有限，除了適合說(shuō)明和推理并發(fā)程序之外，在其它地方用處不大。

　　4結(jié)語(yǔ)

　　時(shí)態(tài)邏輯在哲學(xué)上作為非經(jīng)典邏輯的一個(gè)分支，研究涉及時(shí)間的人類思維中的方方面面，主要體現(xiàn)的是理論性和全面性。時(shí)態(tài)邏輯作為計(jì)算機(jī)形式化的一種工具，只研究和工程實(shí)踐有關(guān)的方面，主要體現(xiàn)的是工具性和實(shí)用性。不管是在邏輯學(xué)還是在計(jì)算機(jī)科學(xué)，時(shí)態(tài)邏輯都是一個(gè)重要的研究課題，而在時(shí)態(tài)邏輯中引入其它算子，擴(kuò)充成表達(dá)性更強(qiáng)的系統(tǒng)，近年來(lái)興起的一個(gè)新的研究課題，也是它的一個(gè)十分重要的發(fā)展方向。