線性時(shí)態(tài)邏輯(LTL)現(xiàn)今已被廣泛運(yùn)用于計(jì)算機(jī)科學(xué)領(lǐng)域(CS)。它常作為描述系統(tǒng)行為的性質(zhì)語(yǔ)言,用在程序驗(yàn)證、程序綜合與人工智能(AI)等研究方向。比方說(shuō),為了驗(yàn)證給定的系統(tǒng)是否滿足其對(duì)應(yīng)的性質(zhì)規(guī)范(通常是用LTL來(lái)書寫的),模型檢測(cè)技術(shù)會(huì)將該性質(zhì)的否定轉(zhuǎn)成與其等價(jià)的Buchi自動(dòng)機(jī),把它與系統(tǒng)模型求交得到新的自動(dòng)機(jī),并在這新的自動(dòng)機(jī)上檢查其接收的語(yǔ)言是否為空,從而可以判定系統(tǒng)是否滿足該性質(zhì)。從LTL在CS中的應(yīng)用場(chǎng)景我們可以抽取出LTL的兩個(gè)基本研究問題：一是從LTL公式到與其等價(jià)的Buchi自動(dòng)機(jī)的轉(zhuǎn)換算法,這個(gè)算法要被頻繁的應(yīng)用于程序驗(yàn)證、程序綜合等方向；還有一個(gè)就是LTL公式的可滿足性檢查問題-這是因?yàn)樵趯?shí)際的應(yīng)用場(chǎng)景中不可滿足的公式是沒有意義的。本文因此就以上兩個(gè)問題展開,提出一些新的算法與解決方案。 我們首先探索從LTL公式到其等價(jià)的Buchi自動(dòng)機(jī)的轉(zhuǎn)換問題,并提出一種新的轉(zhuǎn)換算法(第三章)。和其他方法相比,我們的方案避免了中間自動(dòng)機(jī)的生成,這就潛在的可以加快構(gòu)造的進(jìn)程。我們實(shí)現(xiàn)了該算法并與SPOT工具作了比較-SPOT是目前為止公認(rèn)度較高的最好的LTL到Buchi自動(dòng)機(jī)...

【文章頁(yè)數(shù)】：137 頁(yè)

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

【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 線性時(shí)態(tài)邏輯在計(jì)算機(jī)領(lǐng)域的重要性
    1.2 線性時(shí)態(tài)邏輯在若干問題中的研究現(xiàn)狀
    1.3 本文的選題與主要工作
第二章 基礎(chǔ)知識(shí)
    2.1 LTL線性時(shí)態(tài)邏輯
    2.2 Buchi自動(dòng)機(jī)
    2.3 LTL_f有限線性時(shí)態(tài)邏輯
第三章 從LTL到Buchi自動(dòng)機(jī)的轉(zhuǎn)化
    3.1 背景介紹
    3.2 一個(gè)驅(qū)動(dòng)例子
    3.3 LTL遷移系統(tǒng)
    3.4 轉(zhuǎn)換算法
    3.5 實(shí)驗(yàn)仿真
    3.6 本章小結(jié)
第四章 LTL可滿足性檢查
    4.1 背景介紹
    4.2 義務(wù)加速檢查
    4.3 基于義務(wù)集的完備的可滿足性檢查
    4.4 中心定理的證明
    4.5 實(shí)驗(yàn)仿真
    4.6 本章小結(jié)
第五章 基于SAT技術(shù)的LTL可滿足性檢查
    5.1 背景介紹
    5.2 應(yīng)用義務(wù)公式進(jìn)行的LTL可滿足性檢查
    5.3 基于SAT的加速技術(shù)
    5.4 實(shí)驗(yàn)仿真
    5.5 本章小結(jié)
第六章 LTL_f的可滿足性檢查
    6.1 背景介紹
    6.2 從LTL_f到LTL的可滿足性規(guī)約檢查
    6.3 LTL_f遷移系統(tǒng)
    6.4 基于LTL_f有限屬性的可滿足性檢查
    6.5 優(yōu)化技術(shù)
    6.6 實(shí)驗(yàn)仿真
    6.7 本章小結(jié)
第七章 工具的開發(fā)與使用
    7.1 工具的產(chǎn)生背景
    7.2 工具的簡(jiǎn)單介紹
    7.3 工具的性能測(cè)試
    7.4 工具的使用說(shuō)明
    7.5 小結(jié)
第八章 總結(jié)與展望
    8.1 全文小結(jié)
    8.2 未來(lái)工作展望
參考文獻(xiàn)
致謝
攻讀博士學(xué)位期間發(fā)表論文和參與科研情況



本文編號(hào)：3903051