線性時(shí)間邏輯基于表列、自動(dòng)機(jī)、博弈的模型檢測(cè)理論研究.pdf

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

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

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

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

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

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