淺談時態(tài)邏輯在計算機科學中的發(fā)展

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

　　1 計算機科學中時態(tài)邏輯的形式化

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

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

　　2 時態(tài)邏輯對計算機科學的貢獻

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

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

　　3對時態(tài)邏輯未來發(fā)展的展望

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

　　4結(jié)語

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