發(fā)布時(shí)間：2022-01-26 11:33

　　基于區(qū)間的時(shí)序邏輯,如區(qū)間時(shí)序邏輯（ITL）和投影時(shí)序邏輯（PTL）,在并發(fā)系統(tǒng)的規(guī)范與驗(yàn)證方面有著重要的應(yīng)用價(jià)值。然而,當(dāng)前基于區(qū)間時(shí)序邏輯的程序驗(yàn)證主要是應(yīng)用定理證明技術(shù),自動(dòng)化的模型檢測技術(shù)尚未得到深入的研究。其原因是這類邏輯的模型理論不夠完善,特別是它們的判定性、復(fù)雜性和表達(dá)性等問題尚未得到解決。因此,本文研究命題投影時(shí)序邏輯（PPTL）的判定性、復(fù)雜性、表達(dá)性以及模型檢測算法。進(jìn)一步,為了使用基于區(qū)間的時(shí)序邏輯來驗(yàn)證開放系統(tǒng)（Open Systems）,本文提出了交互式區(qū)間時(shí)序邏輯（AITL）和交互式投影時(shí)序邏輯（APTL）,并給出了相應(yīng)的判定算法和模型檢測方法。另外,為了提高模型檢測的效率,緩解狀態(tài)空間爆炸問題,本文給出了目前最好的打結(jié)不變（Stutter-Invariant）命題線性時(shí)序邏輯（PLTL）產(chǎn)生算法,以及新的抽象精化模型檢測算法。本文的主要貢獻(xiàn)如下：（1）定義了PPTL的正則形,證明了任意的PPTL公式都可以被轉(zhuǎn)換成正則形。在正則形的基礎(chǔ)上,定義了PPTL公式的正則圖和帶標(biāo)記的正則圖,證明了正則圖和帶標(biāo)記的正則圖的有窮性,進(jìn)而證明了該邏輯的可滿足性是可判定的,... 

【文章來源】：西安電子科技大學(xué)陜西省 211工程院校 教育部直屬院校

【文章頁數(shù)】：169 頁

【學(xué)位級(jí)別】：博士

【部分圖文】：

尸VQ的NFG

第5章PPTL的表達(dá)性L(ehop)〔L(next，e卜op)C門L(ehop，ehop*)CL(next，ehop，prj④)=}}L(neXt，ehop，ehop*，pFj)=L(next，prj)門L(next，ehop，ehop*)}}L(next，prj，ehop*)=L(next，prj，prj④)L(next，ehop，ehop*，prj④)}}L(next，ehop，e卜op*，prj，prj④)圖5.5PPTL及子集的關(guān)系Star一freeregularIanguage

并進(jìn)一步構(gòu)造出二尸的B位chi自動(dòng)機(jī)A一，。我們可以通過構(gòu)造A，和A一，的積自動(dòng)機(jī)，然后判斷該積自動(dòng)機(jī)所接收的語言是否為空來驗(yàn)證系統(tǒng)是否滿足期望的性質(zhì)，如圖6.1所示。如果積自動(dòng)機(jī)可接收的語言為空，那么系統(tǒng)就滿足期望的性質(zhì)，否則圖6.1基于自動(dòng)機(jī)的PPTL模型檢測系統(tǒng)不滿足期望的性質(zhì)，并給出一個(gè)反例。SPIN已經(jīng)實(shí)現(xiàn)了一個(gè)將線性時(shí)序邏輯公式自動(dòng)轉(zhuǎn)換為永非斷言的轉(zhuǎn)換器。為了在SPIN中實(shí)現(xiàn)基于PPTL的模型檢測，我們也提供了一個(gè)由PPTL公式向永非斷言轉(zhuǎn)換的轉(zhuǎn)換器，如圖6.2所示。根據(jù)前面的章節(jié)中提出的算法，我們已經(jīng)用C++實(shí)現(xiàn)了該轉(zhuǎn)換器，并成功地將其集成到了原始的SPIN中。6.2復(fù)雜性討論在第四章中，我們通過將不帶星表達(dá)式的判空問題{86」規(guī)約到PPTL公式的可滿足性問題


本文編號(hào)：3610420