線性時間邏輯基于表列、自動機、博弈的模型檢測理論研究.pdf

1、模型檢測理論是邏輯學(xué)和計算機科學(xué)的一個交叉領(lǐng)域，作為模態(tài)邏輯的一個重要分支時間邏輯，它的繁榮發(fā)展就出現(xiàn)在這一領(lǐng)域。數(shù)理邏輯和計算機理論科學(xué)中的最高獎圖靈獎曾于1996年和2007年兩度頒給對模型檢測有重要貢獻的三位科學(xué)家。20世紀(jì)90年代后期，模型檢測的研究基礎(chǔ)才穩(wěn)固下來，它對邏輯學(xué)界的影響以及邏輯學(xué)界對它的重視也開始日益明顯。
　　在邏輯、數(shù)學(xué)和計算機科學(xué)的交界處，有著長久的受重視的傳統(tǒng)，模型檢測思想和這個傳統(tǒng)有著相同的起源，著

2、名的Büchi定理、 Church的序列電路乃至圖靈機都可以為此佐證。然而，從模態(tài)/時間邏輯的角度出發(fā)來研究模型檢測理論在純邏輯學(xué)界卻是一個新課題，筆者第一次站在邏輯學(xué)的視角下，勾勒出模型檢測和應(yīng)用于計算機科學(xué)的時間邏輯的發(fā)展圖景。模型檢測是關(guān)于時間邏輯可滿足性判定問題的研究，其研究的兩類實體一是關(guān)于刻畫程序計算性質(zhì)的邏輯公式，二是用來刻畫程序的模型，模型檢測的任務(wù)就是要校準(zhǔn)這兩種不同形式的信息——公式和模型——是否相一致。
　　

3、線性時間邏輯LTL是應(yīng)用于計算機科學(xué)的一種最基礎(chǔ)的模態(tài)邏輯，而LTL的模型檢測理論也是這個領(lǐng)域中最基礎(chǔ)的部分。筆者將模型檢測理論的研究內(nèi)容劃分為兩部分:一是可滿足性問題研究，二是模型檢測問題研究，前者研究對于某個時間邏輯公式是否存在可滿足的模型，后者研究對于給定模型某個時間邏輯公式是否可滿足。表列、自動機、博弈通常被認(rèn)為是用于解決模型檢測問題的三種元邏輯技術(shù)，筆者分別詳細(xì)闡述了線性時間邏輯LTL基于表列、自動機、博弈的模型檢測理論，并對

4、這三種判定方法進行了比較研究。在考察了三種元邏輯的基礎(chǔ)上，對一種新興的擴展時間邏輯——動態(tài)線性時間邏輯DLTL——進行了全面的更為完整的定義，并使用目前流行的博弈方法給出DLTL模型檢測問題的一個解決方案。概括說來，筆者的主要工作和創(chuàng)新點包括以下四個方面。
　　第一，在對模型檢測的任務(wù)和步驟進行了簡單概括之后，從新的思路出發(fā)，以模型檢測中的核心問題“判定性問題”為線索，系統(tǒng)地回顧了模型檢測的萌芽、初步形式、正式提出和廣泛應(yīng)用、各種

5、擴展時間邏輯的提出四個階段。
　　第二，在對字邏輯、線性時間邏輯LTL、程序與計算、并發(fā)程序等進行概括介紹的基礎(chǔ)上，深入探討了三種元邏輯方法以及它們應(yīng)用于LTL的模型檢測理論，即LTL基于表列的模型檢測理論、LTL基于自動機的模型檢測理論、LTL基于博弈的模型檢測理論，以可滿足性問題研究和模型檢測問題研究為主要內(nèi)容，對相應(yīng)的判定過程分別證明了其可靠性和完全性。
　　第三，從新的角度將LTL和DLTL同時定義在標(biāo)號轉(zhuǎn)換系統(tǒng)的路

6、徑和字模型的字上，以此建立起LTL、自動機、DLTL之間的內(nèi)在聯(lián)系。之后在前人工作的基礎(chǔ)上，對DLTL的語義進行了全新的更為完整的定義，嘗試使用博弈的判定方法探討DLTL的模型檢測理論。
　　第四，從哲學(xué)和邏輯學(xué)的立場出發(fā)，對應(yīng)用于模型檢測的表列、自動機和博弈進行了比較研究和哲學(xué)分析，在較為寬廣的背景下探討這項研究的理論意義，嘗試著展望未來的發(fā)展前景并分析了可能進一步探討的方向。
　　時間邏輯在模型檢測中完成了從理論到應(yīng)用的