淺談時態邏輯在電腦科學中的發展

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

　　1 電腦科學中時態邏輯的形式化

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

　　在電腦科學領域，形式化方法是一種建立在嚴格的數學基礎上，具有精確數學表達形式和語義的開發方法。這種開發方法試圖實現從軟體的規範，軟體的設計到軟體的程式碼實現自動轉換和驗證，從而充分保證系統的正確性和可靠性。在軟體開發過程中，最初級最原始的描述系統也就是規範的方法是用日常語言，這是一種非形式化方法，但這種描述方法可能存在模糊性、歧義性和層次混亂的缺點。

　　2 時態邏輯對電腦科學的貢獻

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

　　時態邏輯對電腦科學的發展還有一個有用之處是：時態邏輯能夠表達程式的兩個特性：安全性和存活性。安全性用於描述事件必須不會發生，相當於程式中的約束條件;存活性用來描述事件必須最終會發生，它可以防止程式只滿足初始條件及影響其它行為。線性時態邏輯顯示任何兩個不同的時間點都有先後關係，時間序列成不分叉的線狀分佈的時態。與“線性時態邏輯”相對，在分支時間時態邏輯中，時間的結構有分支樹形的性質，即每一個時刻都有多個後繼時刻，時間結構就如同一棵有無數分枝的樹，樹上的每個時間點都有一個到有限多個後繼時間。

　　3對時態邏輯未來發展的展望

　　可以預見，時態邏輯在電腦科學中不斷而深入的應用，將為時態邏輯乃至整個邏輯學提供一種源動力。時態邏輯未來的一個重要發展方向就是擴充發展，在時態邏輯中加入其它的運算元就能組成新的邏輯系統。就時態邏輯目前在電腦科學中的應用來看，雖然己經取得了矚目成就，但電腦科學家們己經看到，同其它形式系統一樣，時態邏輯也有其侷限性：一是時態邏輯不能很容易的實現併發程式的規範和驗證。設計併發程式是一個艱難的過程，時態邏輯提供了一種方法，這種方法能夠準確說明程式該做什麼和精確分析程式將做什麼。精確的推理對任何形式系統來說都是艱難和費時的，但時態邏輯是據我所知能消除併發程式中因時間依賴而產生的細微誤差的唯一方法。二是時態邏輯的表達能力有限，除了適合說明和推理併發程式之外，在其它地方用處不大。

　　4結語

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