線性時態(tài)邏輯(LTL)自從上個世紀七十年代被引入計算機科學(xué)領(lǐng)域之后,得到了很大的發(fā)展�，F(xiàn)如今,LTL作為一種形式化的性質(zhì)規(guī)范描述,已在程序驗證與分析、程序綜合、數(shù)據(jù)庫和人工智能領(lǐng)域被廣泛使用。對于邏輯語言LTL來講,可滿足性問題是一個亟待解決的關(guān)鍵性問題。與此同時,對于工業(yè)界而言,該問題也是十分重要的。因為對于程序驗證、綜合或是人工智能領(lǐng)域而言,不可滿足的公式是沒有意義的。本文就LTL的可滿足性問題展開,介紹了一種新的算法OFOA(第三章)。傳統(tǒng)方法中,對LTL的可滿足性性判定需要先將其轉(zhuǎn)化為等價的Buchi自動機,然后再進行判斷；而我們的算法提供了一套全新的推理框架,可以在公式展開的同時對其可滿足性進行判斷,這就是一個明顯的優(yōu)化。按照"on the fly"的思想,我們?yōu)長TL公式定義了“義務(wù)集合”的概念,從而極大加速了公式可滿足性的判定過程。以該算法為基礎(chǔ),我們設(shè)計實現(xiàn)了LTL可滿足性判定工具Aalta,文章的后半部分主要介紹該工具的設(shè)計框架、相應(yīng)的數(shù)據(jù)結(jié)構(gòu)和核心算法。為了驗證算法的效率,我們選取目前公認的最出色的可滿足性檢查工具(PANDA、Cadence SMV和SPOT)進行...

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

【學(xué)位級別】：碩士

【文章目錄】：
摘要
ABSTRACT
第一章：緒論
    1.1 線性時態(tài)邏輯的發(fā)展歷程
    1.2 線性時態(tài)邏輯的應(yīng)用場景
        1.2.1 程序驗證
        1.2.2 程序綜合
    1.3 線性時態(tài)邏輯的研究現(xiàn)狀
    1.4 本文的選題與主要工作
第二章 背景知識
    2.1 LTL線性時態(tài)邏輯
        2.1.1 LTL語法
        2.1.2 LTL語義
    2.2 Büchi自動機
    2.3 遷移系統(tǒng)
    2.4 LTL可滿足性檢查算法
        2.4.1 基于tableau方法的LTL可滿足性檢查
        2.4.2 轉(zhuǎn)化為模型檢查問題的LTL可滿足性檢查
    2.5 本章小結(jié)
第三章 LTL可滿足性算法框架設(shè)計
    3.1 從LTL到Buchi自動機
    3.2 義務(wù)加速檢查
    3.3 基于義務(wù)集合的可滿足性檢查
    3.4 基于SAT技術(shù)的LTL可滿足性檢查
    3.5 本章小結(jié)
第四章 LTL可滿足性工具詳細設(shè)計與實現(xiàn)
    4.1 數(shù)據(jù)結(jié)構(gòu)
        4.1.1 公式結(jié)構(gòu)
        4.1.2 DNF結(jié)構(gòu)
        4.1.3 存儲結(jié)構(gòu)
    4.2 核心算法
        4.2.1 規(guī)范化
        4.2.2 化簡
        4.2.3 一致性判斷
        4.2.4 尋找強連通分量
    4.3 Aalta的實現(xiàn)
        4.3.1 輸入
        4.3.2 輸出
        4.3.3 語法解析器
        4.3.4 公式構(gòu)建器
        4.3.5 可滿足性檢查器
    4.4 本章小結(jié)
第五章 實驗結(jié)果
    5.1 實驗工具
    5.2 實驗平臺
    5.3 實驗輸入
    5.4 實驗結(jié)果
    5.5 本章小結(jié)
第六章 總結(jié)與展望
參考文獻
碩士階段發(fā)表論文和科研情況
致謝



本文編號：3747296